Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Visa övriga samt affilieringar
2013 (Engelska)Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a simple separation kernel for ARMv7. Previous work on information flow kernel security leaves communication to be handled by model-external means, and cannot be used to draw conclusions when there is explicit interaction between partitions. We propose a different approach where communication between partitions is made explicit and the information flow is analyzed in the presence of such a channel. Limiting the kernel functionality as much as meaning-fully possible, we accomplish a detailed analysis and verification of the system, proving its correctness at the level of the ARMv7 assembly. As a sanity check we show how the security condition is reduced to noninterference in the special case where no communication takes place. The verification is done in HOL4 taking the Cambridge model of ARM as basis, transferring verification tasks on the actual assembly code to an adaptation of the BAP binary analysis tool developed at CMU.

Ort, förlag, år, upplaga, sidor
2013, 10. s. 223-234
Nyckelord [en]
Formal verification, Information Flow Security, Separation Kernel, Hypervisor
Nationell ämneskategori
Data- och informationsvetenskap
Identifikatorer
URN: urn:nbn:se:ri:diva-24266DOI: 10.1145/2508859.2516702OAI: oai:DiVA.org:ri-24266DiVA, id: diva2:1043346
Konferens
2013 ACM SIGSAC conference on computer & communications security
Projekt
PROSPERTillgänglig från: 2016-10-31 Skapad: 2016-10-31 Senast uppdaterad: 2018-08-15Bibliografiskt granskad

Open Access i DiVA

fulltext(417 kB)31 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 417 kBChecksumma SHA-512
dcbd84b702236c0bdb1c4ebf63102bc46e3aaf9bb9913512c33c9d40610d62888c451057204fcefc3547d45461ba3887839ae3e0eada16a9a2b935ddec92360e
Typ fulltextMimetyp application/pdf

Övriga länkar

Förlagets fulltexthttp

Personposter BETA

Schwarz, Oliver

Sök vidare i DiVA

Av författaren/redaktören
Schwarz, Oliver
Av organisationen
Security Lab
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 31 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 34 träffar
RefereraExporteraLänk till posten
Permanent länk

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