Skip to content

hol_light

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History

hol_light

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
aarch64
aarch64
 
 
common
common
 
 
x86_64
x86_64
 
 
.gitignore
.gitignore
 
 
README.md
README.md
 
 
s2n_bignum_allowlist.txt
s2n_bignum_allowlist.txt
 
 

README.md

HOL Light proofs

This directory contains HOL Light proofs for the AArch64 and x86_64 assembly routines used in mldsa-native. The proofs are written in the HOL Light theorem prover, utilizing the assembly verification infrastructure from s2n-bignum.

Each function is proved in a separate .ml file in aarch64/proofs/ and x86_64/proofs/. Each file contains the byte code being verified, as well as the specification that is being proved.

What is proven

Unless documented otherwise, for each assembly routine listed below, we prove three properties:

  1. Functional correctness — the routine computes the specified mathematical function (e.g., that mldsa_ntt computes the ML-DSA forward NTT modulo q = 8380417).
  2. Memory safety — the routine accesses only those memory regions permitted by its specification (input/output buffers, stack frame).
  3. Secret-independent timing — the sequence of microarchitectural events (e.g. memory accesses, branch decisions) emitted by the routine is a function of public inputs only, and does not depend on secret data.

Known gap: rejection sampling for the secret vector (rej_uniform_eta{2,4})

The AArch64 and AVX2 kernels rej_uniform_eta{2,4} have secret-independent timing, but we do not yet prove it (see #1160): Their memory access pattern depends on which coefficients fall inside vs. outside the acceptance interval, but no other information about the secret coefficients is leaked. The indices of in bound vs. out of bounds coefficients are statistically independent of the secret key; see Section 5.5 of the Dilithium Round 3 specification1.

Primer

Proofs are 'post-hoc' in the sense that HOL-Light/s2n-bignum operate on the final object code. In particular, the means by which the code was generated need not be trusted.

Specifications are essentially Hoare triples, with the noteworthy difference that the program is implicit as the content of memory at the PC; which is asserted to be the code under verification as part of the precondition. For example, the following is the specification of the mldsa_ntt function:

 (* For all (abbreviated by `!` in HOL):
    - a: Polynomial coefficients pointer
    - zetas: NTT constants pointer
    - x: Original polynomial coefficients
    - pc: Current value of Program Counter (PC)
    - stackpointer: Stack pointer
    - returnaddress: Return address on the stack *)
`!a zetas x pc stackpointer returnaddress.
    (* Alignment and non-overlapping requirements *)
    aligned 32 a /\
    aligned 32 zetas /\
    nonoverlapping (word pc,LENGTH mldsa_ntt_mc) (a, 1024) /\
    nonoverlapping (word pc,LENGTH mldsa_ntt_mc) (zetas, 2496) /\
    nonoverlapping (a, 1024) (zetas, 2496) /\
    nonoverlapping (stackpointer,8) (a, 1024) /\
    nonoverlapping (stackpointer,8) (zetas, 2496)
    ==> ensures x86
      (* Precondition *)
      (\s. (* The memory at the current PC is the byte-code of mldsa_ntt() *)
        bytes_loaded s (word pc) mldsa_ntt_mc /\
        read RIP s = word pc /\
        read RSP s = stackpointer /\
        (* The return address is on the stack *)
        read (memory :> bytes64 stackpointer) s = returnaddress /\
        (* Arguments are passed via C calling convention *)
        C_ARGUMENTS [a; zetas] s /\
        (* NTT constants are properly loaded *)
        wordlist_from_memory(zetas,624) s = MAP (iword: int -> 32 word) mldsa_complete_qdata /\
        (* Input bounds checking *)
        (!i. i < 256 ==> abs(ival(x i)) <= &8380416) /\
        (* Give a name to the memory contents at the source pointer *)
        !i. i < 256
            ==> read(memory :> bytes32(word_add a (word(4 * i)))) s = x i)
      (* Postcondition: Eventually we reach a state where ... *)
      (\s.
        (* The PC is the return address *)
        read RIP s = returnaddress /\
        (* Stack pointer is adjusted *)
        read RSP s = word_add stackpointer (word 8) /\
        (* The integers represented by the final memory contents
         * are congruent to the ML-DSA forward NTT transformation
         * of the original coefficients, modulo 8380417, with proper bounds *)
        !i. i < 256
            ==> let zi = read(memory :> bytes32(word_add a (word(4 * i)))) s in
                (ival zi == mldsa_forward_ntt (ival o x) i) (mod &8380417) /\
                abs(ival zi) <= &42035261)
      (* Footprint: The program may modify (only) the ABI permitted registers
       * and flags, stack pointer, and the memory contents at the source pointer. *)
      (MAYCHANGE [RSP] ,, MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
       MAYCHANGE [memory :> bytes(a,1024)])`

Reproducing the proofs

To reproduce the proofs, enter the nix shell via

nix develop .#hol_light --experimental-features 'nix-command flakes'

from mldsa-native's base directory. Then

make -C proofs/hol_light/aarch64

or

make -C proofs/hol_light/x86_64

will build and run the proofs. Note that this may take hours even on powerful machines.

For convenience, you can also use tests hol_light which wraps the make invocation above; see tests hol_light --help.

Interactive proof development

For interactive proof development, start the HOL Light server:

hol-server [port]  # default port is 2012

Then use the HOL Light extension for VS Code to connect and send commands interactively.

Alternatively, send commands using netcat:

echo '1+1;;' | nc -w 5 127.0.0.1 2012

Routines covered

All routines listed below have been proven correct, memory-safe, and secret-independent in their timing, except for rej_uniform_eta{2,4} which are proven memory-safe only (see Known gap).

AArch64

x86_64

Footnotes

  1. Bai, Ducas, Kiltz, Lepoint, Lyubashevsky, Schwabe, Seiler, Stehlé: CRYSTALS-Dilithium Algorithm Specifications and Supporting Documentation (Version 3.1), https://pq-crystals.org/dilithium/data/dilithium-specification-round3-20210208.pdf ↩

  2. Becker, Kannwischer: Hybrid scalar/vector implementations of Keccak and SPHINCS+ on AArch64, https://eprint.iacr.org/2022/1243 ↩