High-assurance zeroization

Authors

  • Santiago Arranz Olmos MPI-SP, Bochum, Germany
  • Gilles Barthe MPI-SP, Bochum, Germany; IMDEA Software Institute, Madrid, Spain
  • Ruben Gonzalez MPI-SP, Bochum, Germany; Neodyme AG, Munich, Germany
  • Benjamin Grégoire Inria, Sophia-Antipolis, France
  • Vincent Laporte Inria, Nancy, France
  • Jean-Christophe Léchenet Inria, Sophia-Antipolis, France
  • Tiago Oliveira MPI-SP, Bochum, Germany
  • Peter Schwabe MPI-SP, Bochum, Germany; Radboud University, Nijmegen, The Netherlands

DOI:

https://doi.org/10.46586/tches.v2024.i1.375-397

Keywords:

Secret erasure, clear stack memory, defense in depth, high-assurance cryptography

Abstract

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.

Downloads

Published

2023-12-04

Issue

Section

Articles

How to Cite

High-assurance zeroization. (2023). IACR Transactions on Cryptographic Hardware and Embedded Systems, 2024(1), 375-397. https://doi.org/10.46586/tches.v2024.i1.375-397