BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium: When Good Components Go Bad: Formally Secure Compil
 ation Despite Dynamic Compromise
DTSTART:20190926T161500
DTEND:20190926T173000
DTSTAMP:20260510T013139Z
UID:6b2cddb124878500bf00ca7fe0ad4f99c596f62e413cd220ba2b9160
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Catalin Hritcu - INRIA Paris\nVideo of his talk\n\nAbstrac
 t:\nWe propose a new formal criterion for evaluating secure compartmentali
 zation schemes for unsafe languages like C and C++\, expressing end-to-end
  security guarantees for software components that may become compromised a
 fter encountering undefined behavior---for example\, by accessing an array
  out of bounds. Our criterion is the first to model dynamic compromise in 
 a system of mutually distrustful components with clearly specified privile
 ges. It articulates how each component should be protected from all the ot
 hers---in particular\, from components that have encountered undefined beh
 avior and become compromised.\nTo illustrate the model\, we construct a se
 cure compilation chain for a small unsafe language with buffers\, procedur
 es\, and components\, targeting a simple abstract machine with built-in co
 mpartmentalization. We propose a novel proof technique and give a machine-
 checked proof in Coq that this compiler satisfies our secure compilation c
 riterion. Finally\, we show that the protection guarantees offered by the 
 compartmentalized abstract machine can be achieved at the machine-code lev
 el using either software fault isolation or a tag-based reference monitor.
 \n\nBio:\nCatalin Hritcu is a researcher at Inria Paris where he works on 
 security foundations. He is particularly interested in formal methods for 
 security (secure compilation\, compartmentalization\, memory safety\, secu
 rity protocols\, integrity\, information flow)\, programming languages (pr
 ogram verification\, proof assistants\, type systems\, semantics\, formal 
 metatheory\, certified tools\, property-based testing)\, and the design an
 d verification of security-critical systems (reference monitors\, secure c
 ompilation chains\, secure hardware). He was awarded an ERC Starting Grant
  on formally secure compilation (https://secure-compilation.github.io)\, a
 nd is also actively involved in the design of the F* verification system (
 https://www.fstar-lang.org/)\, which is used for building a formally verif
 ied HTTPS stack (https://project-everest.github.io). Catalin received a Ph
 D from Saarland University in Saarbrücken\, a Habilitation from ENS Paris
 \, and was previously also a Research Associate at University of Pennsylva
 nia and a Visiting Researcher at Microsoft Research Redmond.\n\nMore infor
 mation
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR