Abstract Techniques for Programming Languages and Secure Compilation

众所周知，在安全和验证的上下文中推理命令式和高阶编程语言是一项众所周知的困难任务，可以通过分解诸如组合性、充分性和完全抽象等抽象一般性质来促进这一任务。然而，这些性质在实践中也很难建立，而且它们往往是脆弱的，并且对各种因素很敏感，包括语法、语言特征、可观察行为的概念和程序等价性。在Atlas中，我们将建立在最近出现的高阶抽象GSOS概念的基础上，为高阶和命令式语言的语义开发一个集成框架，并将其应用于安全编译器的验证。高阶抽象GSOS是Turi和Plotkin的成熟的一阶对应的最近的关键推广。与后者非常相似的是，高阶抽象GSOS是组成的W.r.t.阿布拉姆斯基的应用生物相似性的强烈变体，但它比一阶概念要复杂得多--因此，释放其全部力量是我们在Atlas中的目标之一。更具体地说，我们首先的目标是协调按值调用的评估策略和更高阶抽象的GSO，并基于Levy的按推值调用的包含范式定义统一的元语言。我们随后将研究高阶抽象GSOS中较弱的等价概念，特别是Abramsky的弱应用互相似性。为此，我们计划对豪的方法进行分类推广。另一个目标是将高阶抽象GSO扩展到类型化语言和具有计算效果的语言，如概率、非确定性和存储。作为一个重要而复杂的示例，我们将具体讨论动态内存分配的前堆模型，它应该特别受益于我们方法的抽象、公理性质。在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.