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 Analysis of Countermeasures against Cache Storage Side Channels
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-9251-3679
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH Royal Institute of Technology.ORCID iD: 0000-0001-5432-6442
2017 (English)Manuscript (preprint) (Other academic)
Place, publisher, year, edition, pages
2017.
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-213405OAI: oai:DiVA.org:kth-213405DiVA: diva2:1137182
Conference
-
Note

QC 20170830

Available from: 2017-08-30 Created: 2017-08-30 Last updated: 2018-01-13Bibliographically approved
In thesis
1. Secure System Virtualization: End-to-End Verification of Memory Isolation
Open this publication in new window or tab >>Secure System Virtualization: End-to-End Verification of Memory Isolation
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Over the last years, security-kernels have played a promising role in reshaping the landscape of platform security on embedded devices. Security-kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms on a small TCB, which enforces isolation between components. The reduced TCB  minimizes the system attack surface and facilitates the use of formal methods to ensure the kernel functional correctness and security.

In this thesis, we explore various aspects of building a provably secure separation kernel using virtualization technology. We show how the memory management subsystem can be virtualized to enforce isolation of system components. Virtualization is done using direct-paging that enables a guest software to manage its own memory configuration. We demonstrate the soundness of our approach by verifying that the high-level model of the system fulfills the desired security properties. Through refinement, we then propagate these properties (semi-)automatically to the machine-code of the virtualization mechanism.

Further, we show how a runtime monitor can be securely deployed alongside a Linux guest on a hypervisor to prevent code injection attacks targeting Linux. The monitor takes advantage of the provided separation to protect itself and to retain a complete view of the guest.

Separating components using a low-level software cannot by itself guarantee the system security. Indeed, current processors architecture involves features that can be utilized to violate the isolation of components. We present a new low-noise attack vector constructed by measuring caches effects which is capable of breaching isolation of components and invalidates the verification of a software that has been verified on a memory coherent model. To restore isolation, we provide several countermeasures and propose a methodology to repair the verification by including data-caches in the statement of the top-level security properties of the system.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2017. 51 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2017:18
Keyword
Platform Security, Hypervisor, Formal Verification, Theorem Proving, HOL4, Cache attack, Security Monitor, Information Flow
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-213030 (URN)978-91-7729-478-8 (ISBN)
Public defence
2017-10-20, Kollegiesalen, Brinellvägen 8, Stockholm, 14:00 (English)
Opponent
Supervisors
Projects
PROSPERHASPOC
Funder
Swedish Foundation for Strategic Research , 6561
Note

QC 20170831

Available from: 2017-08-31 Created: 2017-08-28 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

No full text

Authority records BETA

Nemati, HamedGuanciale, RobertoDam, Mads

Search in DiVA

By author/editor
Nemati, HamedGuanciale, RobertoBaumann, ChristophDam, Mads
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

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