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, 276-291 p.Chapter 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. 276-291 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8307
National Category
Computer Science
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: 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: 2015-04-22Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 268 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