Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Provably secure memory isolation for Linux on ARM
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. (TCS)
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. (TCS)ORCID iD: 0000-0001-9251-3679
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. (TCS)ORCID iD: 0000-0001-5432-6442
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. (TCS)ORCID iD: 0000-0003-4889-8326
2016 (English)In: Journal of Computer Security, ISSN 0926-227X, E-ISSN 1875-8924, Vol. 24, no 6, 793-837 p.Article in journal (Refereed) Published
Abstract [en]

The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a memory virtualization platform for ARMv7-A processors. The design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen. It is shown that this mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the processor. We prove memory isolation along with information flow security for an abstract top-level model of the virtualization mechanism. The abstract model is refined down to a transition system closely resembling a C implementation. Additionally, it is demonstrated how the gap between the low-level abstraction and the binary level-can be filled, using tools that check Hoare contracts. The virtualization mechanism is demonstrated on real hardware via a hypervisor hosting Linux and supporting a tamper-proof run-time monitor that provably prevents code injection in the Linux guest.

Place, publisher, year, edition, pages
IOS Press, 2016. Vol. 24, no 6, 793-837 p.
Keyword [en]
Formal verification, information flow security, separation kernel, hypervisor
National Category
Engineering and Technology
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-197900DOI: 10.3233/JCS-160558ISI: 000389850600004OAI: oai:DiVA.org:kth-197900DiVA: diva2:1054670
Projects
PROSPER, CERCES
Funder
Swedish Foundation for Strategic Research
Note

QC 20161212

Available from: 2016-12-08 Created: 2016-12-08 Last updated: 2017-10-06Bibliographically approved
In thesis
1. Secure System Virtualization: End-to-End Verification of Memory Isolation
Open this publication in new window or tab >>Secure System Virtualization: End-to-End Verification of Memory Isolation
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Over the last years, security-kernels have played a promising role in reshaping the landscape of platform security on embedded devices. Security-kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms on a small TCB, which enforces isolation between components. The reduced TCB  minimizes the system attack surface and facilitates the use of formal methods to ensure the kernel functional correctness and security.

In this thesis, we explore various aspects of building a provably secure separation kernel using virtualization technology. We show how the memory management subsystem can be virtualized to enforce isolation of system components. Virtualization is done using direct-paging that enables a guest software to manage its own memory configuration. We demonstrate the soundness of our approach by verifying that the high-level model of the system fulfills the desired security properties. Through refinement, we then propagate these properties (semi-)automatically to the machine-code of the virtualization mechanism.

Further, we show how a runtime monitor can be securely deployed alongside a Linux guest on a hypervisor to prevent code injection attacks targeting Linux. The monitor takes advantage of the provided separation to protect itself and to retain a complete view of the guest.

Separating components using a low-level software cannot by itself guarantee the system security. Indeed, current processors architecture involves features that can be utilized to violate the isolation of components. We present a new low-noise attack vector constructed by measuring caches effects which is capable of breaching isolation of components and invalidates the verification of a software that has been verified on a memory coherent model. To restore isolation, we provide several countermeasures and propose a methodology to repair the verification by including data-caches in the statement of the top-level security properties of the system.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2017. 51 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2017:18
Keyword
Platform Security, Hypervisor, Formal Verification, Theorem Proving, HOL4, Cache attack, Security Monitor, Information Flow
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-213030 (URN)978-91-7729-478-8 (ISBN)
Public defence
2017-10-20, Kollegiesalen, Brinellvägen 8, Stockholm, 14:00 (English)
Opponent
Supervisors
Projects
PROSPERHASPOC
Funder
Swedish Foundation for Strategic Research , 6561
Note

QC 20170831

Available from: 2017-08-31 Created: 2017-08-28 Last updated: 2017-09-29Bibliographically approved

Open Access in DiVA

fulltext(976 kB)4 downloads
File information
File name FULLTEXT01.pdfFile size 976 kBChecksum SHA-512
85c7e1108e277839e060f3df786a70e3ba5f3cc174639ec4bba91f0fbb2d0cf74de91bf3b80fab63d15d3061a040888f178eac78535567e8bccf971e950ac850
Type fulltextMimetype application/pdf

Other links

Publisher's full texthttp://content.iospress.com/articles/journal-of-computer-security/jcs558

Search in DiVA

By author/editor
Guanciale, RobertoNemati, HamedDam, MadsBaumann, Christoph
By organisation
Theoretical Computer Science, TCS
In the same journal
Journal of Computer Security
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 4 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

Altmetric score

Total: 345 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf