Microarchitectural attacks, such as Spectre and Meltdown, illustrate that artifacts of hardware implementations (like speculative and out-of-order execution) can result in measurable side-effects on program execution time that attackers can exploit to compromise a system’s security. These attacks arise from emerging behaviors obtained when combining hardware and software. Building systems that are resistant against these attacks requires fundamentally rethinking the design of existing security mechanisms. In this talk, I will focus on speculative execution attacks--a specific class of microarchitectural attacks--and I will illustrate a principled approach for reasoning about security against these attacks. The key component of this approach is a*leakage contract*, a formal ISA-level specification of the information that may be leaked through microarchitectural side-effects. Concretely, I will present (1) how to model the information flows at the core of Spectre-style attacks, (2) how to formalize leakage contracts, and (3) how to use contracts to reason about the security of hardware and software.

Vector Commitments allow one to (concisely) commit to a vector of messages so that one can later (concisely) open the commitment at selected locations. In the state of the art of vector commitments, {\em algebraic} constructions have emerged as a particularly useful class, as they enable advanced properties, such as stateless updates, subvector openings and aggregation, that are for example unknown in Merkle-tree-based schemes. In spite of their popularity, algebraic vector commitments remain poorly understood objects. In particular, no construction in standard prime order groups (without pairing) is known. In this paper, we shed light on this state of affairs by showing that a large class of concise algebraic vector commitments in pairing-free, prime order groups are impossible to realize. Our results also preclude any cryptographic primitive that implies the algebraic vector commitments we rule out, as special cases. This means that we also show the impossibility, for instance, of succinct polynomial commitments and functional commitments (for all classes of functions including linear forms) in pairing-free groups of prime order.

Cryptographic accumulators are a common solution to proving information about a large set . They allow to compute a short digest of and short certificates of some of its basic properties, notably membership of an element. Accumulators also allow to track set updates: a new accumulator is obtained by inserting/deleting a given element. In this work we consider the problem of generating membership and update proofs for batches of elements so that we can succinctly prove additional properties of the elements (i.e., proofs are of constant size regardless of the batch size), and we can preserve privacy. Solving this problem would allow to obtain blockchain systems with improved privacy and scalability.

Programs that deal with heap-allocated inputs are difficult to analyze with symbolic execution (SE). Lazy Initialization (LI) is an approach to SE that deals with heap-allocated inputs by starting SE over a fully symbolic heap, and initializing the inputs' fields on demand, as the program under analysis accesses them. However, when the program's assumed precondition has structural constraints over the inputs, operationally captured via repOK routines, LI may produce spurious symbolic structures, making SE traverse infeasible paths and undermining SE's performance.

In this talk I will present LISSA, our solution to efficiently detect and prune paths containing spurious symbolic structures. LISSA employs a novel structural constraint solver, SymSolve, capable of deciding satisfiability of partially symbolic structures. We experimentally assess LISSA against related techniques over various case studies, consisting of programs with heap-allocated inputs with complex constraints. The results show that LISSA is faster and scales better than related techniques.