Change search
ReferencesLink to record
Permanent link

Direct link
Provably secure memory isolation for Linux on ARM: Submission to special issue on Verified Information Flow Security
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)
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-160558OAI: oai:DiVA.org:kth-197900DiVA: diva2:1054670
Projects
PROSPER
Funder
Swedish Foundation for Strategic Research
Note

QC 20161212

Available from: 2016-12-08 Created: 2016-12-08 Last updated: 2016-12-12Bibliographically approved

Open Access in DiVA

No full text

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

Altmetric score

Total: 9 hits
ReferencesLink to record
Permanent link

Direct link