Change search
ReferencesLink to record
Permanent link

Direct link
No Hypervisor Is an Island: System-wide Isolation Guarantees for Low Level Code
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0003-3434-5640
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The times when malware was mostly written by curious teenagers are long gone. Nowadays, threats come from criminals, competitors, and government agencies. Some of them are very skilled and very targeted in their attacks. At the same time, our devices – for instance mobile phones and TVs – have become more complex, connected, and open for the execution of third-party software. Operating systems should separate untrusted software from confidential data and critical services. But their vulnerabilities often allow malware to break the separation and isolation they are designed to provide. To strengthen protection of select assets, security research has started to create complementary machinery such as security hypervisors and separation kernels, whose sole task is separation and isolation. The reduced size of these solutions allows for thorough inspection, both manual and automated. In some cases, formal methods are applied to create mathematical proofs on the security of these systems.

The actual isolation solutions themselves are carefully analyzed and included software is often even verified on binary level. The role of other software and hardware for the overall system security has received less attention so far. The subject of this thesis is to shed light on these aspects, mainly on (i) unprivileged third-party code and its ability to influence security, (ii) peripheral devices with direct access to memory, and (iii) boot code and how we can selectively enable and disable isolation services without compromising security.

The papers included in this thesis are both design and verification oriented, however, with an emphasis on the analysis of instruction set architectures. With the help of a theorem prover, we implemented various types of machinery for the automated information flow analysis of several processor architectures. The analysis is guaranteed to be both sound and accurate.

Abstract [sv]

Förr skrevs skadlig mjukvara mest av nyfikna tonåringar. Idag är våra datorer under ständig hot från statliga organisationer, kriminella grupper, och kanske till och med våra affärskonkurrenter. Vissa besitter stor kompetens och kan utföra fokuserade attacker. Samtidigt har tekniken runtomkring oss (såsom mobiltelefoner och tv-apparater) blivit mer komplex, uppkopplad och öppen för att exekvera mjukvara från tredje part.

Operativsystem borde egentligen isolera känslig data och kritiska tjänster från mjukvara som inte är trovärdig. Men deras sårbarheter gör det oftast möjligt för skadlig mjukvara att ta sig förbi operativsystemens säkerhetsmekanismer. Detta har lett till utveckling av kompletterande verktyg vars enda funktion är att förbättra isolering av utvalda känsliga resurser. Speciella virtualiseringsmjukvaror och separationskärnor är exempel på sådana verktyg. Eftersom sådana lösningar kan utvecklas med relativt liten källkod, är det möjligt att analysera dem noggrant, både manuellt och automatiskt. I några fall används formella metoder för att generera matematiska bevis på att systemet är säkert.

Själva isoleringsmjukvaran är oftast utförligt verifierad, ibland till och med på assemblernivå. Dock så har andra komponenters påverkan på systemets säkerhet hittills fått mindre uppmärksamhet, både när det gäller hårdvara och annan mjukvara. Den här avhandlingen försöker belysa dessa aspekter, huvudsakligen (i) oprivilegierad kod från tredje part och hur den kan påverka säkerheten, (ii) periferienheter med direkt tillgång till minnet och (iii) startkoden, samt hur man kan aktivera och deaktivera isolationstjänster på ett säkert sätt utan att starta om systemet.

Avhandlingen är baserad på sex tidigare publikationer som handlar om både design- och verifikationsaspekter, men mest om säkerhetsanalys av instruktionsuppsättningar. Baserat på en teorembevisare har vi utvecklat olika verktyg för den automatiska informationsflödesanalysen av processorer. Vi har använt dessa verktyg för att tydliggöra vilka register oprivilegierad mjukvara har tillgång till på ARM- och MIPS-maskiner. Denna analys är garanterad att vara både korrekt och precis. Så vitt vi vet är vi de första som har publicerat en lösning för automatisk analys och bevis av informationsflödesegenskaper i standardinstruktionsuppsättningar.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2016. , 180 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2016:22
Keyword [en]
Platform Security, Hypervisor, Formal Verification, Theorem Proving, HOL4, DMA, Peripheral Devices, Instruction Set Architectures, ISA, Information Flow, Boot
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-192466ISBN: 978-91-7729-104-6OAI: oai:DiVA.org:kth-192466DiVA: diva2:968761
Public defence
2016-10-10, F3, Lindstedtsvägen 26, Stockholm, 14:00 (English)
Opponent
Supervisors
Projects
PROSPERHASPOC
Funder
Swedish Foundation for Strategic Research VINNOVA
Note

QC 20160919

Available from: 2016-09-19 Created: 2016-09-12 Last updated: 2016-09-19Bibliographically approved
List of papers
1. Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Open this publication in new window or tab >>Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Show others...
2013 (English)Conference paper (Refereed)
Abstract [en]

A separation kernel simulates a distributed environment us-ing a single physical machine by executing partitions in iso-lation and appropriately controlling communication amongthem. We present a formal verication of information owsecurity for a simple separation kernel for ARMv7. Previouswork on information ow kernel security leaves communica-tion to be handled by model-external means, and cannot beused to draw conclusions when there is explicit interactionbetween partitions. We propose a dierent approach wherecommunication between partitions is made explicit and theinformation ow is analyzed in the presence of such a chan-nel. Limiting the kernel functionality as much as meaning-fully possible, we accomplish a detailed analysis and veri-cation of the system, proving its correctness at the levelof the ARMv7 assembly. As a sanity check we show howthe security condition is reduced to noninterference in thespecial case where no communication takes place. The ver-ication is done in HOL4 taking the Cambridge model ofARM as basis, transferring verication tasks on the actualassembly code to an adaptation of the BAP binary analysistool developed at CMU.

Place, publisher, year, edition, pages
ACM Press, 2013
Keyword
Formal verication; Information Flow Security; Separation Kernel; Hypervisor
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-136348 (URN)2-s2.0-84889040001 (ScopusID)
External cooperation:
Conference
2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13),November 4 - 8, 2013 Berlin, Germany
Note

Qc 20131218

Available from: 2013-12-04 Created: 2013-12-04 Last updated: 2016-09-12Bibliographically approved
2. Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
Open this publication in new window or tab >>Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
2013 (English)In: Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, Springer, 2013, 276-291 p.Conference paper (Refereed)
Abstract [en]

In this paper, we formally verify security properties of the ARMv7 Instruction Set Architecture (ISA) for user mode executions. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. This work establishes a main requirement for operating system and hypervisor verification, as demonstrated for the PROSPER separation kernel. The proof is performed in the HOL4 theorem prover, taking the Cambridge model of ARM as basis. To this end, a proof tool has been developed, which assists the verification of relational state predicates semi-automatically.

Place, publisher, year, edition, pages
Springer, 2013
Series
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8307
Keyword
ARM instruction set, noninterference, user mode execution, kernel security, theorem proving
National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-136354 (URN)10.1007/978-3-319-03545-1_18 (DOI)2-s2.0-84893128835 (ScopusID)978-3-319-03544-4 (ISBN)978-3-319-03545-1 (ISBN)
Conference
Certified Programs and Proofs (CPP)
Projects
PROSPER
Funder
Swedish Foundation for Strategic Research
Note

The provided file is the author version of the correspondent paper published in the proceedings of Certified Programs and Proofs 2013 (CPP; editors: G. Gonthier and M. Norrish), Springer LNCS 8307. The publisher and copyright holder is Springer International Publishing Switzerland. The final publication is available at http://link.springer.com/10.1007/978-3-319-03545-1_18. QC 20140624

Available from: 2013-12-04 Created: 2013-12-04 Last updated: 2016-09-12Bibliographically approved
3. Automatic Derivation of Platform Noninterference Properties
Open this publication in new window or tab >>Automatic Derivation of Platform Noninterference Properties
2016 (English)In: Software Engineering and Formal Methods, Springer LNCS 9763 / [ed] Rocco De Nicola, Eva Kühn, 2016, 27-44 p.Conference paper (Refereed)
Abstract [en]

For the verification of system software, information flow properties of the instruction set architecture (ISA) are essential.They show how information propagates through the processor, including sometimes opaque control registers.Thus, they can be used to guarantee that user processes cannot infer the state of privileged system components, such as secure partitions.Formal ISA models - for example for the HOL4 theorem prover - have been available for a number of years. However, little work has been published on the formal analysis of these models.In this paper, we present a general framework for proving information flow properties of a number of ISAs automatically, for example for ARM.The analysis is represented in HOL4 using a direct semantical embedding of noninterference, and does not use an explicit type system, in order to (i) minimize the trusted computingbase, and to (ii) support a large degree of context-sensitivity, which is needed for the analysis.The framework determines automatically which system components are accessible at a given privilege level, guaranteeing both soundness and accuracy.

Series
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9763
Keyword
Instruction set architectures, ARM, MIPS, noninterference, information flow, theorem proving, HOL4
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-192451 (URN)10.1007/978-3-319-41591-8_3 (DOI)978-3-319-41590-1 (ISBN)978-3-319-41591-8 (ISBN)
Conference
Software Engineering and Formal Methods (SEFM)
Projects
PROSPERHASPOCCERCES
Funder
VINNOVASwedish Foundation for Strategic Research Swedish Civil Contingencies Agency
Note

QC 20160916

Available from: 2016-09-12 Created: 2016-09-12 Last updated: 2016-09-16Bibliographically approved
4. Formal Verification of Secure User Mode Device Execution with DMA
Open this publication in new window or tab >>Formal Verification of Secure User Mode Device Execution with DMA
2014 (English)In: Hardware and Software: Verification and Testing / [ed] Eran Yahav, Springer Publishing Company, 2014, 236-251 p.Conference paper (Refereed)
Abstract [en]

Separation between processes on top of an operating systemor between guests in a virtualized environment is essential for establish-ing security on modern platforms. A key requirement of the underlyinghardware is the ability to support multiple partitions executing on theshared hardware without undue interference. For modern processor archi-tectures - with hardware support for memory management, several modesof operation and I/O interfaces - this is a delicate issue requiring deepanalysis at both instruction set and processor implementation level. In afirst attempt to rigorously answer this type of questions we introducedin previous work an information flow analysis of user program executionon an ARMv7 platform with hardware supported memory protection,but without I/O. The analysis was performed as a semi-automatic proofsearch procedure on top of an ARMv7 ISA model implemented in theCambridge HOL4 theorem prover by Fox et al. The restricted platformfunctionality, however, makes the analysis of limited practical value. Inthis paper we add support for devices, including DMA, to the analy-sis. To this end, we propose an approach to device modeling based onthe idea of executing devices nondeterministically in parallel with the(single-core) deterministic processor, covering a fine granularity of inter-actions between the model components. Based on this model and tak-ing the ARMv7 ISA as an example, we provide HOL4 proofs of severalnoninterference-oriented isolation properties for a partition executing inthe presence of devices which potentially use DMA or interrupts.

Place, publisher, year, edition, pages
Springer Publishing Company, 2014
Series
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8855
Keyword
peripheral devices, DMA, separation, isolation, user mode execu- tion, ARM, formal hardware/software co-verification, theorem proving, HOL4
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-155718 (URN)10.1007/978-3-319-13338-6_18 (DOI)2-s2.0-84921419001 (ScopusID)978-3-319-13337-9 (ISBN)978-3-319-13338-6 (ISBN)
Conference
10th International Haifa Verification Conference, HVC 2014
Projects
PROSPER
Funder
Swedish Foundation for Strategic Research
Note

QC 20141117

Available from: 2014-11-10 Created: 2014-11-10 Last updated: 2016-09-12Bibliographically approved
5. Securing DMA through virtualization
Open this publication in new window or tab >>Securing DMA through virtualization
2012 (English)In: 2012 IEEE Workshop on Complexity in Engineering, 2012, 118-123 p.Conference paper (Refereed)
Abstract [en]

We present a solution for preventing guests in a virtualized system from using direct memory access (DMA) to access memory regions of other guests. The principles we suggest, and that we also have implemented, are purely based on software and standard hardware. No additional virtualization hardware such as an I/O Memory Management Unit (IOMMU) is needed. Instead, the protection of the DMA controller is realized with means of a common ARM MMU only. Overhead occurs only in pre- and postprocessing of DMA transfers and is limited to a few microseconds. The solution was designed with focus on security and the abstract concept of the approach was formally verified.

National Category
Computer Science
Identifiers
urn:nbn:se:kth:diva-112887 (URN)10.1109/CompEng.2012.6242958 (DOI)2-s2.0-84866553727 (ScopusID)
Conference
2nd IEEE Workshop on Complexity in Engineering, COMPENG 2012;Aachen
Funder
ICT - The Next Generation
Note

QC 20130115

Available from: 2013-01-14 Created: 2013-01-14 Last updated: 2016-09-12Bibliographically approved
6. Affordable Separation on Embedded Platforms: Soft Reboot Enabled Virtualization on a Dual Mode System
Open this publication in new window or tab >>Affordable Separation on Embedded Platforms: Soft Reboot Enabled Virtualization on a Dual Mode System
2014 (English)In: / [ed] Thorsten Holz, Sotiris Ioannidis, Springer, 2014, -54 p.Conference paper (Refereed)
Abstract [en]

While security has become important in embedded systems, commodity operating systems often fail in effectively separating processes, mainly due to a too large trusted computing base. System virtualization can establish isolation already with a small code base, but many existing embedded CPU architectures have very limited virtualization hardware support, so that the performance impact is often non-negligible. Targeting both security and performance, we investigate an approach in which a few minor hardware additions together with virtualization offer protected execution in embedded systems while still allowing non-virtualized execution when secure services are not needed. Benchmarks of a prototype implementation on an emulated ARM Cortex A8 platform confirm that switching between those two execution forms can be done efficiently.

Place, publisher, year, edition, pages
Springer, 2014
Keyword
Dual Mode, Separation, Soft Reboot, Virtualization, Hypervisor, Embedded Systems, Security
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-147612 (URN)10.1007/978-3-319-08593-7_3 (DOI)978-3-319-08592-0 (ISBN)978-3-319-08593-7 (ISBN)
Conference
TRUST
Funder
Swedish Foundation for Strategic Research
Note

This is the author version of the correspondent paper published in the proceedings of TRUST 2014 (editors: Thorsten Holz, Sotiris Ioannidis), Springer LNCS 8564. The publisher is Springer International Publishing Switzerland. The final publication is available at http://link.springer.com/10.1007/978-3-319-08593-7_3.

QC 20140708

Available from: 2014-06-30 Created: 2014-06-30 Last updated: 2016-09-12Bibliographically approved

Open Access in DiVA

thesis Oliver Schwarz(2131 kB)27 downloads
File information
File name FULLTEXT01.pdfFile size 2131 kBChecksum SHA-512
97d25a6597e006ea3815d5015a8feab5161e3d77baa2585c1f8af0b2c24f47a6d97a6c479d9f310f642b03c07ec0f955c430ad59a78e628f8ff418a6997c3081
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Schwarz, Oliver
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 27 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 124 hits
ReferencesLink to record
Permanent link

Direct link