Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Logical Relations for Formally Verified Authenticated Data Structures

Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti

TL;DR

The paper tackles the challenge of constructing formally verified authenticated data structures (ADS) by presenting Authentikit, a typed-module library that automatically generates ADS with cryptographic proofs. It introduces a relational separation-logic framework tailored to collision-resistant hash functions, and builds two semantic models to prove security and correctness; these models underpin proofs that optimizations, and hand-written, optimized implementations can be soundly linked to automatically generated code. All results are machine-checked in Coq using the Iris framework, including proofs of four optimizations and the integration of prover, verifier, and ideal semantics. The work advances ADS verification beyond λAuth by providing a complete, modular, type-system-based security and correctness theory, addressing compiler Frontend burdens, optimization coverage, and performance gaps with hand-written implementations. The significance lies in enabling robust, composable ADS development with formal guarantees and practical pathways to optimized, mixed-code deployments.

Abstract

Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are challenging to develop and implement correctly. This paper gives a formal proof of security and correctness for a library that generates authenticated versions of data structures automatically. The proof is based on a new relational separation logic for reasoning about programs that use collision-resistant cryptographic hash functions. This logic provides a basis for constructing two semantic models of a type system, which are used to justify how the library makes use of type abstraction to enforce security and correctness. Using these models, we also prove the correctness of several optimizations to the library and then show how optimized, hand-written implementations of authenticated data structures can be soundly linked with automatically generated code. All of the results in this paper have been mechanized in the Coq proof assistant using the Iris framework.

Logical Relations for Formally Verified Authenticated Data Structures

TL;DR

The paper tackles the challenge of constructing formally verified authenticated data structures (ADS) by presenting Authentikit, a typed-module library that automatically generates ADS with cryptographic proofs. It introduces a relational separation-logic framework tailored to collision-resistant hash functions, and builds two semantic models to prove security and correctness; these models underpin proofs that optimizations, and hand-written, optimized implementations can be soundly linked to automatically generated code. All results are machine-checked in Coq using the Iris framework, including proofs of four optimizations and the integration of prover, verifier, and ideal semantics. The work advances ADS verification beyond λAuth by providing a complete, modular, type-system-based security and correctness theory, addressing compiler Frontend burdens, optimization coverage, and performance gaps with hand-written implementations. The significance lies in enabling robust, composable ADS development with formal guarantees and practical pathways to optimized, mixed-code deployments.

Abstract

Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are challenging to develop and implement correctly. This paper gives a formal proof of security and correctness for a library that generates authenticated versions of data structures automatically. The proof is based on a new relational separation logic for reasoning about programs that use collision-resistant cryptographic hash functions. This logic provides a basis for constructing two semantic models of a type system, which are used to justify how the library makes use of type abstraction to enforce security and correctness. Using these models, we also prove the correctness of several optimizations to the library and then show how optimized, hand-written implementations of authenticated data structures can be soundly linked with automatically generated code. All of the results in this paper have been mechanized in the Coq proof assistant using the Iris framework.
Paper Structure (30 sections, 8 theorems, 35 equations, 13 figures)

This paper contains 30 sections, 8 theorems, 35 equations, 13 figures.

Table of Contents

  1. Introduction
  2. Background
  3. Authentikit
  4. Merkle Trees
  5. Prover Implementation
  6. Verifier Implementation
  7. Ideal Implementation
  8. Security and Correctness
  9. The Language
  10. Collision-Free Reasoning in Separation Logic
  11. Relational Collision-Free Reasoning
  12. Security
  13. Logical Relation for Security
  14. Security of Authentikit
  15. Correctness
  16. ...and 15 more sections

Key Result

theorem 1

Let $\varphi$ be a first-order predicate. If is derivable then $\cfsafe(\expr)$ and for all $i \in \HashFamilyIndex$, if $\langle\expr,(\emptyset, \emptyset, i)\rangle \cfsteps \langle\val, \pstate\rangle$ then $\varphi(\val)$ holds at the meta level.

Figures (13)

  • Figure 1: Authentikit type signatures.
  • Figure 2: Merkle trees implemented using Authentikit.
  • Figure 3: Three realizations of the Authentikit interface in OCaml..
  • Figure 4: The prover view of a Merkle tree where $h_{i}$ is the hash of $t_{i}$. The hash of a node is uniquely determined by the hashes of its children, , $h_{2}$ is derived from $h_{5}$ and $h_{6}$.
  • Figure 5: Excerpt of the grammar of syntax and types for $\thelang$.
  • ...and 8 more figures

Theorems & Definitions (8)

  • theorem 1: Soundness
  • corollary 1: Relational Soundness
  • theorem 2: Security
  • theorem 3
  • lemma 1: Security, semantic
  • theorem 4: Correctness
  • theorem 5
  • lemma 2: Correctness, semantic