From Secure Compilation to Secure Abstraction Stronger Foundations and New Connections

Very often, programs are executed in a setting where abstractions have been compiled away or implemented in terms of more low-level primitives. For example, operating systems will load programs into separate or overlapping regions of memory and use preemptive multi-tasking and CPU-supported virtual memory primitives to simulate fictitious isolated execution environments for every individual process. When such abstractions are implemented such that they continue to hold in the presence of adversaries, this is called a secure abstraction. Formal study of secure abstractions is the topic of a computer science research subfield called secure compilation. Contrary to what the name suggests, the field of secure compilation should not be restricted to what one would traditionally consider a compiler. The field is actually much broader than this and should really be understood as the study of secure abstractions. In this thesis, we will contribute a generalized view on secure compilation, exploring and demonstrating new links and new applications of secure compilation techniques in settings where they have not previously been applied. Specifically, we will look at fields like cryptography, language expressiveness and gradual typing, where the new perspective may offer new insights and techniques.