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 objectives of this project are (1) strengthening the foundations of secure compilation, and (2) establishing and studying new connections to different fields.
To accomplish (1), we will propose and study a new family of characterizations of secure compilation that (a) do not depend on I/O event traces, (b) generalize important properties from the literature and (c) are sufficiently general for the new applications we will develop in this project.
For (2), we will establish new connections between secure compilation and (a) characterizations of relative language expressiveness, (b) enforcement of static types in gradual languages and (c) cryptography.
Short titleSecure Abstractions
Effective start/end date15/11/2014/11/25

    Flemish discipline codes

  • Software engineering

    Research areas

  • Software engineering

ID: 54536311