Abstract Techniques for Programming Languages and Secure Compilation

众所周知，在安全和验证的背景下推理命令式和高阶编程语言是一项非常困难的任务，这可以通过分解诸如组合性，充分性和完全抽象等抽象的一般属性来促进。然而，这些属性也很难在实践中建立，而且它们往往是脆弱的和敏感的各种因素，包括语法，语言功能，可观察的行为和程序等价的概念。在ATLaS中，我们将建立在最近出现的高阶抽象GSOS的概念，开发一个集成的框架，用于高阶和命令式语言的语义与应用程序的安全编译器的验证。高阶抽象GSOS是图里和普洛特金的一阶对应物的最近的关键推广。与后者非常相似，高阶抽象GSOS是组合w.r.t.。Abramsky的应用双相似性的强变体，但它比一阶概念复杂得多-释放其全部力量因此是我们在ATLaS中的目标之一。更具体地说，我们的第一个目标是调和调用的价值评估策略与高阶抽象GSOS，以及定义一个统一的元语言的基础上利维的归入范式的调用推值。随后，我们将研究较弱的概念等价高阶抽象GSOS，突出阿布拉姆斯基的弱应用双相似性。为此，我们正计划发展一种豪方法的分类推广。进一步的目标将是扩展高阶抽象GSOS的类型化语言和语言的计算效果，如概率，非确定性和存储。作为一个重要而复杂的例子，我们将专门讨论动态内存分配的预层模型，它应该特别受益于我们方法的抽象性和公理性。在ATLaS中，我们特别强调在证明助手Agda中形式化我们的结果;这将提供可重用性和正确性的形式化保证，以及遵守类型论的基本原则。我们开发的主要应用领域是新兴的安全编译领域，它涉及在编译过程中检测和防止引入安全漏洞的要求和技术，例如缓冲区溢出，内存泄漏或其他常见的安全漏洞。我们打算解决这些问题，通过建模的安全属性的语言在抽象GSOS和关联的抽象保持编译器，即安全编译器，与形式概念的态射抽象GSOS规范。

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.