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
On the verification of system-level information flow properties for virtualized execution platforms
(Ericsson Research)ORCID iD: 0000-0003-4889-8326
(RISE SICS)ORCID iD: 0000-0003-3434-5640
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
2019 (English)In: Journal of Cryptographic Engineering, ISSN 2190-8508, Vol. 9, no 3, p. 243-261Article in journal (Refereed) Published
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 behavior, 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 and report on the complete verification of guest mode security properties in the HOL4 theorem prover.

Place, publisher, year, edition, pages
Springer, 2019. Vol. 9, no 3, p. 243-261
Keywords [en]
Decomposition, SoC, information flow security, formal verification, hypervisor, ARMv8
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-263686DOI: 10.1007/s13389-019-00216-4Scopus ID: 2-s2.0-85067694646OAI: oai:DiVA.org:kth-263686DiVA, id: diva2:1368718
Projects
trustfull
Funder
Swedish Foundation for Strategic Research
Note

QC 20191111

Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2019-11-11Bibliographically approved

Open Access in DiVA

fulltext(532 kB)8 downloads
File information
File name FULLTEXT01.pdfFile size 532 kBChecksum SHA-512
2c71073a0dc96da6310a0af0ff1c62dae06cc51116bd8724f044cef51e44832bb149b9cc177986751ff099bfa38dd156204c9a0b34b920678a5a722e3572a7a8
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopushttps://link.springer.com/article/10.1007%2Fs13389-019-00216-4

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 8 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

doi
urn-nbn

Altmetric score

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