Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Trustworthy Memory Isolation of Linux on Embedded Devices
KTH Royal Institute of Technology, Sweden.
KTH Royal Institute of Technology, Sweden.
KTH Royal Institute of Technology, Sweden.
RISE., Swedish ICT, SICS.
Visa övriga samt affilieringar
2015 (Engelska)Ingår i: Trust and Trustworthy Computing / [ed] Mauro Conti, Matthias Schunter, Ioannis Askoxylakis, 2015, Vol. 9229, s. 125-142Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
2015. Vol. 9229, s. 125-142
Serie
Lecture Notes in Computer Science (LNCS), ISSN 0302-9743, E-ISSN 1611-3349 ; 9229
Nyckelord [en]
Coherence, Ghost, Flushing, Aliasing
Nationell ämneskategori
Datorsystem
Identifikatorer
URN: urn:nbn:se:ri:diva-33281DOI: 10.1007/978-3-319-22846-4_8Scopus ID: 2-s2.0-84944529938ISBN: 978-3-319-22845-7 (tryckt)ISBN: 978-3-319-22846-4 (digital)OAI: oai:DiVA.org:ri-33281DiVA, id: diva2:1183715
Konferens
8th International Conference on Trust and Trustworthy Computing (TRUST 2015), August 24-26, 2015, Heraklion, Greece
Projekt
PROSPERTillgänglig från: 2018-02-19 Skapad: 2018-02-19 Senast uppdaterad: 2020-12-01Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Sök vidare i DiVA

Av författaren/redaktören
Vahidi, Arash
Av organisationen
SICS
Datorsystem

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 18 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf