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
On the verification of system-level information flow properties for virtualized execution platforms
Ericsson Research Security, Sweden.
RISE - Research Institutes of Sweden, ICT, SICS.ORCID-id: 0000-0003-3434-5640
KTH Royal Institute of Technology, Sweden.
2019 (engelsk)Inngår i: Journal of Cryptographic Engineering, ISSN 2190-8508, Vol. 9, nr 3, s. 243-261Artikkel i tidsskrift (Fagfellevurdert) 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.

sted, utgiver, år, opplag, sider
Springer Verlag , 2019. Vol. 9, nr 3, s. 243-261
Emneord [en]
ARMv8, Decomposition, Formal verification, Hypervisor, Information flow security, SoC, ARM processors, Embedded systems, Message passing, Network security, Programmable logic controllers, Specifications, System-on-chip, Abstract specifications, Embedded system specifications, Execution platforms, Security properties, Top down approaches
HSV kategori
Identifikatorer
URN: urn:nbn:se:ri:diva-39556DOI: 10.1007/s13389-019-00216-4Scopus ID: 2-s2.0-85067694646OAI: oai:DiVA.org:ri-39556DiVA, id: diva2:1335978
Tilgjengelig fra: 2019-07-08 Laget: 2019-07-08 Sist oppdatert: 2020-01-30bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Person

Schwarz, Oliver

Søk i DiVA

Av forfatter/redaktør
Schwarz, Oliver
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

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