Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • 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
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
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-0003-3434-5640
KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.ORCID iD: 0000-0001-5432-6442
2013 (English)In: Certified Programs and Proofs: Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, Springer, 2013, 276-291 p.Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we formally verify security properties of the ARMv7 Instruction Set Architecture (ISA) for user mode executions. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. This work establishes a main requirement for operating system and hypervisor verification, as demonstrated for the PROSPER separation kernel. The proof is performed in the HOL4 theorem prover, taking the Cambridge model of ARM as basis. To this end, a proof tool has been developed, which assists the verification of relational state predicates semi-automatically.

Place, publisher, year, edition, pages
Springer, 2013. 276-291 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8307
Keyword [en]
ARM instruction set, noninterference, user mode execution, kernel security, theorem proving
National Category
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-136354DOI: 10.1007/978-3-319-03545-1_18Scopus ID: 2-s2.0-84893128835ISBN: 978-3-319-03544-4 (print)ISBN: 978-3-319-03545-1 (print)OAI: oai:DiVA.org:kth-136354DiVA: diva2:675843
Conference
Certified Programs and Proofs (CPP)
Projects
PROSPER
Funder
Swedish Foundation for Strategic Research
Note

The provided file is the author version of the correspondent paper published in the proceedings of Certified Programs and Proofs 2013 (CPP; editors: G. Gonthier and M. Norrish), Springer LNCS 8307. The publisher and copyright holder is Springer International Publishing Switzerland. The final publication is available at http://link.springer.com/10.1007/978-3-319-03545-1_18. QC 20140624

Available from: 2013-12-04 Created: 2013-12-04 Last updated: 2016-09-12Bibliographically approved
In thesis
1. No Hypervisor Is an Island: System-wide Isolation Guarantees for Low Level Code
Open this publication in new window or tab >>No Hypervisor Is an Island: System-wide Isolation Guarantees for Low Level Code
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The times when malware was mostly written by curious teenagers are long gone. Nowadays, threats come from criminals, competitors, and government agencies. Some of them are very skilled and very targeted in their attacks. At the same time, our devices – for instance mobile phones and TVs – have become more complex, connected, and open for the execution of third-party software. Operating systems should separate untrusted software from confidential data and critical services. But their vulnerabilities often allow malware to break the separation and isolation they are designed to provide. To strengthen protection of select assets, security research has started to create complementary machinery such as security hypervisors and separation kernels, whose sole task is separation and isolation. The reduced size of these solutions allows for thorough inspection, both manual and automated. In some cases, formal methods are applied to create mathematical proofs on the security of these systems.

The actual isolation solutions themselves are carefully analyzed and included software is often even verified on binary level. The role of other software and hardware for the overall system security has received less attention so far. The subject of this thesis is to shed light on these aspects, mainly on (i) unprivileged third-party code and its ability to influence security, (ii) peripheral devices with direct access to memory, and (iii) boot code and how we can selectively enable and disable isolation services without compromising security.

The papers included in this thesis are both design and verification oriented, however, with an emphasis on the analysis of instruction set architectures. With the help of a theorem prover, we implemented various types of machinery for the automated information flow analysis of several processor architectures. The analysis is guaranteed to be both sound and accurate.

Abstract [sv]

Förr skrevs skadlig mjukvara mest av nyfikna tonåringar. Idag är våra datorer under ständig hot från statliga organisationer, kriminella grupper, och kanske till och med våra affärskonkurrenter. Vissa besitter stor kompetens och kan utföra fokuserade attacker. Samtidigt har tekniken runtomkring oss (såsom mobiltelefoner och tv-apparater) blivit mer komplex, uppkopplad och öppen för att exekvera mjukvara från tredje part.

Operativsystem borde egentligen isolera känslig data och kritiska tjänster från mjukvara som inte är trovärdig. Men deras sårbarheter gör det oftast möjligt för skadlig mjukvara att ta sig förbi operativsystemens säkerhetsmekanismer. Detta har lett till utveckling av kompletterande verktyg vars enda funktion är att förbättra isolering av utvalda känsliga resurser. Speciella virtualiseringsmjukvaror och separationskärnor är exempel på sådana verktyg. Eftersom sådana lösningar kan utvecklas med relativt liten källkod, är det möjligt att analysera dem noggrant, både manuellt och automatiskt. I några fall används formella metoder för att generera matematiska bevis på att systemet är säkert.

Själva isoleringsmjukvaran är oftast utförligt verifierad, ibland till och med på assemblernivå. Dock så har andra komponenters påverkan på systemets säkerhet hittills fått mindre uppmärksamhet, både när det gäller hårdvara och annan mjukvara. Den här avhandlingen försöker belysa dessa aspekter, huvudsakligen (i) oprivilegierad kod från tredje part och hur den kan påverka säkerheten, (ii) periferienheter med direkt tillgång till minnet och (iii) startkoden, samt hur man kan aktivera och deaktivera isolationstjänster på ett säkert sätt utan att starta om systemet.

Avhandlingen är baserad på sex tidigare publikationer som handlar om både design- och verifikationsaspekter, men mest om säkerhetsanalys av instruktionsuppsättningar. Baserat på en teorembevisare har vi utvecklat olika verktyg för den automatiska informationsflödesanalysen av processorer. Vi har använt dessa verktyg för att tydliggöra vilka register oprivilegierad mjukvara har tillgång till på ARM- och MIPS-maskiner. Denna analys är garanterad att vara både korrekt och precis. Så vitt vi vet är vi de första som har publicerat en lösning för automatisk analys och bevis av informationsflödesegenskaper i standardinstruktionsuppsättningar.

Place, publisher, year, edition, pages
Stockholm: KTH Royal Institute of Technology, 2016. 180 p.
Series
TRITA-CSC-A, ISSN 1653-5723 ; 2016:22
Series
SICS Dissertation Series, ISSN 1101-1335 ; 75
Keyword
Platform Security, Hypervisor, Formal Verification, Theorem Proving, HOL4, DMA, Peripheral Devices, Instruction Set Architectures, ISA, Information Flow, Boot
National Category
Computer Science
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-192466 (URN)978-91-7729-104-6 (ISBN)
Public defence
2016-10-10, F3, Lindstedtsvägen 26, Stockholm, 14:00 (English)
Opponent
Supervisors
Projects
PROSPERHASPOC
Funder
Swedish Foundation for Strategic Research VINNOVA
Note

QC 20160919

Available from: 2016-09-19 Created: 2016-09-12 Last updated: 2017-11-24Bibliographically approved

Open Access in DiVA

ARM_ISA_verification_Khakpour_author_version.pdf(899 kB)143 downloads
File information
File name FULLTEXT01.pdfFile size 899 kBChecksum SHA-512
f2abfb1da9437d53063b439c17f5318cecd7c022eab9f7904825c4f13a933a7669b4c99a1ae5ad7f9f8ac2f92c49dff4bad62743c1f8e78856a9d4a8613f3f0d
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopusThe final publication is available at www.springerlink.com

Search in DiVA

By author/editor
Khakpour, NargesSchwarz, OliverDam, Mads
By organisation
Theoretical Computer Science, TCS
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 143 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: 269 hits
CiteExportLink to record
Permanent link

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