Search

In this paper we revisit the problem of erasing sensitive data from memory and registers during return from a cryptographic routine. While the problem and related attacker model is fairly easy to phrase, it turns out to be surprisingly hard to guarantee security in this model when implementing cryptography in common languages such as C/C++ or Rust. We revisit the issues surrounding zeroization and then present a principled solution in the sense that it guarantees that sensitive data is erased and it clearly defines when this happens. We implement our solution as extension to the formally verified Jasmin compiler and extend the correctness proof of the compiler to cover zeroization. We show that the approach seamlessly integrates with state-of-the-art protections against microarchitectural attacks by integrating zeroization into Libjade, a cryptographic library written in Jasmin with systematic protections against timing and Spectre-v1 attacks. We present benchmarks showing that in many cases the overhead of zeroization is barely measurable and that it stays below 2% except for highly optimized symmetric crypto routines on short inputs.

In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.

Abstract The ongoing COVID-19 pandemic let to efforts to develop and deploy digital contact tracing systems to expedite contact tracing and risk notification. Unfortunately, the success of these systems has been limited, partly owing to poor interoperability with manual contact tracing, low adoption rates, and a societally sensitive trade-off between utility and privacy. In this work, we introduce a new privacy-preserving and inclusive system for epidemic risk assessment and notification that aims to address these limitations. Rather than capturing pairwise encounters between user devices as done by existing systems, our system captures encounters between user devices and beacons placed in strategic locations where infection clusters may originate. Epidemiological simulations using an agent-based model demonstrate that, by utilizing location and environmental information and interoperating with manual contact tracing, our system can increase the accuracy of contact tracing actions and may help reduce epidemic spread already at low adoption.

We propose a new approach for building efficient, provably secure, and practically hardened implementations of masked algorithms. Our approach is based on a Domain Specific Language in which users can write efficient assembly implementations and fine-grained leakage models. The latter are then used as a basis for formal verification, allowing for the first time formal guarantees for a broad range of device-specific leakage effects not addressed by prior work. The practical benefits of our approach are demonstrated through a case study of the PRESENT S-Box: we develop a highly optimized and provably secure masked implementation, and show through practical evaluation based on TVLA that our implementation is practically resilient. Our approach significantly narrows the gap between formal verification of masking and practical security.

Differential privacy provides a robust quantifiable methodology to measure and control the privacy leakage of data analysis algorithms. A fundamental insight is that by forcing algorithms to be randomized, their privacy leakage can be characterized by measuring the dissimilarity between output distributions produced by applying the algorithm to pairs datasets differing in one individual. After the introduction of differential privacy, several variants of the original definition have been proposed by changing the measure of dissimilarity between distributions, including concentrated, zero-concentrated and R{\'e}nyi differential privacy. The first contribution of this paper is to introduce the notion of privacy profile of a mechanism. This profile captures all valid $(\varepsilon,\delta)$ differential privacy parameters satisfied by a given mechanism, and contrasts with the usual approach of providing guarantees in terms of a single point in this curve. We show that knowledge of this curve is equivalent to knowledge of the privacy guarantees with respect to the alternative definitions listed above. This sheds further light into the connections between different privacy definitions, and suggests that these should be considered alternative but otherwise equivalent points of view. The second contribution of this paper is to apply the privacy profiles machinery to study the so-called ``privacy amplification by subsampling'' principle, which ensures that a differentially private mechanism run on a random subsample of a population provides higher privacy guarantees than when run on the entire population. Several instances of this principle have been studied for different random subsampling methods, each with an ad-hoc analysis. In this paper we set out to study this phenomenon in detail with the aim to provide a general method capable of recovering prior analyses in a streamlined fashion. Our method makes extensive use of coupling argument, and introduces a new tool to analyse differential privacy for mixture distributions.

Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential privacy. This construction can be defined in two styles. Earlier definitions require the existence of one or more witness distributions, while a recent definition by Sato uses universal quantification over all sets of samples. These notions have each have their own strengths: the universal version is more general than the existential ones, while existential liftings are known to satisfy more precise composition principles. We propose a novel, existential version of approximate lifting, called $\star$-lifting, and show that it is equivalent to Sato's construction for discrete probability measures. Our work unifies all known notions of approximate lifting, yielding cleaner properties, more general constructions, and more precise composition theorems for both styles of lifting, enabling richer proofs of differential privacy. We also clarify the relation between existing definitions of approximate lifting, and consider more general approximate liftings based on $f$-divergences.

The Theory and Practice of Differential Privacy workshop (TPDP 2016) was held in New York City, NY, USA on 23 June 2016 as part of ICML 2016. This is the program.