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
Formal Verification of Secure User Mode Device Execution with DMA
RISE., Swedish ICT, SICS, Security Lab.ORCID-id: 0000-0003-3434-5640
KTH Royal Institute of Technology, Sweden.
2014 (engelsk)Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

Separation between processes on top of an operating system or between guests in a virtualized environment is essential for establishing security on modern platforms. A key requirement of the underlying hardware is the ability to support multiple partitions executing on the shared hardware without undue interference. For modern processor architectures - with hardware support for memory management, several modes of operation and I/O interfaces - this is a delicate issue requiring deep analysis at both instruction set and processor implementation level. In a first attempt to rigorously answer this type of questions we introduced in previous work an information flow analysis of user program execution on an ARMv7 platform with hardware supported memory protection, but without I/O. The analysis was performed as a semi-automatic proof search procedure on top of an ARMv7 ISA model implemented in the Cambridge HOL4 theorem prover by Fox et al. The restricted platform functionality, however, makes the analysis of limited practical value. In this paper we add support for devices, including DMA, to the analysis. To this end, we propose an approach to device modeling based on the idea of executing devices nondeterministically in parallel with the (single-core) deterministic processor, covering a fine granularity of interactions between the model components. Based on this model and taking the ARMv7 ISA as an example, we provide HOL4 proofs of several noninterference-oriented isolation properties for a partition executing in the presence of devices which potentially use DMA or interrupts.

sted, utgiver, år, opplag, sider
2014, 9. Vol. 8855, s. 236-251
Emneord [en]
peripheral devices, DMA, separation, isolation, user mode execution, ARM, formal hardware/software co-verification, theorem proving, HOL4
HSV kategori
Identifikatorer
URN: urn:nbn:se:ri:diva-24374DOI: 10.1007/978-3-319-13338-6_18Scopus ID: 2-s2.0-84921419001ISBN: 9783319133379 (tryckt)OAI: oai:DiVA.org:ri-24374DiVA, id: diva2:1043455
Konferanse
Haifa Verification Conference
Prosjekter
Provably Secure Execution Platforms for Embedded Systems
Merknad

This is the author version of the correspondent paper published in “Hardware and Software: Verification and Testing”, the proceedings of HVC 2014 (editor: Eran Yahav), Springer LNCS 8855. The publisher is Springer International Publishing Switzerland. The final publication is available at http://link.springer.com/10.1007/978-3-319-13338-6_18.

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

Open Access i DiVA

fulltext(504 kB)255 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 504 kBChecksum SHA-512
f9e4939472e39eebb91507c0ee11ca30f7453ba79116612be113e8ce97a44b006f0cd1bb09a5a8b53655687dc0c5804beeae5f989d8776333e739ec317fa1fbf
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: 255 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
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 89 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