检索结果-内蒙古大学图书馆

DimSum: A Decentralized Approach to multi-language semantics and Verification

PROCEEDINGS OF THE ACM ON PROGRAMMING languageS-PACMPL 2023年第POPL期7卷 775-805页

作者： Sammler, Michael Spies, Simon Song, Youngju D'Osualdo, Emanuele Krebbers, Robbert Garg, Deepak Dreyer, Derek MPI SWS Saarland Informat Campus Saarbrucken Germany Radboud Univ Nijmegen Nijmegen Netherlands

Priorwork on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g., fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this paper, we explore the problem of how to avoid such global restrictions. Concretely, we present DimSum: a new, decentralized approach to multi-language semantics and verification, which we have implemented in the Coq proof assistant. Decentralization means that we can define and reason about languages independently from each other (as independent modules communicating via events), but also combine and translate between them when necessary (via a library of combinators). We apply DimSum to a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec. We evaluate DimSum on two case studies: an Asm library extending Rec with support for pointer comparison, and a coroutine library for Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications, despite the behavior of the Asm libraries not being syntactically expressible in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm, showing that it is compatible with these Asm libraries.

关键词： multi-language semantics verification compilers non-determinism separation logic Iris Coq

来源：评论

学校读者我要写书评

暂无评论

An Equivalence-Preserving CPS Translation via multi-language semantics 11

An Equivalence-Preserving CPS Translation via Multi-Language...

引用

16th ACM SIGPLAN International Conference on Functional Programming (ICFP 11)

作者： Ahmed, Amal Blume, Matthias Indiana Univ Bloomington IN 47405 USA

ISBN: (纸本)9781450308656

language-based security relies on the assumption that all potential attacks follow the rules of the language in question. When programs are compiled into a different language, this is true only if the translation process preserves observational equivalence. To prove that a translation preserves equivalence, one must show that if two program fragments cannot be distinguished by any source context, then their translations cannot be distinguished by any target context. Informally, target contexts must be no more powerful than source contexts, i.e., for every target context there exists a source context that "behaves the same." This seems to amount to being able to "back-translate" arbitrary target terms. However, that is simply not viable for practical compilers where the target language is lower-level and, thus, contains expressions that have no source equivalent. In this paper, we give a CPS translation from a less expressive source language (STLC) to a more expressive target language (System F) and prove that the translation preserves observational equivalence. The key to our equivalence-preserving compilation is the choice of the right type translation: a source type sigma mandates a set of behaviors and we must ensure that its translation sigma(+) mandates semantically equivalent behaviors at the target level. Based on this type translation, we demonstrate how to prove that for every target term of type sigma(+), there exists an equivalent source term of type sigma - even when sub-terms of the target term are not necessarily "back-translatable" themselves. A key novelty of our proof, resulting in a pleasant proof structure, is that it leverages a multi-language semantics where source and target terms may interoperate.

关键词： full abstraction equivalence-preserving compilation continuation-passing style multi-language semantics logical relations back-translation

来源：评论

学校读者我要写书评

暂无评论

An Equivalence-Preserving CPS Translation via multi-language semantics

引用

ACM SIGPLAN NOTICES 2011年第9期46卷 431-444页

作者： Ahmed, Amal Blume, Matthias Indiana Univ Bloomington IN 47405 USA

关键词： languages Reliability Security Theory full abstraction equivalence-preserving compilation continuation-passing style multi-language semantics logical relations back-translation

来源：评论

学校读者我要写书评

暂无评论

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING languageS-PACMPL 2023年第OOPSLA期7卷 716–744页

作者： Gueneau, Armael Hostert, Johannes Spies, Simon Sammler, Michael Birkedal, Lars Dreyer, Derek Univ Paris Saclay ENS Paris Saclay CNRS InriaLab Methodes Formelles F-91190 Gif Sur Yvette France Saarland Univ Saarbrucken Germany MPI SWS Saarland Informat Campus Saarbrucken Germany Aarhus Univ Aarhus Denmark

In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this paper, we take the first steps towards the goal of developing program logics for multi-language verification. Specifically, we present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI-previously only described in prose in the OCaml manual-as well as the first program logic to reason about the interactions of program components written in OCaml and C. Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.

关键词： foreign-function interfaces OCaml C program logics multi-language semantics garbage collection separation logic angelic non-determinism transfinite step-indexing Iris Coq

来源：评论

学校读者我要写书评

暂无评论

FunTAL: Reasonably Mixing a Functional language with Assembly 2017

FunTAL: Reasonably Mixing a Functional Language with Assembl...

引用

38th ACM SIGPLAN Conference on Programming language Design and Implementation (PLDI)

作者： Patterson, Daniel Perconti, Jamie Dimoulas, Christos Ahmed, Amal Northeastern Univ Boston MA 02115 USA Harvard Univ Cambridge MA 02138 USA

ISBN: (纸本)9781450349888

We present FunTAL, the first multi-language system to formalize safe interoperability between a high-level functional language and low-level assembly code while supporting compositional reasoning about the mix. A central challenge in developing such a multi-language is bridging the gap between assembly, which is staged into jumps to continuations, and high-level code, where subterms return a result. We present a compositional stack-based typed assembly language that supports components, comprised of one or more basic blocks, that may be embedded in high-level contexts. We also present a logical relation for FunTAL that supports reasoning about equivalence of high-level components and their assembly replacements, mixed-language programs with callbacks between languages, and assembly components comprised of different numbers of basic blocks.

关键词： multi-language semantics typed assembly language inline assembly contextual equivalence logical relations

来源：评论

学校读者我要写书评

暂无评论

Under Control: Compositionally Correct Closure Conversion with Mutable State 19

Under Control: Compositionally Correct Closure Conversion wi...

引用

21st International Symposium on Principles and Practice of Declarative Programming (PPDP)

作者： Mates, Phillip Perconti, Jamie Ahmed, Amal Northeastern Univ Boston MA 02115 USA

ISBN: (纸本)9781450372497

Compositional compiler verification aims to ensure correct compilation of components, not just whole programs. Perconti and Ahmed [2014] propose a methodology for compositional compiler correctness that supports linking with code of arbitrary provenance. In particular, they allow compiled components to be linked with code whose functionality cannot even be expressed in the compiler's own source language. The essence of their approach is to define a multi-language system that formalizes interoperability between the source and target languages so that compiler correctness can be stated as contextual equivalence in the multi-language. They illustrate this methodology on a two-pass type-preserving compiler for a polymorphic language with recursive types. We showhowto extend this multi-language compiler-verification approach to a source language with ML-style mutable references. We present the first compositional correctness proof of typed closure conversion for a language with mutable state. More importantly, we show we can extend our target language with first-class control (call/cc) yielding a compiler correctness theorem that allows components compiled from the source language (without call/cc) to be linked with target-language components (with call/cc) whose extensional behavior cannot be expressed in the source. A non-trivial technical contribution is the design of the multi-language logical relation used to carry out the proof of compiler correctness. This is semantically challenging due to the mix of parametric polymorphism and mutable state in both interoperating languages. We use a blue font to typeset our source language and a bold red to typeset the target. The paper will be much easier to read if viewed/printed in color.

关键词： Compiler correctness typed closure conversion multi-language semantics mutable state first-class continuations logical relations

来源：评论

学校读者我要写书评

暂无评论

Fully Abstract Compilation via Universal Embedding 2016

Fully Abstract Compilation via Universal Embedding

引用

21st ACM SIGPLAN International Conference on Functional Programming (ICFP)

作者： New, Max S. Bowman, William J. Ahmed, Amal Northeastern Univ Boston MA 02115 USA

ISBN: (纸本)9781450342193

A fully abstract compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is secure: target-language attackers can make no more observations of a compiled component than a source-language attacker interacting with the original source component. Proving full abstraction for realistic compilers is challenging because realistic target languages contain features (such as control effects) unavailable in the source, while proofs of full abstraction require showing that every target context to which a compiled component may be linked can be back-translated to a behaviorally equivalent source context. We prove the first full abstraction result for a translation whose target language contains exceptions, but the source does not. Our translation-specifically, closure conversion of simply typed lambda-calculus with recursive types-uses types at the target level to ensure that a compiled component is never linked with attackers that have more distinguishing power than source-level attackers. We present a new back-translation technique based on a shallow embedding of the target language into the source language at a dynamic type. Then boundaries are inserted that mediate terms between the untyped embedding and the strongly-typed source. This technique allows back-translating non-terminating programs, target features that are untypeable in the source, and well-bracketed effects.

关键词： Secure compilation fully abstract compilation universal embedding universal domain parametricity logical relations multi-language semantics back-translation

来源：评论

学校读者我要写书评

暂无评论

Fully Abstract Compilation via Universal Embedding

引用

ACM SIGPLAN NOTICES 2016年第9期51卷 103-116页

作者： New, Max S. Bowman, William J. Ahmed, Amal Northeastern Univ Boston MA 02115 USA

关键词： Secure compilation fully abstract compilation universal embedding universal domain parametricity logical relations multi-language semantics back-translation

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：