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
Trustworthy Memory Isolation of Linux on Embedded Devices
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-9251-3679
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
Show others and affiliations
2015 (English)In: Trust and Trustworthy Computing, TRUST 2015, Springer Berlin/Heidelberg, 2015, 125-142 p.Conference paper, Published paper (Refereed)
Abstract [en]

The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself, for instance by run-time monitoring. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a virtualization platform for the ARMv7-A processor family. Our design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen for the x86 architecture, and used later with minor variants by the Secure Virtual Architecture, SVA. We show that the direct paging 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 ARMv7-A ISA, including the MMU. We prove memory isolation of the hosted components along with information flow security for an abstract top level model of the virtualization mechanism. The abstract model is refined down to a HOL4 transition system closely resembling a C implementation. The virtualization mechanism is demonstrated on real hardware via a hypervisor capable of hosting Linux as an untrusted guest.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015. 125-142 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9229
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-177437DOI: 10.1007/978-3-319-22846-4_8ISI: 000363795400008Scopus ID: 2-s2.0-84944529938ISBN: 978-3-319-22846-4 (print)ISBN: 978-3-319-22845-7 (print)OAI: oai:DiVA.org:kth-177437DiVA: diva2:872807
Conference
8th International Conference on Trust and Trustworthy Computing (TRUST), AUG 24-26, 2015, Fdn Res & Technol Hellas, Inst Comp Sci, Heraklion, GREECE
Funder
Swedish Foundation for Strategic Research
Note

QC 20160714

Available from: 2015-11-20 Created: 2015-11-20 Last updated: 2016-07-14Bibliographically approved

Open Access in DiVA

fulltext(428 kB)84 downloads
File information
File name FULLTEXT01.pdfFile size 428 kBChecksum SHA-512
eabd45c21835eb3eb15b3c126daef134b2e18898a450344777701c55eca0ab614bcf8c09eefa8e317e8be9911fb1af14777c9cf58985641674837a69bcc9d2ee
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Authority records BETA

Nemati, HamedDam, Mads

Search in DiVA

By author/editor
Nemati, HamedDam, MadsGuanciale, Roberto
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 212 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