Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:A formal model for capability machines: Towards secure compilation to CHERI
Speaker:Akram El-Korashy
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Qualifying Exam
Visibility:SWS
We use this to send out email in the morning.
Level:Expert Audience
Language:English
Date, Time and Location
Date:Thursday, 16 March 2017
Time:15:00
Duration:-- Not specified --
Location:Saarbr├╝cken
Building:E1 5
Room:029
Abstract
Vulnerabilities in computer systems often arise due to a mismatch between the abstractions that a high-level programming language offers and the actual low-level environment in which the compiled machine code executes. A low-level environment for example may offer only lax memory safety compared to the memory safety guarantee that the high-level programming language gives.

To address this mismatch, architectures with hardware or instruction-level 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.

In this talk, I discuss a formal model of the CHERI architecture, a capability machine architecture, with the aim of formal reasoning about the security guarantees that it offers. I discuss the notions of capability unforgeability, and memory compartmentalization which we showed can be achieved with the help of CHERI's protection mechanisms.

The motivation for this work is to highlight the potential of using CHERI as a target architecture for secure compilation, i.e., compilation that preserves security properties.
Contact
Name(s):
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
Created:
Maria-Louise Albrecht/MPI-KLSB, 05/19/2017 01:02 PM
Last modified:
Maria-Louise Albrecht/MPI-KLSB, 05/19/2017 01:09 PM
  • Maria-Louise Albrecht, 05/19/2017 01:09 PM -- Created document.