Skip to content

Commit 75ae090

Browse files
jakemasjakemas
committed
Hol-Light: Add Hol-light proof framework and Forward NTT proof
Add HOL-Light framework with NTT proof. This includes: - list_proofs.sh, build-proof.sh, dump_bytecode.ml utilities - mldsa-specs.ml and mldsa-utils.ml to support HOL-Light proofs - HOL-Light proof for ML-DSA x86 AVX2 NTT in mldsa_ntt.ml - Addition of hol_light to scripts/tests to wrap and run proofs - READMEs for usage descriptions - Autogenerate embedded bytecode using dump_bytecode.ml - Add CI jobs to test and run hol-light proofs - Add autogen for asmb files Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent 288bfa8 commit 75ae090

File tree

21 files changed

+8463
-8
lines changed

21 files changed

+8463
-8
lines changed

‎.github/workflows/hol_light.yml‎

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
2+
3+
name: HOL-Light
4+
permissions:
5+
contents: read
6+
on:
7+
push:
8+
branches: ["main"]
9+
paths:
10+
- '.github/workflows/hol_light.yml'
11+
- 'proofs/hol_light/x86_64/Makefile'
12+
- 'proofs/hol_light/x86_64/**/*.S'
13+
- 'proofs/hol_light/x86_64/**/*.ml'
14+
- 'flake.nix'
15+
- 'flake.lock'
16+
- 'nix/hol_light/*'
17+
- 'nix/s2n_bignum/*'
18+
pull_request:
19+
branches: ["main"]
20+
paths:
21+
- '.github/workflows/hol_light.yml'
22+
- 'proofs/hol_light/x86_64/Makefile'
23+
- 'proofs/hol_light/x86_64/**/*.S'
24+
- 'proofs/hol_light/x86_64/**/*.ml'
25+
- 'flake.nix'
26+
- 'flake.lock'
27+
- 'nix/hol_light/*'
28+
- 'nix/s2n_bignum/*'
29+
30+
concurrency:
31+
group: ${{ github.workflow }}-${{ github.ref }}
32+
cancel-in-progress: true
33+
34+
jobs:
35+
# The proofs also check that the byte code is up to date,
36+
# but we use this as a fast path to not even start the proofs
37+
# if the byte code needs updating.
38+
hol_light_bytecode:
39+
name: HOL-Light bytecode check
40+
runs-on: pqcp-x64
41+
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
42+
steps:
43+
- uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
44+
with:
45+
fetch-depth: 0
46+
- uses: ./.github/actions/setup-shell
47+
with:
48+
gh_token: ${{ secrets.GITHUB_TOKEN }}
49+
nix-shell: 'hol_light'
50+
script: |
51+
autogen --update-hol-light-bytecode --dry-run
52+
hol_light_interactive:
53+
name: HOL-Light interactive shell test
54+
runs-on: pqcp-x64
55+
needs: [ hol_light_bytecode ]
56+
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
57+
steps:
58+
- uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
59+
with:
60+
fetch-depth: 0
61+
- uses: ./.github/actions/setup-shell
62+
with:
63+
gh_token: ${{ secrets.GITHUB_TOKEN }}
64+
nix-shell: 'hol_light'
65+
script: |
66+
# Load base infrastructure and specs to validate HOL-Light environment
67+
# When we have smaller/faster proofs, we can run them here instead:
68+
# make -C proofs/hol_light/x86_64 mldsa/mldsa_ntt.o
69+
# echo 'needs "proofs/mldsa_ntt.ml";;' | hol.sh
70+
echo 'needs "x86/proofs/base.ml";; needs "proofs/mldsa_specs.ml";; #quit;;' | hol.sh
71+
hol_light_proofs:
72+
needs: [ hol_light_bytecode ]
73+
strategy:
74+
fail-fast: false
75+
matrix:
76+
proof:
77+
# Dependencies on {name}.{S,ml} are implicit
78+
- name: mldsa_ntt
79+
needs: ["mldsa_specs.ml", "mldsa_utils.ml"]
80+
name: HOL Light proof for ${{ matrix.proof.name }}.S
81+
runs-on: pqcp-x64
82+
if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork
83+
steps:
84+
- uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0
85+
with:
86+
fetch-depth: 0
87+
- name: Get changed files
88+
id: changed-files
89+
uses: tj-actions/changed-files@24d32ffd492484c1d75e0c0b894501ddb9d30d62 # v47.0.0
90+
- name: Check if dependencies changed
91+
id: check_run
92+
shell: bash
93+
run: |
94+
run_needed=0
95+
changed_files="${{ steps.changed-files.outputs.all_changed_files }}"
96+
dependencies="${{ join(matrix.proof.needs, ' ') }} ${{ format('{0}.S {0}.ml', matrix.proof.name) }}"
97+
for changed in $changed_files; do
98+
for needs in $dependencies; do
99+
if [[ "$changed" == *"$needs" ]]; then
100+
run_needed=1
101+
fi
102+
done
103+
done
104+
105+
# Always re-run upon change to nix files for HOL-Light
106+
if [[ "$changed_files" == *"nix/"* ]] || [[ "$changed_files" == *"hol_light.yml"* ]] || [[ "$changed_files" == *"flake"* ]] || [[ "$changed_files" == *"proofs/hol_light/x86_64/Makefile"* ]]; then
107+
run_needed=1
108+
fi
109+
110+
echo "run_needed=${run_needed}" >> $GITHUB_OUTPUT
111+
- uses: ./.github/actions/setup-shell
112+
if: |
113+
steps.check_run.outputs.run_needed == '1'
114+
with:
115+
gh_token: ${{ secrets.GITHUB_TOKEN }}
116+
nix-shell: 'hol_light'
117+
script: |
118+
tests hol_light -p ${{ matrix.proof.name }} --verbose

‎BIBLIOGRAPHY.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -228,6 +228,7 @@ source code and documentation.
228228
- [mldsa/src/native/x86_64/src/rej_uniform_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_avx2.c)
229229
- [mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta2_avx2.c)
230230
- [mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c](mldsa/src/native/x86_64/src/rej_uniform_eta4_avx2.c)
231+
- [proofs/hol_light/x86_64/mldsa/mldsa_ntt.S](proofs/hol_light/x86_64/mldsa/mldsa_ntt.S)
231232

232233
### `Round3_Spec`
233234

‎README.md‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,13 @@ make test
4343

4444
We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to prove absence of various classes of undefined behaviour in C, including out of bounds memory accesses and integer overflows. The proofs cover all C code in [mldsa/src/*](mldsa) and [mldsa/src/fips202/*](mldsa/src/fips202) involved in running mldsa-native with its C backend. See [proofs/cbmc](proofs/cbmc) for details.
4545

46+
HOL-Light functional correctness proofs can be found in [proofs/hol_light/x86_64](proofs/hol_light/x86_64). So far, the following functions have been proven correct:
47+
48+
- x86_64 NTT [ntt.S](mldsa/src/native/x86_64/src/ntt.S)
49+
50+
51+
These proofs are utilizing the verification infrastructure in [s2n-bignum](https://github.com/awslabs/s2n-bignum).
52+
4653
## Security
4754

4855
All assembly in mldsa-native is constant-time in the sense that it is free of secret-dependent control flow, memory access,

‎dev/x86_64/src/ntt.S‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -267,6 +267,7 @@ vmovdqa %ymm11,256*\off+224(%rdi)
267267
.balign 4
268268
.global MLD_ASM_NAMESPACE(ntt_avx2)
269269
MLD_ASM_FN_SYMBOL(ntt_avx2)
270+
endbr64
270271
vmovdqa MLD_AVX2_BACKEND_DATA_OFFSET_8XQ*4(%rsi),%ymm0
271272

272273
levels0t1 0

‎flake.nix‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,8 +100,8 @@
100100
}).overrideAttrs (old: {
101101
shellHook = ''
102102
export PATH=$PWD/scripts:$PATH
103-
# Set PROOF_DIR_ARM based on where we entered the shell
104-
export PROOF_DIR_ARM="$PWD/proofs/hol_light/arm"
103+
# Set proof directory for x86_64
104+
export PROOF_DIR_X86_64="$PWD/proofs/hol_light/x86_64"
105105
'';
106106
});
107107
devShells.ci = util.mkShell {

‎mldsa/src/native/x86_64/src/ntt.S‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@
3434
MLD_ASM_FN_SYMBOL(ntt_avx2)
3535

3636
.cfi_startproc
37+
endbr64
3738
vmovdqa (%rsi), %ymm0
3839
vpbroadcastd 0x84(%rsi), %ymm1
3940
vpbroadcastd 0x524(%rsi), %ymm2

‎nix/hol_light/0005-Configure-hol-sh-for-mldsa-native.patch‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,10 @@ index 1311255..8b2bc36 100755
2121
+SITELIB=$(dirname $(ocamlfind query findlib 2>/dev/null) 2>/dev/null)
2222
+
2323
+# Set HOLLIGHT_LOAD_PATH to include S2N_BIGNUM_DIR and mldsa-native proofs
24-
+export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR_ARM}:${HOLLIGHT_LOAD_PATH}"
24+
+export HOLLIGHT_LOAD_PATH="${S2N_BIGNUM_DIR}:${PROOF_DIR_X86_64}:${HOLLIGHT_LOAD_PATH}"
2525
+
2626
+# Change to mldsa-native proofs directory if set, so define_from_elf can find object files
27-
+[ -n "${PROOF_DIR_ARM}" ] && cd "${PROOF_DIR_ARM}"
27+
+[ -n "${PROOF_DIR_X86_64}" ] && cd "${PROOF_DIR_X86_64}"
2828
+
2929
+${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOL_ML_PATH} -I ${HOLLIGHT_DIR} ${SITELIB:+-I "$SITELIB"}
3030
diff --git a/hol_4.sh b/hol_4.sh

‎nix/s2n_bignum/default.nix‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@
44
{ stdenv, fetchFromGitHub, writeText, ... }:
55
stdenv.mkDerivation rec {
66
pname = "s2n_bignum";
7-
version = "1fcccc89cc7762ae5c56ec660f25b5f1358ba308";
7+
version = "2ab2252b8505e58a7c3392f8ad823782032b61e7";
88
src = fetchFromGitHub {
9-
owner = "jargh";
10-
repo = "s2n-bignum-dev";
9+
owner = "awslabs";
10+
repo = "s2n-bignum";
1111
rev = "${version}";
12-
hash = "sha256-hSJ2WlrwVlTF3wSdMfdBbovBXMG5vltfPxp36hOMd5c=";
12+
hash = "sha256-7lil3jAFo5NiyNOSBYZcRjduXkotV3x4PlxXSKt63M8=";
1313
};
1414
setupHook = writeText "setup-hook.sh" ''
1515
export S2N_BIGNUM_DIR="$1"

‎proofs/README.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,7 @@ This directory contains material related to the formal verification of the sourc
77
## C verification: CBMC
88

99
We use the [C Bounded Model Checker (CBMC)](https://github.com/diffblue/cbmc) to show the absence of various classes of undefined behaviour in the mldsa-native C source, including out of bounds memory accesses and integer overflows. See [proofs/cbmc](cbmc), or the [proof_guide](https://github.com/pq-code-package/mlkem-native/blob/main/proofs/cbmc/proof_guide.md).
10+
11+
## Assembly verification: HOL-Light
12+
13+
We use the [HOL-Light](https://github.com/jrh13/hol-light) interactive theorem prover alongside the verification infrastructure from [s2n-bignum](https://github.com/awslabs/s2n-bignum) to show the functional correctness of highly optimized assembly routines in mlkem-native at the object-code level. See [proofs/hol_light/x86_64](hol_light/x86_64).

‎proofs/hol_light/.gitignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
2+
**/*.o
3+
**/*.native
4+
**/*.correct

0 commit comments

Comments
 (0)