Change search
ReferencesLink to record
Permanent link

Direct link
Formal Verification of Systems Software: No Execution of Malicious Software in Linux in Networked Embedded Systems
KTH, School of Computer Science and Communication (CSC).
2016 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesisAlternative title
Formell verifiering av systemmjukvara : Ingen skadlig mjukvara i Linux i uppkopplade inbyggda system (Swedish)
Abstract [en]

Embedded systems provide critical services in numerous applications requiring complex functionality. The complex functionality is often implemented by complex software stacks, such as GNU/Linux. Since complex software often contains bugs, some of which might be exploitable by attackers, embedded systems are exposed to security attacks. For instance, malicious software might be injected by exploiting a buffer overflow bug. In addition, the number of embedded systems connected to the Internet is increasing, enabling attackers to perform their attacks remotely and thus making embedded systems even more exposed to security attacks.

To address this issue, this thesis presents a software design and an implementation that host Linux with Internet support, such that only signed (non-malicious) Linux code is executed. The software design consists of three software components: A hypervisor and two guests, Linux and a monitor. These three software components can be executed on the development board BeagleBone Black, containing an ARMv7 CPU and a network interface controller (NIC). The hypervisor ensures that the three software components are securely separated and the monitor ensures that only signed Linux code is executed. The software design and the implementation take into account that Linux code might instruct the CPU to configure the NIC to access memory. This software design and implementation therefore ensure that the security service provided by the monitor is not breached by the NIC. In order to increase the reliability of this system, a pen-and-paper proof plan is presented with the purpose of guiding a formal proof of that only signed Linux code is executed in this system.

The original software design and implementation of the hypervisor, provided by the PROSPER project, did not have NIC support. The software design and the implementation of the hypervisor therefore have been extended with a security layer that intercepts writes to NIC registers that are performed by the CPU when it is executing Linux. If a NIC register write cannot enable unsigned (malicious) Linux code to be executed, the hypervisor lets the NIC register write take effect, and otherwise blocks it. In addition, the original software design of the monitor, also provided by the PROSPER project, did not consider the operation of the NIC. The design of the monitor therefore has also been extended in order to prevent memory configurations of Linux that enable unsigned Linux code to be executed. The proof plan describes and motivates how it can be formally proved in a theorem prover that only signed Linux code is executed in this system. For the purposes of the proof plan, HOL4 models of the hardware have been identified and a formal model of the NIC has been specified in pseudocode.

If the work presented in this thesis is fully implemented and combined with earlier work from the PROSPER project, a networked embedded system is acquired in which, with high reliability, no malicious Linux code is executed.

Abstract [sv]

Inbyggda system har ofta kritiska roller som kräver komplex funktionalitet. Denna funktionalitet implementeras ofta genom återanvändning av komplexa mjukvarustackar som exempelvis GNU/Linux. Då antalet buggar ökar med mängden kod och dess komplexitet, så finns det risk för att inbyggda system innehåller buggar, där vissa buggar potentiellt öppnar upp säkerhetshål. Exempelvis kan en buffertöverskridningsbugg möjliggöra installation av skadlig mjukvara. Därtill är det vanligt att inbyggda system är anslutna till Internet vilket gör inbyggda system än känsligare för säkerhetsattacker.

Denna uppsats beskriver en mjukvarudesign och dess implementation som ökar inbyggda systems tillförlitlighet. Implementationens syfte är att försäkra att endast signerad (icke-skadlig) Linuxkod exekveras. Mjukvarudesignen består av tre mjukvarukomponenter: En hypervisor och dess två gäster, Linux och ett kontrollprogram. Dessa tre komponenter kan exekveras på utvecklingskortet BeagleBone Black som har en ARMv7 processor och ett nätverkskort. Hypervisorn försäkrar att de tre mjukvarukomponenterna är isolerade från varandra på ett säkert sätt, och kontrollprogrammet försäkrar att endast signerad Linuxkod exekveras. Mjukvarudesignen och implementationen förhindrar processorn när den exekverar Linux från att konfigurera vilka minnesåtkomster nätverkskortet kan göra. Nätverkskortet kan därför inte förhindra kontrollprogrammet från att försäkra att endast signerad Linuxkod exekveras. För att öka detta systems tillförlitlighet så presenteras även en bevisplan som beskriver hur ett formellt bevis kan konstrueras för att endast signerad Linuxkod exekveras i detta system.

Den ursprungliga mjukvarudesignen och implementationen av hypervisorn, utvecklade i PROSPER projektet, hade inget stöd för nätverkskortet. Mjukvarudesignen och implementation av hypervisorn har därför utökats med ett mjukvarulager som anropas när processorn exekverar Linux och försöker skriva ett nätverkskortsregister. Om skrivningen till nätverkskortsregistret inte kan möjliggöra exekvering av osignerad (skadlig) Linuxkod, så utför processorn skrivningen, och annars inte. Även den ursprungliga mjukvarudesignen av monitorn, också utvecklad i PROSPER projektet, tog inte hänsyn till nätverkskortet. Mjukvarudesignen av monitorn har därför också utökats för att försäkra att minneskonfigurationen är kompatibel med nätverkskortets konfiguration så att nätverkskortet inte möjliggör exekvering av osignerad Linuxkod. Bevisplanen beskriver och motiverar hur det kan bevisas formellt i en teorembevisare att endast signerad Linuxkod exekveras i detta system. Denna bevisplan baseras på en mängd HOL4 modeller och en formell modell av nätverkskortet som specificerats med pseudokod.

Om arbetet som presenteras i denna uppsats implementeras fullt ut och kombineras med tidigare arbete som gjorts i PROSPER projektet, så erhålles ett uppkopplat inbyggt system som, med hög tillförlitlighet, endast exekverar signerad Linuxkod.

Place, publisher, year, edition, pages
2016.
Keyword [en]
formal verification, embedded systems, linux, malware, network, Internet, virtualization, hypervisor, theorem proving, formal methods, NIC, modeling, BeagleBone Black, malicious software, NIC model, proof plan, secure network virtualization
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-195719OAI: oai:DiVA.org:kth-195719DiVA: diva2:1045316
Educational program
Master of Science in Engineering - Computer Science and Technology
Supervisors
Examiners
Available from: 2016-11-21 Created: 2016-11-08 Last updated: 2016-11-21Bibliographically approved

Open Access in DiVA

No full text

By organisation
School of Computer Science and Communication (CSC)
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Total: 37 hits
ReferencesLink to record
Permanent link

Direct link