Who: Catalin Hritcu from Inria Paris, France
When: 14:00 - 15:00 Thursday 05 December 2019
Where: Room ES52, Linsen (Maskingränd 2).
Title: When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
We propose a new formal criterion for evaluating secure compartmentalization schemes for unsafe languages like C and C++, expressing end-to-end security guarantees for software components that may become compromised after 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 privileges. It articulates how each component should be protected from all the others—in particular, from components that have encountered undefined behavior and become compromised. To illustrate the model, we construct a secure compilation chain for a small unsafe language with buffers, procedures, and components, targeting a simple abstract machine with built-in compartmentalization. We propose a novel proof technique and give a machine-checked proof in Coq that this compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or a tag-based reference monitor.
Catalin 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, security protocols, integrity, information flow), programming languages (program verification, proof assistants, type systems, semantics, formal metatheory, certified tools, property-based testing), and the design and verification of security-critical systems (reference monitors, secure compilation chains, secure hardware). He was awarded an ERC Starting Grant on formally secure compilation (https://secure-compilation.github.io), and is also actively involved in the design of the F* verification system (https://www.fstar-lang.org/), which is used for building a formally verified HTTPS stack (https://project-everest.github.io). Catalin received a PhD from Saarland University in Saarbrücken, a Habilitation from ENS Paris, and was previously also a Research Associate at University of Pennsylvania and a Visiting Researcher at Microsoft Research Redmond.
- Chalmers Security Seminar · When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise
- Chalmers Security Seminar · Risk Analysis of Privacy Policies
- Chalmers Security Seminar · The Simplest Multi-key Linearly Homomorphic Signature Scheme
- Chalmers Security Seminar · The Rush Dilemma: Attacking and Repairing Smart Contracts on Forking Blockchains
- Chalmers Security Seminar · SAID: Reshaping Signal into an Identity-Based Asynchronous Messaging Protocol with Authenticated Ratcheting
- Chalmers Security Seminar · Trusted Execution Environments for Privacy-preserving Cloud Applications
- Chalmers Security Seminar · CLIO: Cryptographically Secure Information Flow Control on Key-Value Stores
- Chalmers Security Seminar · Historical Analyses of the Client-Side Web Security and How to tell people they have an issue
- Chalmers Security Seminar · Recent work on probabilistic programming languages
- Chalmers Security Seminar · Privacy and security threat modeling: current research directions
- Chalmers Security Seminar · Security and Privacy on Medical Devices
- Chalmers Security Seminar · ZKBoo: Faster Zero-Knowledge for Boolean Circuits
- Chalmers Security Seminar · Enhancing the COWL W3C Standard
- Chalmers Security Seminar · Selene: Voting with Transparent Verification and Coercion Mitigation
- Chalmers Security Seminar · Verification of differential private computationss
- Chalmers Security Seminar · Privacy engineering: from the building blocks to the system
- Chalmers Security Seminar · Architectural requirements for language-level control of external timing channels
- Chalmers Security Seminar · Security of login pages on the Web: who else can know your password?
- Chalmers Security Seminar · Program behavior-based fuzzing and vulnerability discovery
- Chalmers Security Seminar · Two Can Keep a Secret, If One of Them Uses Haskell
- Chalmers Security Seminar · Recent Breakthroughs in Obfuscation
- Chalmers Security Seminar · Formal Security Analysis of Mobile and Web Applications
- Chalmers Security Seminar · Anonymization of sparse multidimensional data
- Chalmers Security Seminar · Daniel Hausknecht's Licentiate presentation
- Chalmers Security Seminar · Towards more secure and usable text passwords
- Chalmers Security Seminar · Establishing and Maintaining Root of Trust on Commodity Computer Systems