SWS   Info

Expert Audience

English

-- Not specified --

Saarbrücken

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.

--email hidden

passcode not visible

logged in users only