lnu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal verification of information flow security for a simple arm-based separation kernel
KTH Royal Institute of Technology.
KTH Royal Institute of Technology.
KTH Royal Institute of Technology.ORCID iD: 0000-0002-0377-5595
KTH Royal Institute of Technology.
Show others and affiliations
2013 (English)In: Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security, ACM Press, 2013, p. 223-234Conference paper, Published paper (Refereed)
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 meaningfully 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.

Place, publisher, year, edition, pages
ACM Press, 2013. p. 223-234
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:lnu:diva-42251DOI: 10.1145/2508859.2516702ISBN: 978-1-4503-2477-9 (print)OAI: oai:DiVA.org:lnu-42251DiVA, id: diva2:803855
Conference
The 2013 ACM SIGSAC conference on Computer & communications security
Available from: 2015-04-13 Created: 2015-04-13 Last updated: 2018-01-11Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Khakpour, Narges

Search in DiVA

By author/editor
Khakpour, Narges
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 67 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf