Abstract Techniques for Programming Languages and Secure Compilation

点击翻译按钮获取中文摘要

Reasoning about imperative and higher-order programming languages in the context of security and verification is known to be a notoriously difficult task, which can be facilitated by factoring through such abstract general properties as compositionality, adequacy and full abstraction. However, these properties are also very hard to establish in practice and they moreover tend to be fragile and sensitive to various factors including syntax, language features, and notions of observable behaviour and program equivalence. In ATLaS, we will build on the recently emerged notion of higher-order abstract GSOS to develop an integrated framework for the semantics of higher-order and imperative languages with applications to the verification of secure compilers. Higher-order abstract GSOS is a recent pivotal generalization of the well-established first-order counterpart of Turi and Plotkin. Much like the latter, higher-order abstract GSOS is compositional w.r.t. strong variants of Abramsky's applicative bisimilarity, yet it is considerably more sophisticated than the first-order notion -- unleashing its full power is thus one of our goals in ATLaS. More specifically, we first aim to reconcile the call-by-value evaluation strategy with higher-order abstract GSOS as well as define a unifying metalanguage based on Levy's subsuming paradigm of call-by-push-value. We will subsequently investigate weaker notions of equivalence in higher-order abstract GSOS, prominently Abramsky's weak applicative bisimilarity. To that end, we are planing to develop a categorical generalization of Howe's method. A further goal will be to extend higher-order abstract GSOS for typed languages and languages with computational effects such as probability, non-determinism and store. As an important and complex example, we will specifically address presheaf models of dynamic memory allocation, which should particularly benefit from the abstract, axiomatic nature of our approach. In ATLaS we put special emphasis on formalizing our results in the proof assistant Agda; this will provide reusability and a formal guarantee of correctness as well as compliance with the foundational principles of type theory. The main intended application domain for our developments is the emerging field of secure compilation, which deals with requirements and techniques to detect and prevent the introduction of security vulnerabilities during the compilation process, such as buffer overflows, memory leaks, or other common security flaws. We intend to address these issues by modelling the security properties of languages within abstract GSOS and associating abstraction-preserving compilers, i.e. secure compilers, with the formal notion of a morphism across abstract GSOS specifications.