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 virtualization of the ARMv7 memory subsystem
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.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
2015 (English)In: 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015, Springer Berlin/Heidelberg, 2015, 578-589 p.Conference paper, Published paper (Refereed)
Abstract [en]

In order to host a general purpose operating system, hypervisors need to virtualize the CPU memory subsystem. This entails dynamically changing MMU resources, in particular the page tables, to allow a hosted OS to reconfigure its own memory. In this paper we present the verification of the isolation properties of a hypervisor design that uses direct paging. This virtualization approach allows to host commodity Oss without requiring either shadow data structures or specialized hardware support. Our verification targets a system consisting of a commodity CPU for embedded devices (ARMv7), a hypervisor and an untrusted guest running Linux.The verification involves three steps: (i) Formalization of an ARMv7 CPU that includes the MMU, (ii) Formalization of a system behavior that includes the hypervisor and the untrusted guest (iii) Verification of the isolation properties. Formalization and proof are done in the HOL4 theorem prover, thus allowing to re-use the existing HOL4 ARMv7 model developed in Cambridge.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015. 578-589 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8939
Keyword [en]
Formal verification, Hypervisor, Memory management, Theorem proving, Virtual reality, Embedded device, Memory subsystems, Specialized hardware, System behaviors, Theorem provers, Virtualizations, Memory management units
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:kth:diva-167389DOI: 10.1007/978-3-662-46078-8_48ISI: 000357679300047Scopus ID: 2-s2.0-84922031791ISBN: 9783662460771 (print)OAI: oai:DiVA.org:kth-167389DiVA: diva2:815173
Conference
41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015; Pec pod Sněžkou; Czech Republic; 24 January 2015 through 29 January 2015
Note

QC 20150529

Available from: 2015-05-29 Created: 2015-05-22 Last updated: 2016-07-14Bibliographically approved

Open Access in DiVA

fulltext(926 kB)73 downloads
File information
File name FULLTEXT01.pdfFile size 926 kBChecksum SHA-512
35ff746a3dc7c40c3bb7c0b3de8b84d3f846ad3ce9e5aed0169a7471db494db05d0857d0196a2a34b0dc67492526c68de51a16702a06ecf555f1458df105c987
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Authority records BETA

Nemati, HamedDam, Mads

Search in DiVA

By author/editor
Nemati, HamedGuanciale, RobertoDam, Mads
By organisation
Theoretical Computer Science, TCS
Computer and Information Science

Search outside of DiVA

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