From Secure Compilation to Secure Abstractions: Stronger Foundations, New Connections
Abstract
Software engineering facilitates the development, maintenance and evolution of complex software systems by fundamentally relying on abstractions. Such abstractions include operating system services, high-level programming languages, reusable library code, etc. However, many security exploits fundamentally exploit discrepancies between abstract semantics and low-level semantics of programs. This includes, for example, memory safety attacks (e.g. stack smashing), side channel attacks (e.g. Spectre/Meltdown), physical attacks (e.g. Rowhammer) and many others (e.g. symlink races). At the same time, some abstractions are implemented in such a way that (some of) their guarantees continue to hold in the low-level execution. Consider, for example, how operating systems use virtual memory to preserve process isolation when applying preemptive multitasking. Such secure abstractions can be used by programmers, not just for reasoning about software correctness, but also security. They were first studied in 1998 by Abadi and characterized using a property called full abstraction. Since then, the property has been applied in many contexts (secure compilers, secure linkers, secure calling conventions, secure CPU implementations, contract enforcement etc.) and various generalizations of the property have been proposed. The goals of this project are (1) strengthening the foundations of secure compilation, and (2) establishing and studying new connections to different fields.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 21, 2022
- Source ID
- FA95502110054XX0
Entities
People
- Dominique Devriese
Organizations
- Air Force Office of Scientific Research
- United States Air Force
- Vrije Universiteit Brussel