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
KTH Royal Institute of Technology, Sweden.
RISE., Swedish ICT, SICS, Security Lab. KTH Royal Institute of Technology, Sweden.ORCID-id: 0000-0003-3434-5640
KTH Royal Institute of Technology, Sweden.
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, artikkel-id 8307
Emneord [en]
ARM instruction set, noninterference, user mode execution, kernel security, theorem proving
HSV kategori
Identifikatorer
URN: urn:nbn:se:ri:diva-24275DOI: 10.1007/978-3-319-03545-1_18Scopus ID: 2-s2.0-84893128835OAI: oai:DiVA.org:ri-24275DiVA, id: diva2:1043355
Konferanse
Certified Programs and Proofs (CPP)
Prosjekter
PROSPERTilgjengelig fra: 2016-10-31 Laget: 2016-10-31 Sist oppdatert: 2020-12-01bibliografisk kontrollert

Open Access i DiVA

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

Andre lenker

Forlagets fulltekstScopushttp

Person

Schwarz, Oliver

Søk i DiVA

Av forfatter/redaktør
Schwarz, Oliver
Av organisasjonen

Søk utenfor DiVA

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

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 86 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.43.0