diff --git a/proofs/cbmc/mld_h/mld_h_harness.c b/proofs/cbmc/H/H_harness.c similarity index 100% rename from proofs/cbmc/mld_h/mld_h_harness.c rename to proofs/cbmc/H/H_harness.c diff --git a/proofs/cbmc/mld_h/Makefile b/proofs/cbmc/H/Makefile similarity index 96% rename from proofs/cbmc/mld_h/Makefile rename to proofs/cbmc/H/Makefile index 13c39c2e..d3ceb6c0 100644 --- a/proofs/cbmc/mld_h/Makefile +++ b/proofs/cbmc/H/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_h_harness +HARNESS_FILE = H_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. @@ -18,7 +18,6 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/sign.c -USE_FUNCTION_CONTRACTS+=mld_zeroize CHECK_FUNCTION_CONTRACTS=mld_H USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_init $(FIPS202_NAMESPACE)shake256_absorb $(FIPS202_NAMESPACE)shake256_squeeze $(FIPS202_NAMESPACE)shake256_finalize diff --git a/proofs/cbmc/mld_attempt_signature_generation/Makefile b/proofs/cbmc/attempt_signature_generation/Makefile similarity index 98% rename from proofs/cbmc/mld_attempt_signature_generation/Makefile rename to proofs/cbmc/attempt_signature_generation/Makefile index dbc4fc51..683cae1b 100644 --- a/proofs/cbmc/mld_attempt_signature_generation/Makefile +++ b/proofs/cbmc/attempt_signature_generation/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_attempt_signature_generation_harness +HARNESS_FILE = attempt_signature_generation_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_attempt_signature_generation/mld_attempt_signature_generation_harness.c b/proofs/cbmc/attempt_signature_generation/attempt_signature_generation_harness.c similarity index 100% rename from proofs/cbmc/mld_attempt_signature_generation/mld_attempt_signature_generation_harness.c rename to proofs/cbmc/attempt_signature_generation/attempt_signature_generation_harness.c diff --git a/proofs/cbmc/mld_ct_abs_i32/Makefile b/proofs/cbmc/ct_abs_i32/Makefile similarity index 98% rename from proofs/cbmc/mld_ct_abs_i32/Makefile rename to proofs/cbmc/ct_abs_i32/Makefile index 59eb306e..9bfc92b4 100644 --- a/proofs/cbmc/mld_ct_abs_i32/Makefile +++ b/proofs/cbmc/ct_abs_i32/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_ct_abs_i32_harness +HARNESS_FILE = ct_abs_i32_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_ct_abs_i32/mld_ct_abs_i32_harness.c b/proofs/cbmc/ct_abs_i32/ct_abs_i32_harness.c similarity index 100% rename from proofs/cbmc/mld_ct_abs_i32/mld_ct_abs_i32_harness.c rename to proofs/cbmc/ct_abs_i32/ct_abs_i32_harness.c diff --git a/proofs/cbmc/mld_ct_cmask_neg_i32/Makefile b/proofs/cbmc/ct_cmask_neg_i32/Makefile similarity index 97% rename from proofs/cbmc/mld_ct_cmask_neg_i32/Makefile rename to proofs/cbmc/ct_cmask_neg_i32/Makefile index 06a75036..07819a22 100644 --- a/proofs/cbmc/mld_ct_cmask_neg_i32/Makefile +++ b/proofs/cbmc/ct_cmask_neg_i32/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_ct_cmask_neg_i32_harness +HARNESS_FILE = ct_cmask_neg_i32_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_ct_cmask_neg_i32/mld_ct_cmask_neg_i32_harness.c b/proofs/cbmc/ct_cmask_neg_i32/ct_cmask_neg_i32_harness.c similarity index 100% rename from proofs/cbmc/mld_ct_cmask_neg_i32/mld_ct_cmask_neg_i32_harness.c rename to proofs/cbmc/ct_cmask_neg_i32/ct_cmask_neg_i32_harness.c diff --git a/proofs/cbmc/mld_ct_get_optblocker_i64/Makefile b/proofs/cbmc/ct_get_optblocker_i64/Makefile similarity index 97% rename from proofs/cbmc/mld_ct_get_optblocker_i64/Makefile rename to proofs/cbmc/ct_get_optblocker_i64/Makefile index e6e80467..21560ac8 100644 --- a/proofs/cbmc/mld_ct_get_optblocker_i64/Makefile +++ b/proofs/cbmc/ct_get_optblocker_i64/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_ct_get_optblocker_i64_harness +HARNESS_FILE = ct_get_optblocker_i64_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_ct_get_optblocker_i64/mld_ct_get_optblocker_i64_harness.c b/proofs/cbmc/ct_get_optblocker_i64/ct_get_optblocker_i64_harness.c similarity index 100% rename from proofs/cbmc/mld_ct_get_optblocker_i64/mld_ct_get_optblocker_i64_harness.c rename to proofs/cbmc/ct_get_optblocker_i64/ct_get_optblocker_i64_harness.c diff --git a/proofs/cbmc/mld_ct_get_optblocker_u32/Makefile b/proofs/cbmc/ct_get_optblocker_u32/Makefile similarity index 97% rename from proofs/cbmc/mld_ct_get_optblocker_u32/Makefile rename to proofs/cbmc/ct_get_optblocker_u32/Makefile index c7e42aae..612793ba 100644 --- a/proofs/cbmc/mld_ct_get_optblocker_u32/Makefile +++ b/proofs/cbmc/ct_get_optblocker_u32/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_ct_get_optblocker_u32_harness +HARNESS_FILE = ct_get_optblocker_u32_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_ct_get_optblocker_u32/mld_ct_get_optblocker_u32_harness.c b/proofs/cbmc/ct_get_optblocker_u32/ct_get_optblocker_u32_harness.c similarity index 100% rename from proofs/cbmc/mld_ct_get_optblocker_u32/mld_ct_get_optblocker_u32_harness.c rename to proofs/cbmc/ct_get_optblocker_u32/ct_get_optblocker_u32_harness.c diff --git a/proofs/cbmc/mld_ct_sel_int32/Makefile b/proofs/cbmc/ct_sel_int32/Makefile similarity index 98% rename from proofs/cbmc/mld_ct_sel_int32/Makefile rename to proofs/cbmc/ct_sel_int32/Makefile index 61980cf9..bb23b4d0 100644 --- a/proofs/cbmc/mld_ct_sel_int32/Makefile +++ b/proofs/cbmc/ct_sel_int32/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_ct_sel_int32_harness +HARNESS_FILE = ct_sel_int32_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_ct_sel_int32/mld_ct_sel_int32_harness.c b/proofs/cbmc/ct_sel_int32/ct_sel_int32_harness.c similarity index 100% rename from proofs/cbmc/mld_ct_sel_int32/mld_ct_sel_int32_harness.c rename to proofs/cbmc/ct_sel_int32/ct_sel_int32_harness.c diff --git a/proofs/cbmc/mld_sample_s1_s2/Makefile b/proofs/cbmc/sample_s1_s2/Makefile similarity index 98% rename from proofs/cbmc/mld_sample_s1_s2/Makefile rename to proofs/cbmc/sample_s1_s2/Makefile index b14fc153..2f088f24 100644 --- a/proofs/cbmc/mld_sample_s1_s2/Makefile +++ b/proofs/cbmc/sample_s1_s2/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_sample_s1_s2_harness +HARNESS_FILE = sample_s1_s2_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_sample_s1_s2/mld_sample_s1_s2_harness.c b/proofs/cbmc/sample_s1_s2/sample_s1_s2_harness.c similarity index 100% rename from proofs/cbmc/mld_sample_s1_s2/mld_sample_s1_s2_harness.c rename to proofs/cbmc/sample_s1_s2/sample_s1_s2_harness.c diff --git a/proofs/cbmc/mld_value_barrier_i64/Makefile b/proofs/cbmc/value_barrier_i64/Makefile similarity index 97% rename from proofs/cbmc/mld_value_barrier_i64/Makefile rename to proofs/cbmc/value_barrier_i64/Makefile index 0fe8a561..578ad558 100644 --- a/proofs/cbmc/mld_value_barrier_i64/Makefile +++ b/proofs/cbmc/value_barrier_i64/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_value_barrier_i64_harness +HARNESS_FILE = value_barrier_i64_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_value_barrier_i64/mld_value_barrier_i64_harness.c b/proofs/cbmc/value_barrier_i64/value_barrier_i64_harness.c similarity index 100% rename from proofs/cbmc/mld_value_barrier_i64/mld_value_barrier_i64_harness.c rename to proofs/cbmc/value_barrier_i64/value_barrier_i64_harness.c diff --git a/proofs/cbmc/mld_value_barrier_u32/Makefile b/proofs/cbmc/value_barrier_u32/Makefile similarity index 97% rename from proofs/cbmc/mld_value_barrier_u32/Makefile rename to proofs/cbmc/value_barrier_u32/Makefile index 455cf032..3a0b33d7 100644 --- a/proofs/cbmc/mld_value_barrier_u32/Makefile +++ b/proofs/cbmc/value_barrier_u32/Makefile @@ -4,7 +4,7 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = mld_value_barrier_u32_harness +HARNESS_FILE = value_barrier_u32_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. diff --git a/proofs/cbmc/mld_value_barrier_u32/mld_value_barrier_u32_harness.c b/proofs/cbmc/value_barrier_u32/value_barrier_u32_harness.c similarity index 100% rename from proofs/cbmc/mld_value_barrier_u32/mld_value_barrier_u32_harness.c rename to proofs/cbmc/value_barrier_u32/value_barrier_u32_harness.c diff --git a/scripts/check-contracts b/scripts/check-contracts new file mode 100755 index 00000000..610458b1 --- /dev/null +++ b/scripts/check-contracts @@ -0,0 +1,91 @@ +#!/usr/bin/env python3 +# Copyright (c) The mlkem-native project authors +# Copyright (c) The mldsa-native project authors +# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +# +# Looks for CBMC contracts without proof +# + +import re +import sys +import subprocess +import pathlib + +def get_c_source_files(): + return get_files("mldsa/**/*.c") + +def get_header_files(): + return get_files("mldsa/**/*.h") + +def get_files(pattern): + return list(map(str, pathlib.Path().glob(pattern))) + +def gen_proofs(): + cmd_str = ["./proofs/cbmc/list_proofs.sh"] + p = subprocess.run(cmd_str, capture_output=True, universal_newlines=False) + proofs = filter(lambda s: s.strip() != "", p.stdout.decode().split("\n")) + return proofs + +def gen_contracts(): + files = get_c_source_files() + get_header_files() + + for filename in files: + with open(filename, "r") as f: + content = f.read() + + contract_pattern = r'(\w+)\s*\([^)]*\)\s*\n?\s*__contract__' + matches = re.finditer(contract_pattern, content) + for m in matches: + line = content.count('\n', 0, m.start()) + yield (filename, line, m.group(1).removeprefix("mld_")) + +def is_exception(funcname): + # The functions passing this filter are known not to have a proof + + if funcname.endswith("_native") or funcname.endswith("_asm"): + # CBMC proofs are axiomatized against contracts of the backends + return True + + if funcname == "ct_get_optblocker_u64": + # As documented in the code, this contract is treated as an axiom + return True + + if funcname in ["memcmp", "randombytes"]: + # External functions + return True + + if funcname in ["zeroize"]: + # Implemented using inline ASM or external functions + return True + + return False + +def check_contracts(): + contracts = set(gen_contracts()) + proofs = set(gen_proofs()) + + bad = [] + + # Print contracts without proofs + for (filename, line, funcname) in contracts: + if funcname in proofs: + continue + + if is_exception(funcname): + print(f"{filename}:{line}:{funcname} has contract but no proof, " + "but is listed as exception") + continue + + print(f"{filename}:{line}:{funcname}: has contract but no proof. FAIL", + file=sys.stderr) + bad.append(funcname) + + return len(bad) == 0 + +def _main(): + if check_contracts() != True: + sys.exit(1) + +if __name__ == "__main__": + _main() diff --git a/scripts/lint b/scripts/lint index df66d648..30518f6c 100755 --- a/scripts/lint +++ b/scripts/lint @@ -209,3 +209,23 @@ gh_group_end if ! $SUCCESS; then exit 1 fi + +check-contracts() +{ + if python3 $ROOT/scripts/check-contracts >/dev/null; then + info "Check contracts" + gh_summary_success "Check contracts" + else + error "Check contracts" + gh_summary_failure "Check contracts" + SUCCESS=false + fi +} + +gh_group_start "Check contracts" +check-contracts +gh_group_end + +if ! $SUCCESS; then + exit 1 +fi