Refine
Document Type
- Doctoral thesis (4)
Has Fulltext
- yes (4)
Is part of the Bibliography
- no (4)
Keywords
- Eingebettete Systeme (4) (remove)
Verification of software for Contiki-based low-power embedded systems using software model checking
(2017)
The main building blocks for the internet of things are connected embedded systems. Often these systems are also used in safety critical applications. Therefore, it is particularly important that these devices work according to their specification i.e. they behave as intended. Nowadays, even for simple devices embedded operating systems as Contiki are used to simplify application development and to increase portability between different hardware platforms.
The main objective of this thesis is to present a methodology for the verification of software applications written for the operation system Contiki, taking the system hardware into account. Therefore, software model checking and especially bounded model checking [BCC⁺03] is used as a technique, which allows to formally verify software for embedded systems.
For verifying the software against its specification, it is also necessary to build a model of the system hardware. Thereby, the difficulty is to create a model which is detailed enough to capture the hardware behavior so that the software performs correctly, while keeping the computation effort for the verification process manageable. In this work, the drivers which communicate with the hardware are therefore replaced with abstract models during the verification process. This enables the verification based on an abstract hardware platform independent of specific hardware.
A special role within embedded systems play interrupts. Interrupts are used to save power and can also be used to react on external events. Current methods for verification of interrupt driven software are based on the interleaving model and partial order reduction to reduce the size of the verification problem. This thesis argues that this method is not sufficient for software, whose behavior relies on periodically occurring interrupts. Therefore, in this thesis, a new approach called periodic interrupt modeling is introduced. This approach can be applied automatically and reduces the number of incorrect verification results due to inaccurate modeling. In addition, properties can be proven that depend on the number of occurring interrupts.
Using applications for the Contiki operating system, and based on a verification flow, the approaches toward interrupt modeling are compared.
With the introduction of the Internet at the end of the last century the modern society was fundamentally changed. Computer systems became an element of nearly all parts of our daily live. Due to the interconnection of these systems local borders are mostly vanished, so that information is accessible and exchangeable anywhere and at anytime. But this increased connectivity causes that physical fences are no longer an adequate protection for computer systems. Whereas the security of commodity computer systems was improved continuously and similarly with their increased connectivity, deeply embedded systems were then and now mostly protected by physical fences. But the ubiquitous availability of embedded systems in personal and commercial environments makes these systems likewise accessible and moves them strongly into the focus of security investigations.
Deeply embedded systems are usually equipped with tiny scale micro controllers, which are limited in their available resources and do not feature secure mechanisms to isolate system resources. Hence, a single error in a local software component is not limited to the component itself, instead the complete system may be influenced. The lack of resource isolation makes tiny scale systems prone for accidental errors but in particular vulnerable for a broad variety of malicious software. For a safe and secure operation of computer systems it is strongly recommended that software components are isolated in such a manner that they have access only to those resources, which are assigned to them. Even though a substantial number of approaches in the context of embedded system’s safety were investigated during the last fifteen years, security was mostly neglected.
This thesis is focused on security aspects where malicious software wittingly tries to bypass available protection mechanisms. The thesis introduces a security platform for tiny scale systems that enforces an isolation of software components considering security aspects. Due to the limited resources of tiny scale systems the proposed solution is based on a co-design process that takes the static and predefined nature of deeply embedded systems into account and includes hardware, compile-time, and run-time partitions to reduce the number of additional run-time components, to avoid performance drawbacks, and to minimize the memory as well as the components footprint overhead. To prove the applicability of the presented platform it was applied and evaluated with two real applications. In addition, an investigation of technologies of commodity computer systems that are suitable to build secure systems is presented. The thesis analyzes their enforcement based on the features provided by the introduced security platform. The contributions of this thesis include an enforcement of a security isolation of system resources on tiny scale systems and enable the development of a broad variety of secure tiny scale system applications.
Drahtlose eingebettete Systeme haben vielfältige Anwendungsmöglichkeiten, sei es im Internet der Dinge oder in Sensornetzen. Diese Systeme sollen dabei ohne Eingriff von außen eine hohe Laufzeit erreichen. Die Energieversorgung und der Verbrauch spielen dabei entscheidende Rollen, sind jedoch Varianzen unterworfen. Sollen Wartungsintervalle oder Lebenszeitziele erreicht werden, ist deshalb ein dynamisches Energiemanagement unabdingbar.
In dieser Doktorarbeit wird ein solcher Ansatz vorgestellt, umgesetzt und evaluiert. Im Gegensatz zu existierenden Ansätzen werden Varianzen auf allen drei Ebenen des Managements (Energieversorgung, Energieverbrauch und Energieverwaltung) adressiert. Für die Energieversorgung wird eine Batterieüberwachung vorgestellt, welche eine Steuerung des Verbrauchs ohne komplexe Berechnung des Ladezustands ermöglicht. Der Verbrauch des Systems wird durch einen Software-basierten Ansatz feingranular ermittelt und bezieht Varianzen durch Änderungen der Spannung und der Effizienz von Spannungswandlern ein. Die Verwaltung und Zuordnung der Energie zu Anwendungszielen erfolgt mittels dynamischer Energiebudgets und bietet verschiedene Strategien, um auf Änderungen des Bedarfs adäquat reagieren zu können.
In dieser Arbeit wird ein umfassendes Betriebssystemkonzept für tief eingebettete Steuersysteme vorgestellt. Das Konzept sieht dabei eine vollständig ereignisbasierte Abarbeitung von Aufgaben vor. Nach einer breiten Domänenanalyse wird gezeigt, welche Vorteile der verfolgte Ansatz hinsichtlich der üblichen Randbedingungen der Zielsysteme hat. Außerdem werden praktische Ergebnisse, welche anhand einer exemplarischen Umsetzung des Konzeptes gewonnen wurde, vorgestellt.