Fully Abstract Compilation via Universal Embedding

Reference. Fully Abstract Compilation via Universal Embedding

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 λ-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.

Cite

Cite as @new_bowman_ahmed_2016 (helia, typst) · \cite{new_bowman_ahmed_2016} (LaTeX)

BibTeX

bibtex · 8 lines

@inproceedings{new_bowman_ahmed_2016,
 title = {Fully Abstract Compilation via Universal Embedding},
 author = {New, Max S. and Bowman, William J. and Ahmed, Amal},
 year = {2016},
 url = {http://dl.acm.org/citation.cfm?id=2951941},
 booktitle = {Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016},
 publisher = {ACM}
}

hayagriva YAML (typst)

yaml · 13 lines

new_bowman_ahmed_2016:
  type: article
  title: Fully Abstract Compilation via Universal Embedding
  author:
  - New, Max S.
  - Bowman, William J.
  - Ahmed, Amal
  date: 2016
  url: http://dl.acm.org/citation.cfm?id=2951941
  parent:
    type: proceedings
    title: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016
    publisher: ACM

Download: new_bowman_ahmed_2016.bib · new_bowman_ahmed_2016.yml

Cited by (3)

Type-Preserving Flat Closure Optimization geller-2025-typeOOPSLA · 2025

Type-preserving compilation seeks to make intent as much as a part of compilation as computation . Specifications of intent in the form of types are preserved and exploited during compilation and linking, alongside the mere computation of a program. This provides lightweight guarantees for compilation, optimization, and linking. Unfortunately, type-preserving compilation typically interferes with important optimizations. In this paper, we study typed closure representation and optimization. We analyze limitations in prior typed closure conversion representations, and the requirements of many important closure optimizations. We design a new typed closure representation in our Flat-Closure Calculus (FCC) that admits all these optimizations, prove type safety and subject reduction of FCC, prove type preservation from an existing closure converted IR to FCC, and implement common closure optimizations for FCC.

PDF · DOI · pldb

Multi-Language Probabilistic Programming stites-2025-multiOOPSLA · 2025

There are many different probabilistic programming languages that are specialized to specific kinds of probabilistic programs. From a usability and scalability perspective, this is undesirable: today, probabilistic programmers are forced up-front to decide which language they want to use and cannot mix-and-match different languages for handling heterogeneous programs. To rectify this, we seek a foundation for sound interoperability for probabilistic programming languages: just as today’s Python programmers can resort to low-level C programming for performance, we argue that probabilistic programmers should be able to freely mix different languages for meeting the demands of heterogeneous probabilistic programming environments. As a first step towards this goal, we introduce Multi PPL, a probabilistic multi-language that enables programmers to interoperate between two different probabilistic programming languages: one that leverages a high-performance exact discrete inference strategy, and one that uses approximate importance sampling. We give a syntax and semantics for Multi PPL, prove soundness of its inference algorithm, and provide empirical evidence that it enables programmers to perform inference on complex heterogeneous probabilistic programs and flexibly exploits the strengths and weaknesses of two languages simultaneously.

PDF · DOI · arXiv · pldb

FabULous Interoperability for ML and a Linear Language scherer_etal_2018FoSSaCS · 2018

Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate to cover the same feature space. This can improve usability by making each part simpler than the whole, but there is a risk of abstraction leaks from one language to another that would break expectations of the users familiar with only one or some of the involved languages.

We propose a formal specification for what it means for a given language in a multi-language system to be usable without leaks: it should embed into the multi-language in a fully abstract way, that is, its contextual equivalence should be unchanged in the larger system.

To demonstrate our proposed design principle and formal specification criterion, we design a multi-language programming system that combines an ML-like statically typed functional language and another language with linear types and linear state. Our goal is to cover a good part of the expressiveness of languages that mix functional programming and linear state (ownership), at only a fraction of the complexity. We prove that the embedding of ML into the multi-language system is fully abstract: functional programmers should not fear abstraction leaks. We show examples of combined programs demonstrating in-place memory updates and safe resource handling, and an implementation extending OCaml with our linear language.

Web

Cites 36 works (0 here)

External (36)

Fully-abstract compilation by approximate back-translation (2016)
Lightweight verification of separate compilation (2016)
Compiler verification meets cross-language linking via data abstraction (2016)
Noninterference for free (2015)
The correctness-security gap in compiler optmization (2015)
Pilsner: A compositionally verified compiler for a higher-order imperative language (2015)
Secure compilation to protected module architectures (2015)
Verifying an open compiler using multi-language semantics (2014)
Fully abstract compilation to JavaScript (2013)
Secure compilation of object-oriented components to protected module architectures (2013)
On protection by layout randomization (2012)
Secure compilation to modern processors (2012)
The impact of higher-order state and control effects on local relational reasoning (2012)
An equivalence-preserving CPS translation via multi-language semantics (2011)
Local memory via layout randomization (2011)
Embedding an interpreted language using higher-order functions and types (2011)
Typed closure conversion preserves observational equivalence (2008)
Proving noninterference by a fully complete translation to the simply typed λ-calculus (2008)
Operational semantics for multi-language programs (2007)
Fully abstract semantics of additive aspects by translation (2007)
Proving noninterference by a fully complete translation to the simply typed λ-calculus (2007)
Step-indexed syntactic logical relations for recursive and quantified types (2006)
Securing the .NET programming model (2006)
Translating dependency into parametricity (2004)
Universal types and what they are good for (2003)
Object closure conversion (1999)
Protection in programming-language translations (1998)
Compiling Standard ML to Java bytecodes (1998)
Operational reasoning for functions with local state (1998)
Typed closure conversion (1996)
A fully abstract semantics for a concurrent functional language with monadic types (1995)
Classical logic, storage operators and second-order lambda-calculus (1994)
A revised report on the syntactic theories of sequential control and state (1992)
Fully abstract translations between functional languages (1991)
Continuations may be unreasonable (1988)
Data types as lattices (1976)