Tools for verifying leakage descriptions of hardware aim to ensure that a given hardware design doesn’t leak secrets via its microarchitecture, when executing programs with appropriate countermeasures. However, existing techniques for proving correctness of leakage descriptions are based on non-constructive proofs via non-interference. As a result, they often rely on expensive solvers that offer little help when verification fails or require handwritten invariants, which are difficult to come up with and even harder to debug. In this paper, we present a new approach to leakage verification which we call simulation-based leakage proofs. To show that a leakage description correctly captures a hardware design using a simulation-based proof, the user constructs a simulator—another hardware design that must faithfully replicate all attacker-observable behavior from explicitly leaked secrets. Simulation-based proofs therefore offer a constructive alternative to classic non-interference proofs, exposing a proof object—the simulator, witnessing the correctness claim. As simulators are just programs, we can write, execute and debug them like any other program, making them easy to use. We also show that they can be checked locally, which makes proof checking fast. We implement simulation-based leakage proofs in Pantomime, a tool that supports writing processors and their leakage proofs in Haskell; we report on using Pantomime to write and verify AIMCore, a 5-stage in-order processor, its leakage description, and simulator, as well as a side-channel hardened version of the core. We show that Pantomime verifies them efficiently (it checks AIMCore in under 40s), and use AIMCore’s leakage description to check for leakages in crypto libraries which uncovered two new vulnerabilities in wolfSSL that have both been assigned CVE’s.

Many proofs of interactive cryptographic protocols (e.g., as in Universal Composability) operate by proving the protocol at hand to be observationally equivalent to an idealized specification. While pervasive, formal tool support for observational equivalence of cryptographic protocols is still a nascent area of research. Current mechanization efforts tend to either focus on diff-equivalence, which establishes observational equivalence between protocols with identical control structures, or require an explicit witness for the observational equivalence in the form of a bisimulation relation. Our goal is to simplify proofs for cryptographic protocols by introducing a core calculus, IPDL, for cryptographic observational equivalences. Via IPDL, we aim to address a number of theoretical issues for cryptographic proofs in a simple manner, including probabilistic behaviors, distributed message-passing, and resource-bounded adversaries and simulators. We demonstrate IPDL on a number of case studies, including a distributed coin toss protocol, Oblivious Transfer, and the GMW multi-party computation protocol. All proofs of case studies are mechanized via an embedding of IPDL into the Coq proof assistant.

The Eckmann-Hilton argument shows that any two monoid structures on the same set satisfying the interchange law are in fact the same operation, which is moreover commutative. When the monoids correspond to the vertical and horizontal composition of a sufficiently higher-dimensional category, the Eckmann-Hilton argument itself appears as a higher cell. This cell is often required to satisfy an additional piece of coherence, which is known as the syllepsis. We show that the syllepsis can be constructed from the elimination rule of intensional identity types in Martin-Löf type theory.

Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us to give short proofs of a number of useful corollaries, some of which were conjectured in other works: the commutativity of sequential colimits with identity types, with homotopy fibers, loop spaces, and truncations, and the preservation of the properties of truncatedness and connectedness under sequential colimits. Our entire development carries over to (∞, 1)-toposes using Shulman's recent interpretation of homotopy type theory into these structures.

Reynolds' original theory of relational parametricity was intended to capture the observation that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formulated in a metatheory with an impredicative universe, such as the Calculus of Inductive Constructions. A number of more abstract treatments of relational parametricity have since appeared; however, as we show, none of these seem to express Reynolds' original theory in a satisfactory way.

Homotopy type theory is a new branch of mathematics that merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us to represent a variety of mathematical objects as basic type-theoretic construction, higher inductive types. We present a proof that in homotopy type theory, the torus is equivalent to the product of two circles. This result indicates that the synthetic definition of torus as a higher inductive type is indeed correct.

Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs.

Logical relations are a central concept used to study various higher-order type theories and occur frequently in the proofs of a wide variety of meta-theorems. Besides extending the logical relation principle to more general languages, an important research question has been how to represent and thus verify logical relation arguments in logical frameworks. We formulate a theory of logical relations for Dependent Type Theory (DTT) with β η-equality which guarantees that any valid logical relation satisfies the Basic Lemma. Our definition is syntactic and reflective in the sense that a relation at a type is represented as a DTT type family but also permits expressing certain semantic definitions. We use the Edinburgh Logical Framework (LF) incarnation of DTT and implement our notion of logical relations in the type-checker Twelf. This enables us to formalize and mechanically decide the validity of logical relation arguments. Furthermore, our implementation includes a module system so that logical relations can be built modularly. We validate our approach by formalizing and verifying several syntactic and semantic meta-theorems in Twelf. Moreover, we show how object languages encoded in DTT can inherit a notion of logical relation from the logical framework.

Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.