Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Secure System Virtualization: End-to-End Verification of Memory Isolation
KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.ORCID-id: 0000-0001-9251-3679
2017 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Stockholm: KTH Royal Institute of Technology, 2017. , 51 s.
Serie
TRITA-CSC-A, ISSN 1653-5723 ; 2017:18
Nyckelord [en]
Platform Security, Hypervisor, Formal Verification, Theorem Proving, HOL4, Cache attack, Security Monitor, Information Flow
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datalogi
Identifikatorer
URN: urn:nbn:se:kth:diva-213030ISBN: 978-91-7729-478-8 (tryckt)OAI: oai:DiVA.org:kth-213030DiVA: diva2:1136624
Disputation
2017-10-20, Kollegiesalen, Brinellvägen 8, Stockholm, 14:00 (Engelska)
Opponent
Handledare
Projekt
PROSPERHASPOC
Forskningsfinansiär
Stiftelsen för strategisk forskning (SSF), 6561
Anmärkning

QC 20170831

Tillgänglig från: 2017-08-31 Skapad: 2017-08-28 Senast uppdaterad: 2017-09-29Bibliografiskt granskad
Delarbeten
1. Provably secure memory isolation for Linux on ARM
Öppna denna publikation i ny flik eller fönster >>Provably secure memory isolation for Linux on ARM
2016 (Engelska)Ingår i: Journal of Computer Security, ISSN 0926-227X, E-ISSN 1875-8924, Vol. 24, nr 6, 793-837 s.Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation and verification of a memory virtualization platform for ARMv7-A processors. The design is based on direct paging, an MMU virtualization mechanism previously introduced by Xen. It is shown that this mechanism can be implemented using a compact design, suitable for formal verification down to a low level of abstraction, without penalizing system performance. The verification is performed using the HOL4 theorem prover and uses a detailed model of the processor. We prove memory isolation along with information flow security for an abstract top-level model of the virtualization mechanism. The abstract model is refined down to a transition system closely resembling a C implementation. Additionally, it is demonstrated how the gap between the low-level abstraction and the binary level-can be filled, using tools that check Hoare contracts. The virtualization mechanism is demonstrated on real hardware via a hypervisor hosting Linux and supporting a tamper-proof run-time monitor that provably prevents code injection in the Linux guest.

Ort, förlag, år, upplaga, sidor
IOS Press, 2016
Nyckelord
Formal verification, information flow security, separation kernel, hypervisor
Nationell ämneskategori
Teknik och teknologier
Forskningsämne
Datalogi
Identifikatorer
urn:nbn:se:kth:diva-197900 (URN)10.3233/JCS-160558 (DOI)000389850600004 ()
Projekt
PROSPER, CERCES
Forskningsfinansiär
Stiftelsen för strategisk forskning (SSF)
Anmärkning

QC 20161212

Tillgänglig från: 2016-12-08 Skapad: 2016-12-08 Senast uppdaterad: 2017-10-06Bibliografiskt granskad
2. Trustworthy prevention of code injection in Linux on embedded devices
Öppna denna publikation i ny flik eller fönster >>Trustworthy prevention of code injection in Linux on embedded devices
Visa övriga...
2015 (Engelska)Ingår i: 20th European Symposium on Research in Computer Security, ESORICS 2015, Springer, 2015, 90-107 s.Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

We present MProsper, a trustworthy system to prevent code injection in Linux on embedded devices. MProsper is a formally verified run-time monitor, which forces an untrusted Linux to obey the executable space protection policy; a memory area can be either executable or writable, but cannot be both. The executable space protection allows the MProsper’s monitor to intercept every change to the executable code performed by a user application or by the Linux kernel. On top of this infrastructure, we use standard code signing to prevent code injection. MProsper is deployed on top of the Prosper hypervisor and is implemented as an isolated guest. Thus MProsper inherits the security property verified for the hypervisor: (i) Its code and data cannot be tampered by the untrusted Linux guest and (ii) all changes to the memory layout is intercepted, thus enabling MProsper to completely mediate every operation that can violate the desired security property. The verification of the monitor has been performed using the HOL4 theorem prover and by extending the existing formal model of the hypervisor with the formal specification of the high level model of the monitor.

Ort, förlag, år, upplaga, sidor
Springer, 2015
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9326
Nyckelord
Codes (symbols), Embedded systems, Linux, Security of data, Security systems, Systems analysis, Embedded device, Executable codes, High-level modeling, Protection policy, Security properties, Standard codes, Theorem provers, Trustworthy systems, Computer operating systems
Nationell ämneskategori
Datorsystem
Identifikatorer
urn:nbn:se:kth:diva-181591 (URN)10.1007/978-3-319-24174-6_5 (DOI)000374478000005 ()2-s2.0-84951274986 (Scopus ID)9783319241739 (ISBN)
Konferens
20th European Symposium on Research in Computer Security, ESORICS 2015; Vienna; Austria
Forskningsfinansiär
Stiftelsen för strategisk forskning (SSF)
Anmärkning

QC 20160204

Tillgänglig från: 2016-02-04 Skapad: 2016-02-02 Senast uppdaterad: 2017-08-28Bibliografiskt granskad
3. Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures
Öppna denna publikation i ny flik eller fönster >>Cache Storage Channels: Alias-Driven Attacks and Verified Countermeasures
2016 (Engelska)Ingår i: Proceedings - 2016 IEEE Symposium on Security and Privacy, SP 2016, Institute of Electrical and Electronics Engineers (IEEE), 2016, 38-55 s.Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Institute of Electrical and Electronics Engineers (IEEE), 2016
Nyckelord
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
Nationell ämneskategori
Elektroteknik och elektronik
Identifikatorer
urn:nbn:se:kth:diva-194955 (URN)10.1109/SP.2016.11 (DOI)000387292800003 ()2-s2.0-84987617492 (Scopus ID)9781509008247 (ISBN)
Konferens
2016 IEEE Symposium on Security and Privacy, SP 2016, 23 May 2016 through 25 May 2016
Projekt
PROSPER, CERCES
Forskningsfinansiär
Stiftelsen för strategisk forskning (SSF)
Anmärkning

QC 20161123

Tillgänglig från: 2016-11-23 Skapad: 2016-11-01 Senast uppdaterad: 2017-10-06Bibliografiskt granskad
4. Formal Analysis of Countermeasures against Cache Storage Side Channels
Öppna denna publikation i ny flik eller fönster >>Formal Analysis of Countermeasures against Cache Storage Side Channels
2017 (Engelska)Manuskript (preprint) (Övrigt vetenskapligt)
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
urn:nbn:se:kth:diva-213405 (URN)
Konferens
-
Anmärkning

QC 20170830

Tillgänglig från: 2017-08-30 Skapad: 2017-08-30 Senast uppdaterad: 2017-11-07Bibliografiskt granskad

Open Access i DiVA

fulltext(1241 kB)21 nedladdningar
Filinformation
Filnamn FULLTEXT02.pdfFilstorlek 1241 kBChecksumma SHA-512
f094f8e885dccc36bd1e60f7b15c5fed081afa0f67cd7f9140b21a71e483ce4accc01f652cdc93dd579c3c01c6f2dee689c634fccedcd8b450ee49a2e6250b8f
Typ fulltextMimetyp application/pdf

Personposter BETA

Nemati, Hamed

Sök vidare i DiVA

Av författaren/redaktören
Nemati, Hamed
Av organisationen
Teoretisk datalogi, TCS
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 21 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

isbn
urn-nbn

Altmetricpoäng

isbn
urn-nbn
Totalt: 1260 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf