Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
RISE., Swedish ICT, SICS, Security Lab.ORCID-id: 0000-0003-3434-5640
2013 (engelsk)Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
2013, 9. s. 276-291
Emneord [en]
ARM instruction set, noninterference, user mode execution, kernel security, theorem proving
HSV kategori
Identifikatorer
URN: urn:nbn:se:ri:diva-24275OAI: oai:DiVA.org:ri-24275DiVA, id: diva2:1043355
Konferanse
Certified Programs and Proofs (CPP)
Prosjekter
PROSPER
Merknad

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 http://link.springer.com/10.1007/978-3-319-03545-1_18.

Tilgjengelig fra: 2016-10-31 Laget: 2016-10-31 Sist oppdatert: 2020-01-30bibliografisk kontrollert

Open Access i DiVA

fulltext(393 kB)65 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 393 kBChecksum SHA-512
78009a043cca9957568353eff17128088f3d33289edbf8674c43a275362444c59accaf96717a29e7727c1983ece6b5896fa8724ae9a5509bf9ef8300513c3a51
Type fulltextMimetype application/pdf

Andre lenker

http

Personposter BETA

Schwarz, Oliver

Søk i DiVA

Av forfatter/redaktør
Schwarz, Oliver
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 65 nedlastinger
Antall nedlastinger er summen av alle nedlastinger av alle fulltekster. Det kan for eksempel være tidligere versjoner som er ikke lenger tilgjengelige

urn-nbn

Altmetric

urn-nbn
Totalt: 47 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
v. 2.35.9