Change search
ReferencesLink to record
Permanent link

Direct link
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
Number of Authors: 3
2013 (English)Conference paper (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
2013, 9. 276-291 p.
Keyword [en]
ARM instruction set, noninterference, user mode execution, kernel security, theorem proving
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-15462OAI: diva2:1036779
Certified Programs and Proofs (CPP)
This is the author version of the correspondent paper published in the proceedings of Certified Programs and Proofs 2013 (CPP; editors: G. Gonthier and M. Norrish), Springer LNCS 8307. The publisher is Springer International Publishing Switzerland . The final publication is available at from: 2016-10-13 Created: 2016-10-13

Open Access in DiVA

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

Other links


Search in DiVA

By author/editor
Khakpour, NargesDam, Mads
Computer and Information Science

Search outside of DiVA

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

ReferencesLink to record
Permanent link

Direct link