Ruhr-Uni-Bochum
Cyber Security in the Age of Large-Scale Adversaries

CASA Distinguished Lectures

 

In den CASA Distinguished Lectures heißen wir ausgewählte international und nationale Wissenschaftler*innen am HGI willkommen.
An die meist einstündigen Vorträge dieser exzellenten Gastredner*innen schließt immer auch eine Diskussion mit den Teilnehmenden an. Damit möchten wir unser Ziel verwirklichen, einen regen Gedankenaustausch innerhalb der Cyber-Security-Forschung anzutreiben und neue Perspektiven zu öffnen.

Aufgrund der aktuellen Situation rund um die COVID-19-Epidemie werden die Lectures online abgehalten - und sind damit für Interessierte auf der ganzen Welt zugänglich. Der Zugangslink zur jeweiligen Veranstaltung wird unter den Informationen zu den Votragenden geteilt.

 

Service-Angebote zu den Distinguished Lectures

Auf unserem Youtube-Kanal können Sie sich einige vergangene Distinguished Lectures in voller Länge anschauen. Wenn Sie über die anstehenden Vorträge informiert werden möchten, melden Sie sich bitte zu unserem Newsletter an.

Catalin Hritcu (Inria Paris, Prosecco team)

"When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise"

Abstract. 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 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.

Biography. 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, type systems, proof assistants, 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/) and its use for building a formally verified HTTPS stack (https://project-everest.github.io).

Catalin received his PhD from Saarland University, supported by fellowships from the International Max Planck Research School for Computer Science and Microsoft Research Cambridge. Recently he received a Habilitation degree from ENS Paris, and was previously also a Research Associate at University of Pennsylvania and a Visiting Researcher at Microsoft Research Redmond.

Cyber Security in the Age of Large-Scale Adversaries

Catalin Hritcu (Inria Paris, Prosecco team)

"When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise"

Abstract. 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 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.

Biography. 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, type systems, proof assistants, 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/) and its use for building a formally verified HTTPS stack (https://project-everest.github.io).

Catalin received his PhD from Saarland University, supported by fellowships from the International Max Planck Research School for Computer Science and Microsoft Research Cambridge. Recently he received a Habilitation degree from ENS Paris, and was previously also a Research Associate at University of Pennsylvania and a Visiting Researcher at Microsoft Research Redmond.