POPV Seminars

Weekly Principles of Programming and Verification seminars are now held in a hybrid format on Tuesday from 4 pm to 5:30 pm ET in-person meeting will be held in Hariri seminar room MCS 157, and Zoom link will be sent out in POPV mailling list.

You can subscribe to the POPV mailing list here.

If you are interested in attending, please contact the organizer Cheng Zhang czhang03@bu.edu.

 


Schedule (Spring 2022)

Below is a list of seminar dates for with information on the speakers:

Date Speaker Talk Title
Feb 22 Michael Greenberg (Stevens Institute of Technology) Logical Tools for the PL Practitioner: from Datalog and SMT to ASP and Beyond.
Mar 1 No Talk
Mar 8 No Talk (Spring Recession)
Mar 15 No Talk
Mar 22 Benoît Montagu  (Inria) Trace-Based Control-Flow Analysis (Part 1)
Mar 29 Benoît Montagu  (Inria) Trace-Based Control-Flow Analysis (Part 2)
Apr 5 Li-yao Xia (University of Pennsylvania) Executable Denotational Semantics with Interaction Trees
Apr 12 Aaron Stump (The University of Iowa) From Inductive Lambda Encodings to Divide-and-Conquer Recursion
Apr 19 Pedro Azevedo de Amorim (Cornell University) Distribution Theoretic Semantics for Non-Smooth Differentiable Programming
Apr 26 Jonathan Sterling (Aarhus University) Intrinsic semantics of termination-insensitive noninterference
May 3 Robert Rand (University of Chicago) Verifying Quantum Programs: From Deutsch’s Algorithm to Shor’s
May 5 Gabriele Vanoni (University of Bologna) Reasonable Space for the Lambda-Calculus, Logarithmically
May 10 Eric Koskinen (Stevens Institute of Technology) Programming with Commutativity
May 31 Robert Y. Lewis (Brown University) TBA

 

Logical Tools for the PL Practitioner: from Datalog and SMT to ASP and Beyond

Time: Feb 22nd, Tuesday, 4:00pm Eastern Time

Speaker: Michael Greenberg (Stevens Institute of Technology)

Abstract: In an ideal world, the formalism we prove things about would neatly match the artifact we implement. Various logical tools help us bridge the gap between theoretical, paper proofs and practical, efficient implementations.
Datalog and SMT have long been acknowledged as powerful tools in the PL practitioner’s toolbox. Datalog use is on the rise; SMT is pervasive. Both tools marry classical logics with efficient implementations; both tools offer declarative languages supported by powerful, complex implementations.
I’ll first talk about how our Formulog language combines Datalog, SMT, and functional programming. Formulog helps bridge the theory/practice gap with efficiently executable, formal artifacts.
Then I’ll talk about a recent application of answer set programming (ASP) to a Datalog synthesis problem. ASP is a powerful technology combining features of Datalog and SAT, and it deserves to be better known in the PL community.
This is joint work with Steve Chong and Aaron Bembenek, both at Harvard.

Bio: Michael Greenberg is an assistant professor at Stevens Institute of Technology. He received BAs in Computer Science and Egyptology from Brown University (2007) and his PhD in Computer Science from the University of Pennsylvania (2013); previously, he was an assistant professor at Pomona College. His work has ranged from functional-reactive JavaScript (with Shriram Krishnamurthi at Brown) to runtime verification of higher-order programs (with Benjamin Pierce at Penn) to software-defined networking (with Dave Walker at Princeton) to present activities focused on the POSIX shell and executable formalism.

 

 

Trace-Based Control-Flow Analysis

Time: Mar 22nd, Tuesday, 4:00pm Eastern Time

Speaker: Benoît Montagu  (Inria)

Abstract: I will present some recent advances in control-flow analysis (CFA) for the untyped lamba-calculus, a classic static analysis for higher-order languages.

First, I will explain how the well-known k-CFA analysis can be obtained in a simple manner, by abstracting the execution traces of a lambda-term. To this end, I will introduce a small-step semantics that builds a trace of the control-flow events (calls, and returns of functions) that are produced by a program. Using this technical development, the constraint-based formulation of k-CFA can be proved sound in a modular way, as opposed to the usual method based on “subject reduction”.

Then, building on the previous development, I will introduce a novel control-flow analysis, called nabla-CFA, that uses a widening operator. Experiments show that nabla-CFA converges faster in practice compared to k-CFA. Nabla-CFA also enables the use of domains of unbounded heights, such as intervals—a new point in the design space of CFAs. I will discuss how nabla-CFA compares to k-CFA in terms of cost and precision and, if time permits, sketch some recent developments that solve some of the limitations of nabla-CFA.

This work was presented at PLDI’21.

 

Executable Denotational Semantics with Interaction Trees

Time: Apr 5th, Tuesday, 4:00pm Eastern Time

Speaker: Li-yao Xia (University of Pennsylvania)

Abstract: Machine-checked proofs are now feasible at scale, in a wide variety of  domains. As the systems we verify become more complex, a growing challenge is to relate specifications across many abstraction layers, expressed in disparate formalisms.

Interaction trees are a model to represent the behavior of effectful and reactive systems. Interaction trees are implemented as a library in the Coq proof assistant. This model is modular, compositional, and executable, which makes it applicable to express specifications at many layers of the computing stack. I discuss two applications. First, we verify a compiler from a simple imperative language to assembly, by proving a semantic preservation theorem which is termination-sensitive, using an equational proof. Second, we build a framework of concurrent objects. Concurrent objects are implemented using interaction trees, leveraging the functionalities provided by the library. The framework supports proof techniques for both linearizability and strict serializability, two well-known correctness conditions for concurrent objects.

 

 

From Inductive Lambda Encodings to Divide-and-Conquer Recursion

Time: Apr 12th, Tuesday, 4:00pm Eastern Time

SpeakerAaron Stump (The University of Iowa)

Abstract: This talk begins with typed lambda encodings, where data like numbers, lists, and trees are represented as terms of pure lambda calculus, typable using impredicative polymorphism.  The inability to derive induction for such encodings in the Calculus of Constructions (CC) led historically to the development of the Calculus of Inductive Constructions (CIC), the type theory underlying Coq.  In CIC, inductive types are added to the theory as primitives.  We will see an alternative, where induction can be derived in an extension of CC with dependent intersection types.  This derivation has been implemented in the Cedille prover, and is the basis for Cedille’s elaboration of inductive types to its core theory.  Going further, we will see how to derive a new form of recursion/induction called divide-and-conquer recursion.  This form of recursion allows one to initiate subsidiary inner recursions which can construct data upon which outer recursions may legally recurse.  This allows direct implementation in total type theory of algorithms like mergesort, quicksort, etc., which otherwise require methods like well-founded recursion.  Amazingly, these ideas can be realized not just in a somewhat exotic prover like Cedille, but in Coq.

Bio: Aaron Stump is a professor of Computer Science at The University of Iowa.  His current research interests are in new foundations for type theory, as well as total functional programming.  He is the creator of The Iowa Type Theory Commute podcast.

 

 

Distribution Theoretic Semantics for Non-Smooth Differentiable Programming

Time: Apr 19th, Tuesday, 4:00pm Eastern Time

SpeakerPedro Azevedo de Amorim (Cornell University)

Abstract: With the widespread of deep learning and gradient descent inspired optimization algorithms, differentiable programming has gained traction. Nowadays it has found applications in many different areas as well, such as scientific computing, robotics, computer graphics and others. One of its notoriously difficult problems consists in interpreting programs that are not differentiable everywhere.

In this work we define , a core calculus for non-smooth differentiable programs and define its semantics using concepts from distribution theory, a well-established area of functional analysis. We also show how presents better equational properties than other existing semantics and use our semantics to reason about a simplified ray tracing algorithm.

 

 

Intrinsic semantics of termination-insensitive noninterference

Time: Apr 26th, Tuesday, 4:00pm Eastern Time

Speaker: Jonathan Sterling (Aarhus University)

Abstract: Security-typed programming languages aim to control the flow of high-security information to low security clients. Starting with Abadi et al.’s dependency core calculus, the denotational semantics of such languages has been dominated by an extrinsic approach in which an existing insecure model of computation (e.g. ordinary domains) is restricted by a logical relation of “indistinguishability” to prevent low-security outputs from depending on high-security inputs (noninterference). Thus in the extrinsic approach, security properties are bolted onto an insecure model by brute force, as it were. A more refined information flow policy called termination-insensitive noninterference allows high-security bits to be leaked through termination channels but not through return values; unfortunately, the adaptation of the extrinsic/relational semantics to this more relaxed policy is incompatible with the transitivity of the logical relation, contradicting the intuition of “indistinguishability”.

In contrast, an intrinsic semantics of security typing would involve a new computational model that evinces secure information flow and noninterference properties directly without any post hoc restriction by a logical relation. We contribute the first such intrinsic semantics of security typing in this sense by considering sheaves of dcpos on a space of abstract behaviors on which security classes arise as open/closed partitions; the security monads then arise as the closed modalities of topos theory that restrict a sheaf to its component over a closed subspace.

An advantage of our intrinsic semantics is that termination-insensitive noninterference arises automatically from our computational model, namely the fact that the Sierpiński domain is not a constant sheaf; a further advantage is that our semantics is an instance of standard domain theoretic denotational semantics, albeit over a richer category of domains. This is joint work with Robert Harper.

Preprint: Sheaf semantics of termination-insensitive noninterference

Bio: Jonathan Sterling is a Marie Skłodowska-Curie Postdoctoral Fellow at Aarhus University, supervised by Lars Birkedal; previously he received his Ph.D. from Carnegie Mellon University where he was advised by Robert Harper.

 

 

Verifying Quantum Programs: From Deutsch’s Algorithm to Shor’s

Time: May 3rd, Tuesday, 4:00pm Eastern Time

SpeakerRobert Rand (University of Chicago)

Abstract:  Ensuring the correctness of quantum programs is a challenging but critical problem. As a field, quantum computing has developed a broad range of powerful algorithms, with applications from computer security to machine learning. However, while these algorithms have been programmed in a variety of languages, they have never been executed: We simply don’t have quantum or classical computers capable of doing the job. The implementations are likely to fail on real-world quantum computers and when they do so, we will not be able to easily diagnose the errors. Formal verification has proven remarkably successful in addressing this problem, despite the many complications of quantum computing. In this talk, I will review progress in this domain, from early work on verifying Deutsch’s algorithm and quantum teleportation in the QWIRE language to a brand new proof of Shor’s algorithm using the proof-focused SQIR intermediate representation.

Familiarity with the Coq proof assistant will be useful in understanding the details of this talk, no quantum computing background will be assumed.

Bio: Robert Rand is an Assistant Professor of Computer Science at the University of Chicago. His research focuses on programming languages and verification for quantum computing and his main projects include the QWIRE quantum circuit language, the VOQC compiler for quantum circuits, and a stabilizer-based type system for quantum programs. He is currently developing tools for novel models of quantum computation like the ZX-calculus and the one-way quantum computer. Robert developed and maintains the INQWIRE QuantumLib, an open-source library for verified quantum computing in the Coq proof assistant, which underlies many of his projects including his online textbook, Verified Quantum Computing.

Paper link(s):

https://arxiv.org/pdf/2010.01240.pdf (ITP paper)

https://arxiv.org/pdf/2204.07112.pdf (Shor’s algorithm preprint)

 

 

Reasonable Space for the Lambda-Calculus, Logarithmically

Time: May 5th, Thursday, 4:00pm Eastern Time

SpeakerGabriele Vanoni (University of Bologna)

Abstract: Can the lambda-calculus be considered as a reasonable computational model? Can we use it for measuring the time and space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the lambda-calculus, based on a variant over the Krivine abstract machine. For the first time, this cost model is able to account for logarithmic space. Moreover, we study the time behavior of our machine and show how to transport our results to the call-by-value lambda-calculus. Finally, we give a system of non-idempotent intersection types that is able to capture exactly the newly introduced space measure.

Short Bio: Gabriele Vanoni completed its PhD program at Università di Bologna working under the supervision of Ugo Dal Lago. He has worked mainly on implementation techniques and complexity analysis for the lambda-calculus. He has spent five months at LIPN in Paris, visiting Damiano Mazza, and is currently visiting the FLINT group, led by Zhong Shao, at Yale University.

 

 

Programming with Commutativity

Time: May 10th, Tuesday, 4:00pm Eastern Time

SpeakerEric Koskinen (Stevens Institute of Technology)

Abstract: There is an ongoing effort to provide programming abstractions that ease the burden of exploiting multicore hardware. Many programming abstractions (eg, concurrent objects, transactional memory, etc.) simplify matters, but still involve intricate engineering. We argue that some difficulty of multicore programming can be meliorated through a declarative programming style in which programmers directly express the independence of fragments of sequential programs.

I will describe a new language paradigm in which programmers write programs in a familiar, sequential manner, with the added ability to explicitly express the conditions under which code fragments sequentially commute. Putting such commutativity conditions into source code offers a new entry point for a compiler to exploit the known connection between commutativity and parallelism. I will discuss semantic implications and how to ensure equivalence between the parallel and sequential semantics.

Commutativity conditions (in our and other settings) must be sound or else concurrent execution could be incorrect. I will next describe a series of work (TACAS’18, VMCAI’21) in which we automatically verify and even synthesize commutativity conditions of programs.

 

 


Schedule (Fall 2021)

Below is a list of seminar dates for with information on the speakers:

Date Speaker Talk Title
Sep 28 Yao Li (University of Pennsylvania) Reasoning About the Garden of Forking Paths
Oct 05 Brittany Nkounkou (University of Connecticut) A Certified Scalably Executable Semantics for Nondeterministic True-Concurrent Languages
Oct 12 Julia Belyakova (Northeastern University) Julia: Language Design and Users Working Together.
Oct 19 Ethan Cecchetti (Maryland Cybersecurity Center) Compositional Security for Reentrant Applications
Oct 26 Nada Amin (Havard University) Beyond Collapsing Towers: Staging a Relational Interpreter
Nov 02 Andrew Hirsch (Max Planck Institute for Software Systems) Semantic Technique For Information Flow Languages
Nov 09 Arjun Guha (Northeastern University) Solver-Based Gradual Type Migration
Nov 16 Aymeric Fromherz (Inria Paris) Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic
Nov 23 Caroline Lemieux  (Microsoft Research) Expanding the Reach of Fuzzing
Nov 30
Dec 07 Ralf Jung (MIT) RustBelt: A Deep Dive Into The Abyss
Dec 14 Robin Fu (Boston University) The Calculus of Linear Constructions

Abstracts

Reasoning about the garden of forking paths

Speaker: Yao Li (University of Pennsylvania)

Time: Sep 28th, Tuesday, 4:00pm Eastern Time

Abstract: Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program’s computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq.

Paper link: https://doi.org/10.1145/3473585 (you do NOT need to read the paper; I just post the link here for reference)

Code link: https://github.com/lastland/ClairvoyanceMonad

 

A Certified Scalably Executable Semantics for Nondeterministic True-Concurrent Languages

Speaker: Brittany Nkounkou (University of Connecticut)

Time: Oct 05th, Tuesday, 4:00pm Eastern Time

Abstract: A nondeterministic true-concurrent language defines the possible behavior of two parallel indivisible operations to include both the nondeterministic interleaving of the operations and their simultaneous execution. Executing largely parallel programs in such a language is especially challenging if it must satisfy some global predicate over simultaneously executed operations that cannot be inferred from some local predicate over each of its individual operations. In this talk, I will address this challenge with a labelled-transition operational semantics that is (1) mechanically formalized and (2) readily parametric over fitting nondeterministic true-concurrent languages, and whose execution is (3) mechanically verified and (4) scalable with respect to largely parallel programs. The semantics is built using the Coq proof assistant and utilizes a modular continuation-passing-style approach to its execution. I’ll exemplify the scalability and applicability of the semantics by using it to simulate the first asynchronous microprocessor, a largely parallel program in the nondeterministic true-concurrent language Communicating Hardware Processes (CHP). I further compare this simulation in our framework to that in Maude. This work is currently under double-blind review.

 

Julia: Language Design and Users Working Together.

Speaker: Julia Belyakova (Northeastern University)

Time: Oct 12th, Tuesday, 4:00pm Eastern Time

Abstract: As a programming language for scientific computing, Julia strives for predictable performance as well as flexibility and ease of use. To tackle this challenge, Julia employs two strategies. First, it enables highly compositional programs by using multiple dispatch as the core paradigm, but at the same time, pragmatically restricts the language to facilitate optimizations. Second, Julia enables productive collaboration between the programmer and the JIT compiler by making the compiler’s behavior predictable and encouraging optimization-conducive coding discipline.
In this talk, we look at several components of this two-fold approach. We start with an overview of multiple dispatch. Next, we talk about type stability, a property of the code that enables the key optimization in Julia’s optimization pipeline. Finally, we look at the world age, a mechanism that allows for a pragmatic trade-off between flexibility of “eval” and predictability of compiler optimizations.

 

Compositional Security for Reentrant Applications

Speaker: Ethan Cecchetti (Maryland Cybersecurity Center)

Time: Oct 19th, Tuesday, 4:00pm Eastern Time

Abstract: The disastrous vulnerabilities in smart contracts sharply remind us of our ignorance: we do not know how to write code that is secure in composition with malicious code. Information flow control has long been proposed as a way to achieve compositional security, offering strong guarantees even when combining software from different trust domains. Unfortunately, this appealing story breaks down in the presence of reentrancy attacks. In this talk I will present a highly general definition of reentrancy and reentrancy security that allows software modules like smart contracts to protect their key invariants while retaining the expressive power of safe forms of reentrancy. I will describe how we can combine a type system and run-time mechanism to enforce this new notion of security even in the presence of unknown code.

This work recently received a best paper award at IEEE S&P ’21. The paper is available at https://ethan.umiacs.io/papers/serif.pdf

Bio: Ethan is currently a post-doc at the University of Maryland working primarily with Mike Hicks and is on the market for tenure-track academic jobs this year. His research focuses broadly on designing secure decentralized systems and building tools to ease their development using programming languages and applied cryptography. He completed his PhD at Cornell in August 2021 working with Andrew Myers and Ari Juels. More information is available at his website: https://ethan.umiacs.io/

 

Beyond Collapsing Towers: Staging a Relational Interpreter

Speaker: Nada Amin (Havard University)

Time: Oct 26th, Tuesday, 4:00 pm Eastern Time

Abstract: Staging — splitting a program into stages, the code generator and the generated code — can mechanically turn an interpreter into a compiler. Going further, we can collapse a tower of interpreters into a one-pass compiler.
An interpreter written in a relational programming language (miniKanren) for a functional programming language (subset of Racket) can not only evaluate an expression to a value, but also synthesize an expression (or more generally, term) for a hole — in particular, turning functions into relations.
We adapt staging to the relational setting, turning functions into relations — and more — with reduced interpretive overhead, promising a tractable avenue for the synthesis of functional programs.

Semantic Techniques for Information-Flow Languages

SpeakerAndrew Hirsch (Max Planck Institute for Software Systems)

Time: Nov 02th, Tuesday, 4:00 pm Eastern Time

Abstract: Information-flow languages enforce information-security policies for any program written in them. The most basic security policy of such languages is noninterference, which states that secret inputs do not affect the observations of an adversary. However, current practices for developing and proving correct information-flow languages rely exclusively on hand-rolled proofs, making exploration of the design space slow and labor intensive. Moreover, proofs are almost never given for implementations of information-flow languages.In this talk, I discuss how semantic techniques can alleviate some of this burden by providing general frameworks for noninterference proofs. In particular, I discuss how the semantics of effects eases the burden of proof for the source language,  how denotational semantics can ease proofs of security preservation for compilers, and how modal logics can ensure that low-level security enforcement preserves noninterference.

 

Solver-Based Gradual Type Migration

Speaker: Arjun Guha (Northeastern University)

Time: Nov 09th, Tuesday, 4:00 pm Eastern Time

Abstract: Gradually typed languages allow programmers to mix statically and dynamically typed code, enabling them to incrementally reap the benefits of static typing as they add type annotations to their code. However, this type migration process is typically a manual effort with limited tool support. In this talk, we examine the problem of automated type migration: given a dynamic program, infer additional or improved type annotations.

Existing type migration algorithms prioritize different goals, such as maximizing type precision, maintaining compatibility with unmigrated code, and preserving the semantics of the original program. We argue that the type migration problem involves fundamental compromises: optimizing for a single goal often comes at the expense of others. Ideally, a type migration tool would flexibly accommodate a range of user priorities.

We present TypeWhich, a new approach to automated type migration for an extension of the gradually-typed lambda calculus. Unlike prior work, which relies on custom solvers, TypeWhich produces constraints that can be solved by an off-the-shelf MaxSMT solver. This allows us to easily express objectives, such as minimizing the number of necessary syntactic coercions, and constraining the type of the migration to be compatible with unmigrated code.

We present the first comprehensive evaluation of GTLC type migration algorithms, and compare TypeWhich to four other tools from the literature. Our evaluation uses prior benchmarks, and a new set of “challenge problems”. Moreover, we design a new evaluation methodology that highlights the subtleties of gradual type migration. In addition, we apply TypeWhich to a suite of benchmarks for Grift, a programming language based on the GTLC. TypeWhich is able to reconstruct all human-written annotations on all but one program.

Biography: Arjun Guha is an associate professor of Computer Science at Northeastern University. Using the tools and techniques of programming languages, his research addresses security, reliability, and performance problems in web applications, systems, networking, and robotics. His work has received an ACM SIGPLAN Most Influential Paper Award, an ACM SIGPLAN Distinguished Paper Award, an ACM SIGPLAN Research Highlight, and a Google Faculty Research Award.

 

Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic

Speaker: Aymeric Fromherz (Inria Paris)

Time: Nov 16th, Tuesday, 4:00 pm Eastern Time

Abstract: Modern software increasingly exploits parallelism to reach new heights of performance. Unfortunately, concurrent programming is error-prone, and developers often make incorrect assumptions about how their programs will behave, raising concerns about its use in critical systems. Using formal methods to provide strong correctness guarantees is appealing, but challenging; verification frameworks either lack the expressivity required to model every advanced low-level pattern found in real-world implementations, or they do not retain the level of automation needed to ensure the scalability of verification. To address this issue, we present Steel, a new verification framework to develop and prove concurrent programs embedded in F*, a dependently typed programming language and proof assistant.

In this talk, we give an overview of Steel from the ground up.
To reason about programs, Steel provides a higher-order, impredicative concurrent separation logic with support for dynamically-allocated invariants and partial commutative monoids (PCMs). To automate verification, Steel separates verification conditions between separation logic predicates and first-order logic encodeable predicates; we develop a (partial) decision procedure using efficient, reflective tactics that focuses on the former, while the latter can be encoded efficiently to SMT by F*. We will conclude by presenting several verified Steel libraries, including mutable, self-balancing trees as well as a novel PCM-based encoding of 2-party dependently typed sessions, that illustrate the expressiveness and programmability of Steel.

 

Expanding the Reach of Fuzzing

Speaker: Caroline Lemieux  (Microsoft Research)

Time: Nov 16th, Tuesday, 4:00 pm Eastern Time

AbstractSoftware bugs are pervasive in modern software. As software is integrated into increasingly many aspects of our lives, these bugs have increasingly severe consequences, both from a security (e.g. Cloudbleed, Heartbleed, Shellshock) and cost standpoint. Fuzzing refers to a set of techniques that automatically find bug-triggering inputs by sending many random-looking inputs to the program under test. In this talk, I will discuss how, by identifying core under-generalized components of modern fuzzing algorithms, and building algorithms that generalize or tune these components, I have expanded the application domains of fuzzing. First, by building a general feedback-directed fuzzing algorithm, I enabled fuzzing to consistently find performance and resource consumption errors. Second, by developing techniques to maintain structure during mutation, I brought fuzzing exploration to “deeper” program states. Third, by decoupling the user-facing abstraction of random input generators from their sampling distributions, I built faster validity fuzzing and even tackled program synthesis. Finally, I will discuss the key research problems that must be tackled to make fuzzing readily-available and useful to all developers.

Bio: Caroline Lemieux is a Postdoc at Microsoft Research and incoming Assistant Professor at the University of British Columbia. Her research aims to help developers improve the correctness, security, and performance of large, existing software systems, ranging from complex open-source projects to industrial-scale software. Her current projects tackle these goals with a focus on fuzz testing and program synthesis. Her work on fuzz testing has been awarded an ACM SIGSOFT Distinguished Paper Award, ACM SIGSOFT Distinguished Artifact Award, ACM SIGSOFT Tool Demonstration Award, and Best Paper Award (Industry Track). She received her PhD at UC Berkeley advised by Koushik Sen, and her B.Sc. in Combined Honours Computer Science and Mathematics at UBC . She is the recipient of a Berkeley Fellowship for Graduate Study and a Google PhD Fellowship in Programming Technologies and Software Engineering.

 

RustBelt: A deep dive into the Abyss

Speaker: Ralf Jung (MIT)

Time: Dec 07th, Tuesday, 4:00 pm Eastern Time

Abstract: Rust is a young systems programming language that aims to fill the gap between high-level languages — which provide strong static guarantees like memory and thread safety — and low level languages — which give the programmer fine-grained control over data layout and memory management. This talk gives an introduction to RustBelt, a formal model of Rust’s type system, together with a soundness proof establishing memory and thread safety. The model is designed to verify the safety of a number of intricate APIs from the Rust standard library, despite the fact that the implementations of these APIs use unsafe language features. After explaining the basics of RustBelt and the general approach of semantic type safety, we will look at the safety proof of one particularly interesting Rust API: the Cell type, which seemingly breaks some of the fundamental constraints of the Rust type system by permitting mutation of shared state.

 

Title: The Calculus of Linear Constructions

Speaker: Robin Fu (Boston University)

Time:Dec 14th, Tuesday, 4:00 pm Eastern Time

Abstract: The Calculus of Linear Constructions (CLC) is an extension of the Calculus of Constructions (CC) with linear types. Specifically, CLC extends the predicative CC? with a hierarchy of linear universes that precisely controls the weakening and contraction of its term level inhabitants. We study the meta-theory of CLC, showing that it is a sound logical framework for reasoning about resource. We further extend CLC with rules for defining inductive linear types in the style of CIC, forming the Calculus of Inductive Linear Constructions (CILC). Through examples, we demonstrate that CILC facilitates correct by construction imperative programming and lightweight protocol enforcement. We have formalized and proven correct all major results in the Coq Proof Assistant.

 


Below is a list of seminar dates for Fall 2020 with information on the speakers:

Date Speaker Talk Title
Sep 22 Ankush Das
(Carnegie Mellon University)
Resource-Aware Session Types for Digital Contracts
Sep 29 Social Time
Oct 06 Jonathan Protzenko
(Microsoft Research)
Latest advances in scaling cryptographic verification in F*
Oct 13 June Wunder
(Boston University)
Agda Tutorial
Oct 20 Assaf Kfoury
(BU)
First-Order Term Rewriting (compressed tutorial)
Oct 27 Ben Greenman
(Northeastern University)
Complete Monitoring for Gradual Types
Nov 03 Mirai Ikebuchi
(MIT)
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
(Northeastern University)
Compositional Optimizations for CertiCoq
Dec 1 Stephanie Balzer
(Carnegie Mellon University)
Manifest Deadlock-Freedom for Shared Session Types
Dec 8 Clément Pit-Claudel
(MIT)
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

Abstracts

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 [1]. 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 [2].

[1] 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.
[2] https://github.com/uds-psl/coq-library-undecidability

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
truly anything.

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.

Bio:
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.


Spring-Summer 2020

Below is a list of seminar dates for Spring-Summer 2020 with information on the speakers:

Date Speaker Talk Title
Jan 28 Alley Stoughton
(Boston University)
You Sank My Battleship! A Case Study in Secure Programming
Feb 4 Chris Casinghino
(Draper Labs)
A Language for Programmable Hardware Security
Feb 11 Ugo Dal Lago
(University of Bologna)
Differential Program Semantics
Feb 18 Riyadh Baghdadi
(MIT)
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
(Boston University)
Dependent Types to Support Continuous Offline Testing
Mar 24 Aaron Bembenek
(Harvard University)
Formulog: Datalog for SMT-based Static Analysis
Mar 31 No Talk No Talk
Apr 7 Marco Gaboardi
(Boston University)
Bounded Linear Logic and Metric Interpretation
Apr 14 No Talk No Talk
Apr 21 Joseph Tassarotti
(Boston College)
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
(Northeastern University)
Oxide: The Essence of Rust
June 2 Anitha Gollamudi
(Harvard University)
Information Flow Control for Distributed Trusted Execution Environments
June 9 Stephen Chang
(Northeastern University)
Improving Software Development via (Typed) Language Tailoring
June 16 Paolo Perrone
(MIT)
Monads, partial evaluations, and rewriting
June 23 Michael Greenberg
(Pomona College)
Executable Formal Semantics for the POSIX Shell
June 30 Anindya Banerjee
(NSF)
Incorrectness Logic
July 7 Anindya Banerjee
(NSF)
Incorrectness Logic

Abstracts

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.

Based upon:
* 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.

Arxiv: https://arxiv.org/abs/2004.08450

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
is it?

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
dangerous combination.

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
the shell.

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

This is joint work with Austin J. Blatt, now an engineer at Puppet Labs.

Speaker: Anindya Banerjee (NSF)

Incorrectness Logic

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