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
Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
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.ORCID iD: 0000-0003-4889-8326
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
2016 (English)In: Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016, Institute of Electrical and Electronics Engineers (IEEE), 2016, 38-55 p.Conference paper, Published paper (Refereed)
Abstract [en]

Caches pose a significant challenge to formal proofs of security for code executing on application processors, as the cache access pattern of security-critical services may leak secret information. This paper reveals a novel attack vector, exposing a low-noise cache storage channel that can be exploited by adapting well-known timing channel analysis techniques. The vector can also be used to attack various types of security-critical software such as hypervisors and application security monitors. The attack vector uses virtual aliases with mismatched memory attributes and self-modifying code to misconfigure the memory system, allowing an attacker to place incoherent copies of the same physical address into the caches and observe which addresses are stored in different levels of cache. We design and implement three different attacks using the new vector on trusted services and report on the discovery of an 128-bit key from an AES encryption service running in TrustZone on Raspberry Pi 2. Moreover, we subvert the integrity properties of an ARMv7 hypervisor that was formally verified against a cache-less model. We evaluate well-known countermeasures against the new attack vector and propose a verification methodology that allows to formally prove the effectiveness of defence mechanisms on the binary code of the trusted software.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2016. 38-55 p.
Keyword [en]
cache storage channels, hypervisor, side channels, verification, Application programs, Codes (symbols), Cryptography, Physical addresses, Side channel attack, Vectors, Virtual addresses, Application processors, Application security, Defence mechanisms, Design and implements, Side-channel, Storage channels, Verification methodology, Cache memory
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:kth:diva-194955DOI: 10.1109/SP.2016.11ISI: 000387292800003Scopus ID: 2-s2.0-84987617492ISBN: 9781509008247 (print)OAI: oai:DiVA.org:kth-194955DiVA: diva2:1049063
Conference
2016 IEEE Symposium on Security and Privacy, SP 2016, 23 May 2016 through 25 May 2016
Projects
PROSPER, CERCES
Funder
Swedish Foundation for Strategic Research
Note

QC 20161123

Available from: 2016-11-23 Created: 2016-11-01 Last updated: 2017-10-06Bibliographically 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 Science
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: 2017-09-29Bibliographically approved

Open Access in DiVA

fulltext(371 kB)1 downloads
File information
File name FULLTEXT01.pdfFile size 371 kBChecksum SHA-512
03d716eee702c24bbaf5b969319120e62f9e1cdd6c8c0b8a4afade89f6b9cf51fcd7ab4b7513f78e2c32077b97c617de50b7cd63a07488a58a19f5a1054adcf1
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Guanciale, RobertoNemati, HamedBaumann, ChristophDam, Mads
By organisation
Theoretical Computer Science, TCS
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

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

Altmetric score

Total: 62 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