previous day
all days

View: session overviewtalk overview

09:00-10:00 Session 5: Invited talk by Leonardo de Moura

Invited talk by Leonardo de Moura, Microsoft Research, Redmond

Title: Dependent Type Practice

Abstract: Dependent type theory is a powerful and expressive language for writing mathematical expressions and proofs, but careful design, engineering, and hard work are needed to put the theory into practice. In this talk, I will discuss some of the ideas and techniques that have been used in the design of the Lean theorem prover, a new proof system based on dependent type theory that aims to make the theorem proving process more natural, convenient, and efficient.

10:30-12:00 Session 6: Foundations


A Logic of Proofs for Differential Dynamic Logic
SPEAKER: unknown

ABSTRACT. Differential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyber-physical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models of self-driving cars and collision avoidance protocols for aircraft. Unfortunately, these theorem provers do not have explicit proof terms, which makes the implementation of a number of important features unnecessarily complicated without soundness-critical and extra logical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counter-examples, and synthesis of surely-live deterministic programs from liveness proofs for nondeterministic programs.

This paper presents a differential dynamic logic with such an explicit representation of proofs. The resulting logic extends both the syntax and semantics of differential dynamic logic with proof terms -- syntactic representations of logical deductions. To support axiomatic theorem proving, the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions.

Constructing the Propositional Truncation using Non-recursive HITs

ABSTRACT. In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all results in a new proof assistant, Lean.

A Nominal Exploration of Intuitionism
SPEAKER: unknown

ABSTRACT. This papers extends the Nuprl proof assistant (a system representative of the class of extensional type theories a la Martin-Lof) with named exceptions and handlers, as well as a nominal fresh operator. Using these new features, we prove a version of Brouwer's Continuity Principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl's meta-theory using our formalization of Nuprl in Coq and show how we can reflect these meta-theoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl's key meta-theoretical properties, in particular consistency and the congruence of Howe's computational equivalence relation. Using continuity and the fan theorem we prove important results of Intuitionistic Mathematics: Brouwer's continuity theorem and bar induction on monotone bars.

14:00-15:30 Session 7: Verification for Concurrent and Distributed Systems

Verification for Concurrent and Distributed Systems

Bisimulation Up-to Techniques for Psi-calculi
SPEAKER: unknown

ABSTRACT. Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine- checked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework.

Bisimulation up-to techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psi- calculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up to-techniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.

Planning for Change in a Formal Verification of the Raft Consensus Protocol
SPEAKER: unknown

ABSTRACT. We present the first formal verification of the Raft consensus protocol, a critical component of many distributed systems. We proved that our implementation is a linearizable replicated state machine, which required iteratively discovering and proving nSysInv system invariants. Our verified implementation can be extracted and run on real networks.

The primary challenge we faced during the verification process was proof maintenance, since proving one invariant often required strengthening and updating other parts of our proof. To address this challenge, we propose a methodology of planning for change during verification. Our methodology adapts classical information hiding techniques to the context of proof assistants, factors out common invariant strengthening patterns into custom induction principles, proves higher-order lemmas that show any property proved about a particular component imply analogous properties about related components, and makes proofs robust to change using structural tactics. We also discuss how our methodology may be applied to systems verification more broadly.

A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
SPEAKER: unknown

ABSTRACT. We describe the formalization of a correctness proof for a conflict detection algorithm for XACML (eXtensible Access Control Markup Language). XACML is a standardized declarative access control policy language that is increasingly used in industry. In practice it is common for rule sets to grow large, and contain unintended errors, often due to conflicting rules. A conflict occurs in a policy when one rule permits a request and another denies that same request. Such errors can lead to serious risks involving both allowing access to an unauthorized user as well as denying access to someone who needs it. Removing conflicts is thus an important aspect of debugging policies, and the use of a verified algorithm provides the highest assurance in a domain where security is important. In this paper, we focus on several complex XACML constructs, including time ranges and integer intervals, as well as ways to combine any number of functions using the boolean operators and, or, and not. The latter are the most complex, and add significant expressive power to the language. We propose an algorithm to find conflicts and then use the Coq Proof Assistant to prove the algorithm correct. We develop a library of tactics to help automate the proof.

16:00-17:00 Session 8: Compiler Verification

Compiler Verification

Formal Verification of Control-flow Graph Flattening
SPEAKER: unknown

ABSTRACT. Code obfuscation is emerging as a key asset in security by obscurity. It aims at hiding sensitive information in programs so that they become more difficult to understand and reverse engineer. Since the results on the impossibility of perfect and universal obfuscation, many obfuscation techniques have been proposed in the literature, ranging from simple variable encoding to hiding the control-flow of a program.

In this paper, we formally verify in Coq an advanced code obfuscation called control-flow graph flattening, that is used in state-of-the-art program obfuscators. Our control-flow graph flattening is a program transformation operating over C programs, that is integrated into the CompCert formally verified compiler. The semantics preservation proof of our program obfuscator relies on a simulation proof performed on a realistic language, the Clight language of CompCert. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.

Axiomatic Semantics for Compiler Verification
SPEAKER: unknown

ABSTRACT. Based on constructive type theory, we study two idealized imperative languages GC and IC and verify the correctness of a compiler from GC to IC. GC is a guarded command language with underspecified execution order defined with an axiomatic semantics. IC is a deterministic low-level language with linear sequential composition and lexically scoped gotos defined with a small-step semantics. We characterize IC with an axiomatic semantics and prove that the compiler from GC to IC preserves specifications. The axiomatic semantics we consider model total correctness and map programs to continuous predicate transformers. We define the axiomatic semantics of GC and IC with elementary inductive predicates and show that the predicate transformer described by a program can be obtained compositionally by recursion on the syntax of the program using a fixed point operator for loops and continuations. We also show that two IC programs are contextually equivalent if and only if their predicate transformers are equivalent.

18:00-21:00 Session

CPP Reception, sponsored by the DeepSpec project

The Science of Deep Specification is a new U.S. National Science Foundation initiative on applying proof assistants at scale to system verification.  Come learn about the project, with a brief presentation by Benjamin Pierce, plus, of course, plenty of food, drink, and socializing.