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
 
 
riscv32
riscv32
 
 
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, x86_64, and RV32IM 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 under aarch64/proofs/, x86_64/proofs/, or riscv32/proofs/. Each proof entry contains the checked bytecode for its corresponding object file near the top.

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.

For RV32IM, the timing claim follows the s2n-bignum RISC-V model. In particular, MUL and MULH are modeled without operand-dependent timing events. The proof therefore applies to implementations where those instructions have fixed latency, or where any operand-dependent latency is otherwise excluded from the attacker model.

By design: rejection sampling for the public matrix (rej_uniform)

rej_uniform expands the public matrix A from the public seed rho. Because it operates on public data only, secret-independent timing is not a requirement, and admitting variable-time execution enables a faster implementation. We therefore prove properties 1 and 2 for it, but deliberately not property 3.

Constant-time rejection sampling for the secret vector (rej_uniform_eta{2,4})

The rej_uniform_eta{2,4} kernels (on both AArch64 and x86_64) sample the secret vectors s1/s2 by rejection, so their control flow and memory-access pattern depend on which candidates are accepted, and the standard one-line safety tactic asserting full obliviousness does not apply. Instead we prove secret-independence against a public reject pattern: the microarchitectural event trace is a function of the public pointers and the reject pattern — one accept/reject bit per candidate nibble — and of nothing else, in particular not of the accepted coefficient values. The XOF stream is secret, but the reject pattern is safe to leak, each acceptance decision being statistically independent of the accepted values (Section 5.5 of 1).

Concretely, the constant-time safety theorems for rej_uniform_eta2 and rej_uniform_eta4 state that some event-generating function f_events, depending only on public data, reproduces the entire trace (shown here for eta2; the eta4 statement is identical with REJ_MASK_ETA4 and val x < 9):

`?f_events.
   !res buf buflen table (inlist:byte list) pc e stackpointer returnaddress.
     (* same alignment / non-overlap preconditions as _MEMSAFE *)
     ...
     ==> ensures arm
          (\s. (* same precondition as _MEMSAFE: code at pc, C arguments
                  [res;buf;buflen;table], input bytes at buf, table at table,
                  event log = e *)
               ... /\ read events s = e)
          (\s. read PC s = returnaddress /\
               ?e2. read events s = APPEND e2 e /\
                    (* the events of this call are EXACTLY f_events applied to the
                       public arguments and the reject pattern -- and not the
                       accepted coefficient values *)
                    e2 = f_events res buf buflen table pc stackpointer
                                  returnaddress (REJ_MASK_ETA2 inlist) /\
                    memaccess_inbounds e2 (read set) (write set))
          (\s s'. T)`

where REJ_MASK_ETA2 l = MAP (\x. val x < 15) (NIBBLES_OF_BYTES l) is the reject pattern — one accept/reject bit per nibble, accepted values discarded. (Contrast REJ_NIBBLES_ETA2, which keeps the accepted values and is secret.) Because the whole trace factors through the reject pattern, two inputs with the same pattern are indistinguishable to a timing/cache adversary regardless of their coefficient values.

The x86_64 AVX2 kernels prove the identical property (with ensures x86). Because the x86_64 rej_uniform_eta{2,4} assembly processes a fixed-length input buffer (136 bytes for eta2, 272 for eta4) rather than taking a runtime buflen argument, its f_events and preconditions specialise buflen to that constant; the reject-pattern factoring is otherwise identical.

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

For RV32IM, use the shell containing the cross toolchain:

nix develop .#hol_light-cross-riscv32 \
  --experimental-features 'nix-command flakes'
make -C proofs/hol_light/riscv32

These commands 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. Pass -a riscv32 when cross-checking RV32IM proofs on another host; 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 the matrix sampler rej_uniform, which is proven correct and memory-safe, and is variable-time by design (see By design). rej_uniform_eta{2,4} are proven correct, memory-safe, and secret-independent in timing: their event trace is a function of the public pointers and the reject pattern only, never of the accepted coefficient values (see Constant-time rejection sampling).

AArch64

x86_64

RV32IM

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 ↩