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
Compositional Verification of Security Properties for Embedded Execution Platforms
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0003-4889-8326
RISE SICS.ORCID iD: 0000-0003-3434-5640
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. (TCS)ORCID iD: 0000-0001-5432-6442
2017 (English)In: PROOFS 2017: 6th International Workshop on Security Proofs for Embedded Systems / [ed] Ulrich Kühne and Jean-Luc Danger and Sylvain Guilley, 2017, Vol. 49, p. 1-16Conference paper, Published paper (Refereed)
Abstract [en]

The security of embedded systems can be dramatically improved through the use of formally verified isolation mechanisms such as separation kernels, hypervisors, or microkernels. For trustworthiness, particularly for system level behaviour, the verifications need precise models of the underlying hardware. Such models are hard to attain, highly complex, and proofs of their security properties may not easily apply to similar but different platforms. This may render verification economically infeasible. To address these issues, we propose a compositional top-down approach to embedded system specification and verification, where the system-on-chip is modeled as a network of distributed automata communicating via paired synchronous message passing. Using abstract specifications for each component allows to delay the development of detailed models for cores, devices, etc., while still being able to verify high level security properties like integrity and confidentiality, and soundly refine the result for different instantiations of the abstract components at a later stage. As a case study, we apply this methodology to the verification of information flow security for an industry scale security-oriented hypervisor on the ARMv8-A platform. The hypervisor statically assigns (multiple) cores to each guest system and implements a rudimentary, but usable, inter guest communication discipline. We have completed a pen-and-paper security proof for the hypervisor down to state transition level and report on a partially completed verification of guest mode security in the HOL4 theorem prover.

Place, publisher, year, edition, pages
2017. Vol. 49, p. 1-16
Series
EPiC Series in Computing, ISSN 2398-7340
Keyword [en]
ARMv8, hardware platform, formal verification, hypervisor, decomposition, SoC, system security
National Category
Computer Systems Embedded Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-215208OAI: oai:DiVA.org:kth-215208DiVA, id: diva2:1147002
Conference
PROOFS 2017. 6th International Workshop on Security Proofs for Embedded Systems
Projects
HASPOCPROSPERCERCES
Funder
Swedish Civil Contingencies AgencyVINNOVASwedish Foundation for Strategic Research
Note

QC 20171009

Available from: 2017-10-04 Created: 2017-10-04 Last updated: 2018-01-03Bibliographically approved

Open Access in DiVA

fulltext(1004 kB)34 downloads
File information
File name FULLTEXT01.pdfFile size 1004 kBChecksum SHA-512
78dfeadc178cfc06b482718bd16fc3c01f4f28ba964b65c9c737abb095517f9103dc430be665f99388024e00ad5b8d9112c63c17518dea0433e98d0f37071c23
Type fulltextMimetype application/pdf

Other links

Published version

Search in DiVA

By author/editor
Baumann, ChristophSchwarz, OliverDam, Mads
By organisation
Theoretical Computer Science, TCS
Computer SystemsEmbedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 34 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 119 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