lnu.sePublications
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
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties.
KTH Royal Institute of Technology.ORCID iD: 0000-0002-0377-5595
SICS.ORCID iD: 0000-0003-3434-5640
KTH Royal Institute of Technology.ORCID iD: 0000-0001-5432-6442
2013 (English)In: Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, Springer, 2013, p. 276-291Chapter in book (Refereed)
Abstract [en]

In this paper, we formally verify security properties of the ARMv7 Instruction Set Architecture (ISA) for user mode executions. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. This work establishes a main requirement for operating system and hypervisor verification, as demonstrated for the PROSPER separation kernel. The proof is performed in the HOL4 theorem prover, taking the Cambridge model of ARM as basis. To this end, a proof tool has been developed, which assists the verification of relational state predicates semi-automatically.

Place, publisher, year, edition, pages
Springer, 2013. p. 276-291
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8307
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:lnu:diva-42250DOI: 10.1007/978-3-319-03545-1_18ISBN: 978-3-319-03544-4 (print)OAI: oai:DiVA.org:lnu-42250DiVA, id: diva2:803854
Conference
Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013
Available from: 2015-04-13 Created: 2015-04-13 Last updated: 2018-01-11Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Khakpour, NargesSchwartz, OliverDam, Mads

Search in DiVA

By author/editor
Khakpour, NargesSchwartz, OliverDam, Mads
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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