de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

A Formal Model for Capability Machines An Illustrative Case Study towards Secure Compilation to CHERI

MPS-Authors

El-Korashy,  Akram
International Max Planck Research School, MPI for Informatics, Max Planck Society;

Patrignani,  Marco
Max Planck Institute for Software Systems, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons144522

Garg,  Deepak
Max Planck Institute for Software Systems, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

El-Korashy, A. (2016). A Formal Model for Capability Machines An Illustrative Case Study towards Secure Compilation to CHERI. Master Thesis, Universität des Saarlandes, Saarbrücken.


Cite as: http://hdl.handle.net/11858/00-001M-0000-002C-41CA-B
Abstract
Vulnerabilities in computer systems arise in part due to programmer's logical errors, and in part also due to programmer's false (i.e., over-optimistic) expectations about the guarantees that are given by the abstractions of a programming language. For the latter kind of vulnerabilities, architectures with hardware or instructionlevel support for protection mechanisms can be useful. One trend in computer systems protection is hardware-supported enforcement of security guarantees/policies. Capability-based machines are one instance of hardware-based protection mechanisms. CHERI is a recent implementation of a 64-bit MIPS-based capability architecture with byte-granularity memory protection. The goal of this thesis is to provide a paper formal model of the CHERI architecture with the aim of formal reasoning about the security guarantees that can be offered by the features of CHERI. We first give simplified instruction operational semantics, then we prove that capabilities are unforgeable in our model. Second, we show that existing techniques for enforcing control-flow integrity can be adapted to the CHERI ISA. Third, we show that one notion of memory compartmentalization can be achieved with the help of CHERI's memory protection. We conclude by suggesting other security building blocks that would be helpful to reason about, and laying down a plan for potentially using this work for building a secure compiler, i.e., a compiler that preserves security properties. The outlook and motivation for this work is to highlight the potential of using CHERI as a target architecture for secure compilation.