Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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 integrity-Preserving countermeasures against cache storage side-channels
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
2018 (English)In: 7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Springer, 2018, Vol. 10804, p. 109-133Conference paper, Published paper (Refereed)
Abstract [en]

Formal verification of systems-level software such as hypervisors and operating systems can enhance system trustworthiness. However, without taking low level features like caches into account the verification may become unsound. While this is a well-known fact w.r.t. timing leaks, few works have addressed latent cache storage side-channels, whose effects are not limited to information leakage. We present a verification methodology to analyse soundness of countermeasures used to neutralise these channels. We apply the proposed methodology to existing countermeasures, showing that they allow to restore integrity of the system. We decompose the proof effort into verification conditions that allow for an easy adaption of our strategy to various software and hardware platforms. As case study, we extend the verification of an existing hypervisor whose integrity can be tampered using cache storage channels. We used the HOL4 theorem prover to validate our security analysis, applying the verification methodology to a generic hardware model. 

Place, publisher, year, edition, pages
Springer, 2018. Vol. 10804, p. 109-133
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10804
Keywords [en]
Cache memory, Hardware, Network security, Hardware models, Information leakage, Low-level features, Security analysis, Software and hardwares, Storage channels, Verification condition, Verification methodology, Formal verification
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-227490DOI: 10.1007/978-3-319-89722-6_5ISI: 000445805600005Scopus ID: 2-s2.0-85045658183ISBN: 9783319897219 (print)OAI: oai:DiVA.org:kth-227490DiVA, id: diva2:1206183
Conference
7th International Conference on Principles of Security and Trust, POST 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018; Thessaloniki; Greece; 14 April 2018 through 20 April 2018
Projects
trustfullcerces
Note

QC 20180516

QC 20181012

Available from: 2018-05-16 Created: 2018-05-16 Last updated: 2019-11-20Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Baumann, ChristophGuanciale, RobertoDam, Mads

Search in DiVA

By author/editor
Baumann, ChristophGuanciale, RobertoDam, Mads
By organisation
Theoretical Computer Science, TCS
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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