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
Trustworthy prevention of code injection in Linux on embedded devices
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.ORCID iD: 0000-0001-5432-6442
Show others and affiliations
2015 (English)In: 20th European Symposium on Research in Computer Security, ESORICS 2015, Springer, 2015, 90-107 p.Conference paper, Published paper (Refereed)
Resource type
Text
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.

Place, publisher, year, edition, pages
Springer, 2015. 90-107 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9326
Keyword [en]
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
National Category
Computer Systems
Identifiers
URN: urn:nbn:se:kth:diva-181591DOI: 10.1007/978-3-319-24174-6_5ISI: 000374478000005Scopus ID: 2-s2.0-84951274986ISBN: 9783319241739 (print)OAI: oai:DiVA.org:kth-181591DiVA: diva2:900571
Conference
20th European Symposium on Research in Computer Security, ESORICS 2015; Vienna; Austria
Funder
Swedish Foundation for Strategic Research
Note

QC 20160204

Available from: 2016-02-04 Created: 2016-02-02 Last updated: 2017-08-28Bibliographically 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(953 kB)83 downloads
File information
File name FULLTEXT01.pdfFile size 953 kBChecksum SHA-512
2481da688a7bab70290746dfd551071529037cb6052aa56a32bd9b7317b41a5bf4915962dde176e97a63ca43e542d0c9dedc088486917b8571dd654e8901cbbf
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Authority records BETA

Nemati, HamedDam, Mads

Search in DiVA

By author/editor
Nemati, HamedGuanciale, RobertoDam, Mads
By organisation
Theoretical Computer Science, TCS
Computer Systems

Search outside of DiVA

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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 175 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