Max-Planck-Institut für Informatik
max planck institut
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:Efficient Formally Secure Compilers to a Tagged Architecture
Speaker:Catalin Hritcu
coming from:InRIA, Paris
Speakers Bio:Catalin is a tenured Research Scientist at Inria Paris where he develops rigorous formal techniques for solving security problems.

He is particularly interested in formal methods for security (memory safety, compartmentalization, access control, integrity, security
protocols, information flow), programming languages (type systems verification, proof assistants, property-based testing, semantics,
formal metatheory, certified tools, dynamic enforcement), and the design and verification of security-critical systems (reference
monitors, secure compilers, microkernels, secure hardware).  He is a developer of the new F* verification system and of several other open
source tools based on his research.  Catalin was a PhD student at Saarland University and a Research Associate at University of
Pennsylvania before joining Inria Paris in September 2013.

Event Type:SWS Colloquium
Visibility:SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Expert Audience
Date, Time and Location
Date:Monday, 22 February 2016
Duration:90 Minutes
Severe low-level vulnerabilities abound in today's computer systems, allowing cyber-attackers to remotely gain full control. This happens in big part because our programming languages, compilers, and architectures were designed in an era of scarce hardware resources and
too often trade off security for efficiency. The semantics of mainstream low-level languages like C is inherently insecure, and even for safer languages, establishing security with respect to a high-level semantics does not guarantee the absence of low-level
attacks. Secure compilation using the coarse-grained protection mechanisms provided by mainstream hardware architectures would be too inefficient for most practical scenarios.

In this talk I will present a new project that is aimed at leveraging emerging hardware capabilities for fine-grained protection to build the first, efficient secure compilers for realistic programming languages, both low-level (the C language) and high-level (ML and F*,
a dependently-typed variant). These compilers will provide a secure semantics for all programs and will ensure that high-level abstractions cannot be violated even when interacting with untrusted low-level code. To achieve this level of security without sacrificing
efficiency, our secure compilers target a novel tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules. Formally, our goal is full abstraction with respect to a secure
high-level semantics. This property is much stronger than just compiler correctness and ensures that no machine-code attacker can do more harm to securely compiled components than a component in the secure source language already could.
Name(s):Claudia Richter
Phone:9303 9103
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Saarbrücken
To Building:E1 5To Room:029
Tags, Category, Keywords and additional notes
Attachments, File(s):

Created:Claudia Richter/MPI-SWS, 02/15/2016 02:02 PM Last modified:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Claudia Richter, 02/15/2016 02:08 PM -- Created document.