Weekly Principles of Programming and Verification seminars are now held on Tuesday at 4pm via zoom, because of the recent COVID-19 outbreak. If you are interested in attending, please contact Marco Gaboardi <email@example.com>.
You can subscribe to the POPV mailing list here.
Below is a list of seminar dates for Fall 2020 with information on the speakers:
|Sep 22||Ankush Das
(Carnegie Mellon University)
|Resource-Aware Session Types for Digital Contracts|
|Sep 29||Social Time|
|Oct 06||Jonathan Protzenko
|Latest advances in scaling cryptographic verification in F*|
|Oct 13||June Wunder
|Oct 20||Assaf Kfoury
|First-Order Term Rewriting (compressed tutorial)|
|Oct 27||Ben Greenman
|Complete Monitoring for Gradual Types|
|Nov 03||Mirai Ikebuchi
|Homological Methods in Rewriting|
|Nov 10||Justin Hsu
(University of Wisconsin – Madison)
|A Separation Logic for Probabilistic Independence|
|Nov 17||Paul Downen
(University of Oregon)
|Kinds Are Calling Conventions: Intensional Static Polymorphism|
|Nov 24||Zoe Paraskevopoulou
|Compositional Optimizations for CertiCoq|
|Dec 1||Stephanie Balzer
(Carnegie Mellon University)
|Manifest Deadlock-Freedom for Shared Session Types|
|Dec 8||Clément Pit-Claudel
|Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs|
|Dec 15||Andrej Dudenhefner (Saarland University)||Tamed and Mechanized: Undecidability of System F Typability and Type Checking|
Speaker: Andrej Dudenhefner (Saarland University)
Title: Tamed and Mechanized: Undecidability of System F Typability and Type Checking
Abstract: The undecidability of both typability and type checking for System F (second-order lambda-calculus) was established by Wells in the late 1990s . After months of experience failing to mechanize the original 40 page argument in the Coq proof assistant, a new, simpler argument emerged. This talk will give an overview over the following results:
1) Simpler undecidability proof for System F typability and type checking,
2) Constructive mechanization (in the Coq proof assistant) of many-one, reductions from Turing machine halting to System F typability, type checking, and inhabitation using the Coq Library of Undecidability Proofs .
 Wells, Joe B. “Typability and type checking in System F are equivalent and undecidable.” Annals of Pure and Applied Logic 98.1-3 (1999): 111-156.
Speaker: Clément Pit-Claudel (MIT)
Title: Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Abstract: We present an original approach to sound program extraction in a proof assistant, using syntax-driven automation to derive correct-by-construction imperative programs from nondeterministic functional source code. Our approach does not require committing to a single inflexible compilation strategy and instead makes it straightforward to create domain-specific code translators. In addition to a small set of core definitions, our framework is a large, user-extensible collection of compilation rules each phrased to handle specific language constructs, code patterns, or data manipulations. By mixing and matching these pieces of logic, users can easily tailor extraction to their own domains and programs, getting maximum performance and ensuring correctness of the resulting assembly code.
Using this approach, we complete the first proof-generating pipeline that goes automatically from high-level specifications to assembly code. In our main case study, the original specifications are phrased to resemble SQL-style queries, while the final assembly code does manual memory management, calls out to foreign data structures and functions, and is suitable to deploy on resource-constrained platforms. The pipeline runs entirely within the Coq proof assistant, leading to final, linked assembly code with overall full-functional-correctness proofs in separation logic.
Speaker: Stephanie Balzer (Carnegie Mellon University)
Title: Manifest Deadlock-Freedom for Shared Session Types
Abstract: Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed pi-calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to an acquire-release discipline. The resulting language recovers the expressiveness of the untyped asynchronous pi-calculus and accommodates practical programming scenarios, such as shared servers, file systems etc. The resulting language is implemented as a prototype in C0 (a safe subset for C used to teach freshmen at CMU) and as a DSL in Rust (https://github.com/maybevoid/ferrite).
The generalization, however, comes at the cost of deadlock-freedom, a property which holds for the purely linear fragment. In this talk, I report on recent work that makes up for this deficiency and introduces a type system of linear and shared session types in which the adjoint modalities are complemented with possible worlds to rule out cyclic dependencies between acquires and synchronizations. I distill the key abstractions to reason about cyclic dependencies and the key invariants enforced by the type system to guarantee deadlock-freedom. Time permitted, I report on ongoing work that also uses possible world modalities for type-based verification of program properties of interest.
Bio: Stephanie Balzer is a research faculty in the Principles of Programming group in the Computer Science Department at Carnegie Mellon University. Stephanie obtained her PhD from ETH Zurich under the supervision of Thomas R. Gross. In her PhD work, Stephanie developed the sequential relationship-based programming language Rumer and an invariant-based verification technique for Rumer. Stephanie’s current work focuses on the development of type systems and logics for verifying properties of concurrent programs.
Speaker: Zoe Paraskevopoulou (Northeastern University)
Title: Compositional Optimizations for CertiCoq
Abstract: In this talk I will present the verified, optimizing middle-end pipeline for CertiCoq, a compiler from Gallina (Coq’s specification language) to C. The middle-end optimizes and closure-converts an untyped functional intermediate language (ANF or CPS) to a subset of that language without nested functions, which can easily be code-generated to low-level languages. The pipeline is a sequence of small, efficient transformation passes that are implemented and verified in Coq. Our novel refactoring of these transformations allows us to express more complex optimizations as a composition of small passes that have simpler implementations, simpler specifications, and simpler proofs.
The pipeline comes with an end-to-end theorem that covers both whole-program and separate compilation, even when different modules are compiled with different optimizations (using the same intermediate languages). We accomplish this lightweight compositional compiler correctness using a new technique to compose logical-relation proofs. Additionally, we use a novel technique to prove divergence preservation — even for transformations that reduce the number of steps the programs take.
Speaker: Paul Downen (University of Oregon)
Title: Kinds Are Calling Conventions: Intensional Static Polymorphism
Abstract: System F has served as the workhorse for compiling typed programming
languages for many years. It provides a logical foundation for
polymorphism (i.e., generics) in programming languages. When extended
with common basic features (like data types), System F serves as a
practical core language used en route during the compilation process.
Many convenient, complex, user-facing features given to programmers
can be desugared into basic primitives — expressed in System F —
which greatly aids in optimizations and lower-level code generation.
And yet, from the perspective of systems programming, System F is
impractical. Systems languages enable programmers to write efficient
software by giving them fine-grained control over bare-metal
implementation details used in the machine, such as the layout of data
structures in memory, or the way in which they are passed to and from
functions. Sadly, these kind of important intensional details seem
incompatible with System F’s polymorphism: modern machines have many
specialized instructions, registers, etc., for working with different
types of primitives, but real generic code must work the same way with
In this talk, I’ll present a long line of work, begun almost 30 years
ago, for reconciling the tension between machine primitives and System
F’s static polymorphism. The goal is the development of intermediate
languages — the midway point in modern compiler pipeline between
source code and target assembly — which are useful for distilling
complex programming languages as well as enabling compiler-driven
optimizations. Throughout the past three decades, approaches have
been taken to improve optimizations by extending System F with
low-level details about how data is represented (such as boxed or
unboxed) and functions are called (such as by-value or by-reference),
which requires refinements to its notion of static polymorphism. And
I will show you how, in the end, they all reach the same conclusion:
kinds are calling conventions.
Speaker: Justin Hsu (UW)
Title: A Separation Logic for Probabilistic Independence
Abstract: Probabilistic independence is a basic concept for describing the result of random sampling—a fundamental operation in all probabilistic programs—and for reasoning about groups of random variables. Nevertheless, existing verification methods handle independence poorly, if at all. We will introduce a probabilistic separation logic called PSL, where separation models probabilistic independence, based on a new, probabilistic model of the logic of bunched implications (BI). The program logic PSL is capable of verifying information-theoretic security of cryptographic constructions for several well-known tasks, including private information retrieval, oblivious transfer, secure multi-party addition, and simple oblivious RAM, while reasoning solely in terms of independence and uniformity. If time permits, we will also discuss ongoing work for reasoning about conditional independence.
Speaker: Mirai Ikebuchi (MIT)
Title: Homological Methods in Rewriting
Abstract: It is well-known that some equational theories such as groups or boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. In this talk, we will see a way to find a lower bound of the number of axioms. The inequality that gives the lower bound is obtained by analyzing the algebraic structure, called the homology group, associated with the given equational theory. I will explain how equational theories and rewriting systems relate to abstract algebra, what homology groups in general settings are like, and what the homology groups of equational theories give us.
Speaker: Ben Greenman (Northeastern University)
Title: Complete Monitoring for Gradual Types
Abstract: In a gradual language, type soundness guarantees the safety of typed code; when untyped code fails to respect types, a runtime check finds the discrepancy. As for untyped code, type soundness makes no promises. Soundness does not protect untyped code from mistakes in type specifications and unwarranted blame.
What protects untyped code? To address the asymmetry, we adapt complete monitoring from the contract world to gradual typing. Complete monitoring leads to a guarantee that catches problems with faulty type specifications and helps tell apart the many designs in the gradual typing literature.
Speaker: Assaf Kfoury (BU)
Title: First-Order Term Rewriting (compressed tutorial)
Abstract: Term rewriting is an important computational model with applications in software engineering, declarative programming, and automated theorem proving. In term rewriting, computation is achieved by directed equations and pattern matching. In this tutorial we present basic notions and results, including confluence (weak and strong), normalization (weak and strong), and various other related properties and how they interact. We conclude with a very brief exposition of critical pairs and completion procedures. Throughout we aim to stress the deep connections between equational reasoning and term rewriting. We precisely define all these notions and accompany them with numerous motivating examples.
This tutorial provides a partial background for Mirai Ikebuchi’s lecture on November 3: Homological Methods in Rewriting.
Speaker: Jonathan Protzenko (Microsoft Research)
Title: Latest advances in scaling cryptographic verification in F*
Abstract: Project Everest is a large-scale verification effort that aims to verify an entire TLS stack from the ground up. In the journey to a fully verified protocol, several projects have gained a life of their own. In particular, all of the core cryptographic components are now packaged in a library called EverCrypt, which offers vectorized algorithms, assembly optimized versions, and high-level APIs that offer multiplexing, agility and automatic CPU autodetection.
In this talk, I will give an overview of EverCrypt and Project Everest. I will then reflect on the lessons we have learned since the first version of our cryptographic library nearly 5 years ago, and how we managed to scale up to 17 algorithms and nearly 40 implementations. The talk will cover language techniques and general proof design and engineering.
Speaker: Ankush Das (Carnegie Mellon University)
Title: Resource-Aware Session Types for Digital Contracts
Abstract: While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges, this talk presents an analysis for statically deriving worst-case bounds on the computational complexity of message-passing processes, respectively. The analysis is based on novel resource-aware session types that describe resource contracts by allowing both messages and processes to carry potential and amortize cost. The talk then applies session types to implement digital contracts. Digital contracts are protocols that describe and enforce execution of a contract, often among mutually distrusting parties. Programming digital contracts comes with its unique challenges, which include describing and enforcing protocols of interaction, analyzing resource usage and tracking linear assets. The talk presents the type-theoretic foundations of Nomos, a programming language for digital contracts whose type system addresses the aforementioned domain-specific requirements. To express and enforce protocols, Nomos is based on shared binary session types rooted in linear logic. To control resource usage, Nomos uses resource-aware session types and automatic amortized resource analysis, a type-based technique for inferring resource bounds. To track assets, Nomos employs a linear type system that prevents assets from being duplicated or discarded. The talk concludes with future work directions on designing an efficient implementation for Nomos and making it robust to attacks from malicious entities.
Ankush Das is a final year PhD student at Carnegie Mellon University. He is advised by Prof. Jan Hoffmann. He is broadly interested in programming languages with a specific focus on resource analysis, session types and language design for smart contracts on the blockchain. He is the lead designer and developer of Nomos, a domain-specific language for implementing smart contracts based on resource-aware session types. In the past, he has worked jointly with Prof. Frank Pfenning and his advisor on designing resource-aware session types for parallel complexity analysis of concurrent programs implemented in a programming language called Rast. Before joining CMU, he worked as a Research Fellow at Microsoft Research, India with Akash Lal where he developed an efficient method to perform precise alias analysis for C and C++ programs for Windows driver modules to automatically infer safe null pointer dereferences. He completed his undergraduate at IIT Bombay, India in 2014 where he worked with Prof. Supratik Chakraborty and Prof. Akshay S on deciding termination of linear loop programs.
Below is a list of seminar dates for Spring-Summer 2020 with information on the speakers:
|Jan 28||Alley Stoughton
|You Sank My Battleship! A Case Study in Secure Programming|
|Feb 4||Chris Casinghino
|A Language for Programmable Hardware Security|
|Feb 11||Ugo Dal Lago
(University of Bologna)
|Differential Program Semantics|
|Feb 18||Riyadh Baghdadi
|Building Compilers for High Performance Code Generation|
|Feb 25||Maximiliam Algehed (Chalmers University)||Simple Noninterference from Parametricity|
|Mar 3||No Talk||No Talk|
|Mar 10||Spring Break|
|Mar 17||Mark Lemay
|Dependent Types to Support Continuous Offline Testing|
|Mar 24||Aaron Bembenek
|Formulog: Datalog for SMT-based Static Analysis|
|Mar 31||No Talk||No Talk|
|Apr 7||Marco Gaboardi
|Bounded Linear Logic and Metric Interpretation|
|Apr 14||No Talk||No Talk|
|Apr 21||Joseph Tassarotti
|Verifying Concurrent Randomized Programs|
|Apr 28||Eric Koskinen
(Stevens Institute of Technology)
|Reducing Commutativity Verification to Reachability with Differencing Abstractions|
|May 5||Aleks Nanevski
(Imdea Software Institute)
|Type and proof structures for concurrency – part 1|
|May 12||Aleks Nanevski
(Imdea Software Institute)
|Type and proof structures for concurrency – part 2|
|May 19||Arthur Azevedo de Amorim
(Carnegie Mellon University)
|Reconciling Noninterference and Gradual Typing|
|May 26||Aaron Weiss
|Oxide: The Essence of Rust|
|June 2||Anitha Gollamudi
|Information Flow Control for Distributed Trusted Execution Environments|
|June 9||Stephen Chang
|Improving Software Development via (Typed) Language Tailoring|
|June 16||Paolo Perrone
|Monads, partial evaluations, and rewriting|
|June 23||Michael Greenberg
|Executable Formal Semantics for the POSIX Shell|
|June 30||Anindya Banerjee
|July 7||Anindya Banerjee
Speaker: Alley Stoughton (BU)
Title: You Sank My Battleship! A Case Study in Secure Programming
Abstract: We report on a case study in secure programming, focusing on the design, implementation and auditing of programs for playing the board game Battleship. We begin by precisely defining the security of Battleship programs, borrowing ideas from theoretical cryptography. We then consider three implementations of Battleship: one in Concurrent ML featuring a trusted referee; one in Haskell/LIO using information flow control to avoid needing a trusted referee; and one in Concurrent ML using access control to avoid needing such a referee. All three implementations employ data abstraction in key ways.
* Alley Stoughton, Andrew Johnson, Samuel Beller, Karishma Chadha, Dennis Chen, Kenneth Foner, Michael Zhivich:
You Sank My Battleship!: A Case Study in Secure Programming. PLAS@ECOOP 2014: 2
Speaker: Chris Casinghino (Draper Labs)
A Language for Programmable Hardware Security
Abstract: Hardware security mechanisms have struggled to keep up with the rapidly changing security landscape. Hardware is time-consuming to design, and its fixed nature makes it challenging to adapt to new threats. Modern tagged architectures solve this problem by enforcing general software-defined security policies. Policies define what information is stored in the tags and what rules the architecture enforces relative to this information (e.g., data tagged as confidential should not be sent over the network). However, this introduces new questions: What tools should we use to build these software-defined policies? How can we be confident that these policies enforce the security and safety properties we are interested in? This talk examines these questions in the context of a general-purpose security mechanism that extends existing processors with software-defined tag processing. We describe the language we use to define tag-based policies, and related research.
Speaker: Ugo Dal Lago (University of Bologna)
Differential Program Semantics
Abstract: Giving meaning to programs through axiomatic, denotational, and operational semantics is one of the main goals of theoretical computer science since its early days. Traditionally, program semantics is built around notions of program equivalence and refinement, based on which verification and transformation techniques can be justified. More and more often, however, programs are substituted with approximately equivalent programs, or verified against imprecise specifications. Program semantics has started dealing with program differences only in recent years, through the interpretation of programs in metric spaces. We give a brief survey about the state of the art on program semantics, and argue about the inadequacy of metrics as a way to deal with program differences. We thus point at a few preliminary results on a new kind of differential program semantics: logical relations, bisimilarity, and game semantics.
Speaker: Riyadh Baghdadi (MIT)
Building Compilers for High Performance Code Generation
Abstract: This talk is about building compilers for high performance code generation. It has three parts. The first part is about Tiramisu (http://tiramisu-compiler.org/), a polyhedral compiler designed for generating highly efficient code for multicores and GPUs. It is the first polyhedral compiler that can match the performance of highly hand-optimized industrial libraries such as Intel MKL and cuDNN. The second part is about applying Tiramisu to accelerate deep learning (DNN) inference. In comparison to other DNN compilers, Tiramisu has two unique features: (1) it supports sparse DNNs; and (2) it can express and optimize general RNNs (Recurrent Neural Networks). The third part will present recent work on the problem of automatic code optimization. In particular, it will focus on using deep learning to build a cost model to explore the search space of code optimizations.
Speaker: Maximiliam Algehed (Chalmers University)
Simple Noninterference from Parametricity
Abstract: We revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a polyvariant variation of the Dependency Core Calculus of in the Calculus of Constructions. The proof is modular: it leverages parametricity for the Calculus of Constructions and the encoding of data abstraction using existential types. This perspective gives rise to simple and understandable proofs of noninterference from parametricity. All our contributions have been mechanised in the Agda proof assistant.
Speaker: Mark Lemay (Boston University)
Dependent Types to Support Continuous Offline Testing
Speaker: Aaron Bembenek (Harvard University)
Formulog: Datalog for SMT-based Static Analysis
Many static analyses are based around satisfiability modulo theories (SMT) solving; examples include symbolic execution, refinement type checking, and forms of model checking. This talk presents Formulog, a domain-specific language that makes it possible to write a range of SMT-based static analyses in a way that is both close to their formal specifications and amenable to high-level optimizations and efficient evaluation. Formulog is an extension of the logic programming language Datalog with a first-order fragment of ML and mechanisms for representing and reasoning about SMT formulas; a novel type system supports the construction of expressive formulas, while ensuring that neither normal evaluation nor SMT solving goes wrong. Our case studies demonstrate that a diverse range of SMT-based analyses can naturally and concisely be encoded in Formulog, and that — thanks to this encoding — high-level Datalog-style optimizations can be automatically and advantageously applied to these analyses.
Speaker: Marco Gaboardi (Boston University)
Bounded Linear Logic and Metric Interpretation
In this talk I will present the basic ideas of linear logic (in its intuitionistic version), for then connecting them with the idea of bounded linear logic. I will then show how we can give to bounded linear logic an interesting metric interpretation.
Speaker: Joseph Tassarotti (Boston College)
Verifying Concurrent Randomized Programs
Despite continued progress in program verification, many fundamental data structures and algorithms remain difficult to verify. Challenges arise when programs use concurrency or randomization because these effects lead to non-deterministic behavior. Although many specialized logics have been developed to reason about programs that use either concurrency or randomization, most can only handle the use of one of these features in isolation. However, many common concurrent data structures are randomized, making it important to consider the combination.
This talk will describe Polaris, a logic for reasoning about programs that are both concurrent and randomized. Polaris combines ideas from three separate lines of work: (1) Varacca and Winskel’s denotational model of non-determinism and probability, (2) Barthe et al.’s approach to probabilistic relational reasoning via couplings, and (3) higher-order concurrent separation logic, as realized in the Iris verification framework.
Bio: Joseph Tassarotti is an assistant professor at Boston College. Previously, he was a postdoctoral associate in the Parallel and Distributed Operating Systems group at MIT. He received his Ph.D. from Carnegie Mellon University, where he was advised by Robert Harper.
Speaker: Eric Koskinen (Stevens Institute of Technology)
Reducing Commutativity Verification to Reachability with Differencing Abstractions
Commutativity of data structure methods is of ongoing interest, with roots in the database community. In recent years commutativity has been shown to be a key ingredient to enabling multicore concurrency in contexts such as parallelizing compilers, transactional memory, speculative execution and, more broadly, software scalability. Despite this interest, it remains an open question as to how a data structure’s commutativity specification can be verified automatically from its implementation.
I will describe our recent work on techniques to automatically prove the correctness of method commutativity conditions from data structure implementations. We introduce a new kind of abstraction that characterizes the ways in which the effects of two methods differ depending on the order in which the methods are applied, and abstracts away effects of methods that would be the same regardless of the order. I’ll then discuss a novel algorithm that reduces the problem to reachability, so that off-the-shelf program analysis tools can perform the reasoning necessary for proving commutativity. Finally, I’ll describe CityProver: a proof-of-concept commutativity verifier and some experimental results on ADTs such as a memory cell, counter, two-place Set, array-based stack, queue, and a rudimentary hash table. I’ll conclude with a discussion of what makes a data structure’s commutativity provable with today’s tools and what needs to be done to prove more in the future.
Joint work with Kshitij Bansal
Speaker: Aleks Nanevski (Imdea Software Institute)
Type and proof structures for concurrency
The main challenge of concurrent software verification has always been in achieving modularity, i.e., the ability to divide and conquer the correctness proofs with the goal of scaling the verification effort.
Types are a formal method well-known for its ability to modularize programs, and in the case of dependent types, the ability to modularize and scale complex mathematical proofs.
In this talk I will present our recent work towards reconciling dependent types with shared memory concurrency, with the goal of achieving modular proofs for the latter. Applying the type-theoretic paradigm to concurrency has lead us to view separation logic as a type theory of state, and has motivated novel abstractions for expressing concurrency proofs based on the algebraic structure of a resource and on structure-preserving functions (i.e., morphisms) between resources.
Speaker: Arthur Azevedo de Amorim (Carnegie Mellon University)
Reconciling Noninterference and Gradual Typing
One of the standard correctness criteria for gradual typing is the dynamic gradual guarantee, which ensures that loosening type annotations in a program does not affect its behavior in arbitrary ways. Though natural, prior work has pointed out that the guarantee does not hold of any gradual type system for information-flow control. Toro et al.’s GSL Ref language, for example, had to abandon it to validate noninterference.
We show that we can solve this conflict by avoiding a feature of prior proposals: type-guided classification, or the use of type ascription to classify data. Gradual languages require run-time secrecy labels to enforce security dynamically; if type ascription merely checks these labels without modifying them (that is, without classifying data), it cannot violate the dynamic gradual guarantee. We demonstrate this idea with GLIO, a gradual type system based on the LIO library that enforces both the gradual guarantee and noninterference, featuring higher-order functions, general references, coarse-grained information-flow control, security subtyping and first-class labels. We give the language a domain-theoretic semantics, using Pitts’ framework of relational structures to prove noninterference and the dynamic gradual guarantee.
Speaker: Aaron Weiss (Northeastern University)
Oxide: The Essence of Rust
Rust claims to advance industrial programming by bridging the gap between
low-level systems programming and high-level application
programming. At the heart of the argument that this enables programmers to build
more reliable and efficient software is the borrow checker — a novel
approach to ownership which aims to balance type system expressivity with
usability. And yet, to date there is no core type system that captures Rust’s
notion of ownership and borrowing, resulting in no foundation for research on
Rust to build upon.
In this work, we set out to capture the essence of this model of ownership by
developing a type systems account of Rust’s borrow checker. To that end, we
present Oxide, a formalized programming language close to source-level
Rust (but with fully-annotated types). This presentation takes a new view of
lifetimes as an approximation of the provenances of references,
and our type system is able to automatically compute this information through a
substructural typing judgment. We then provide the first syntactic proof of type
safety for borrow checking using progress and preservation. Oxide is a
simpler formulation of borrow checking — including recent features such as
non-lexical lifetimes — that we hope researchers will be able to use as
the basis for work on Rust.
Speaker: Anitha Gollamudi (Harvard University)
Information Flow Control for Distributed Trusted Execution Environments
Distributed applications cannot assume that their security policies will be enforced on untrusted hosts. Trusted execution environments (TEEs) combined with cryptographic mechanisms enable execution of known code on an untrusted host and the exchange of confidential and authenticated messages with it. TEEs do not, however, establish the trustworthiness of code executing in a TEE. Thus, developing secure applications using TEEs requires specialized expertise and careful auditing. This paper presents DFLATE, a core security calculus for distributed applications with TEEs. DFLATE offers high-level abstractions that reflect both the guarantees and limitations of the underlying security mechanisms they are based on. The accuracy of these abstractions is exhibited by asymmetry between confidentiality and integrity in our formal results: DFLATE enforces a strong form of noninterference for confidentiality, but only a weak form for integrity. This reflects the asymmetry of the security guarantees of a TEE: a malicious host cannot access secrets in the TEE or modify its contents, but they can suppress or manipulate the sequence of its inputs and outputs. Therefore DFLATE cannot protect against the suppression of high-integrity messages, but when these messages are delivered, their contents cannot have been influenced by an attacker.
Joint work with Owen Arden and Stephen Chong.
Speaker: Stephen Chang (Northeastern University)
Improving Software Development via (Typed) Language Tailoring
Programmers intuitively understand that specialized programming
languages make them more productive. Thus, unsurprisingly, there has
been a recent explosion of new specialized languages, many created by
software companies seeking to benefit from this productivity increase.
Despite all the new languages, however, programmers still waste effort
fighting their language each time they sit down to program, since it
is infeasible for any language to be perfectly suited for every task. Or
In this talk, I argue that this wasted effort would be better directed
towards tailoring the language to be indeed exactly what the
programmer needs. I then explain how a programmer’s tools—namely,
their programming language—can support this approach to programming.
Finally, I will present a new framework for creating tailorable
*typed* languages in this manner. The tutorial will show how the
framework makes it straightforward to implement type rules that are
modular and customizable, and can even be combined into a large system
like a proof assistant.
Speaker: Paolo Perrone (MIT)
Monads, partial evaluations, and rewriting
Monads can be interpreted as encoding formal expressions, or formal operations in the sense of universal algebra. We give a construction which formalizes the idea of “evaluating an expression partially”: for example, “2+3” can be obtained as a partial evaluation of “2+2+1”. This construction can be given for any monad, and it is linked to the famous bar construction, of which it gives an operational interpretation: the bar construction induces a simplicial set, and its 1-cells are partial evaluations.
We study the properties of partial evaluations for general monads. We prove that whenever the monad is weakly cartesian, partial evaluations can be composed via the usual Kan filler property of simplicial sets, of which we give an interpretation in terms of substitution of terms.
In terms of rewritings, partial evaluations give an abstract reduction system which is reflexive, confluent, and transitive whenever the monad is weakly cartesian.
For the case of probability monads, partial evaluations correspond to what probabilists call conditional expectation of random variables.
This is part of a work in progress on a general rewriting interpretation of the bar construction.
Joint work with Tobias Fritz (Perimeter Institute for Theoretical Physics, Canada).
References: arXiv:1810.06037 and www.paoloperrone.org/phdthesis.pdf
Speaker: Michael Greenberg (Pomona College)
Executable Formal Semantics for the POSIX Shell
The POSIX shell is a widely deployed, powerful tool for managing
computer systems. The shell is the expert’s control panel, a necessary
tool for configuring, compiling, installing, maintaining, and deploying
systems. Even though it is powerful, critical infrastructure, the POSIX
shell is maligned and misunderstood. Its power and its subtlety are a
We define a formal, mechanized, executable small-step semantics for the
POSIX shell, which we call Smoosh. We compared Smoosh against seven
other shells that aim for some measure of POSIX compliance (bash, dash,
zsh, OSH, mksh, ksh93, and yash). Using three test suites—the POSIX test
suite, the Modernish test suite and shell diagnosis, and a test suite of
our own device—we found Smoosh’s semantics to be the most conformant to
the POSIX standard. Modernish judges Smoosh to have the fewest bugs
(just one, from using dash’s parser) and no quirks. To show that our
semantics is useful beyond yielding a conformant, executable shell, we
also implemented a symbolic stepper to illuminate the subtle behavior of
Smoosh will serve as a foundation for formal study of the POSIX shell,
supporting research on and development of new shells, new tooling for
shells, and new shell designs.
This talk will refine and extend my POPL 2020 talk with technical detail
on the POSIX shell itself, on Smoosh’s implementation, and on future
This is joint work with Austin J. Blatt, now an engineer at Puppet Labs.
Speaker: Anindya Banerjee (NSF)
This talk presents Peter O’Hearn’s paper “Incorrectness
Logic” (POPL 2020). In contrast to Hoare logic, incorrectness logic is
an underapproximating program logic in which one can reason
compositionally about the presence of bugs. An incorrectness triple
[p]C[\epsilon:q] with presumption p, result q, and exit condition
\epsilon says: every state in the result can be reached –normally
or erroneously–from some state in the presumption. The talk will
include the verification of various examples presented in O’Hearn’s