diff --git a/cbmc/proofs/mlkem_shake256_prf/Makefile b/cbmc/proofs/mlkem_shake256_prf/Makefile new file mode 100644 index 000000000..01062efcb --- /dev/null +++ b/cbmc/proofs/mlkem_shake256_prf/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = mlkem_shake256_prf_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. +PROOF_UID = mlkem_shake256_prf + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/symmetric-shake.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)mlkem_shake256_prf +USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = $(MLKEM_NAMESPACE)mlkem_shake256_prf + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/mlkem_shake256_prf/cbmc-proof.txt b/cbmc/proofs/mlkem_shake256_prf/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/mlkem_shake256_prf/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/mlkem_shake256_prf/mlkem_shake256_prf_harness.c b/cbmc/proofs/mlkem_shake256_prf/mlkem_shake256_prf_harness.c new file mode 100644 index 000000000..05295b0c8 --- /dev/null +++ b/cbmc/proofs/mlkem_shake256_prf/mlkem_shake256_prf_harness.c @@ -0,0 +1,29 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include +#include "symmetric.h" + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) +{ + uint8_t *out; + size_t outlen; + uint8_t *key; + uint8_t nonce; + mlkem_shake256_prf(out, outlen, key, nonce); +} diff --git a/cbmc/proofs/mlkem_shake256_rkprf/Makefile b/cbmc/proofs/mlkem_shake256_rkprf/Makefile new file mode 100644 index 000000000..d4e2a2d0e --- /dev/null +++ b/cbmc/proofs/mlkem_shake256_rkprf/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = mlkem_shake256_rkprf_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. +PROOF_UID = mlkem_shake256_rkprf + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/symmetric-shake.c $(SRCDIR)/fips202/fips202.c + +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)mlkem_shake256_rkprf +USE_FUNCTION_CONTRACTS=$(FIPS202_NAMESPACE)shake256_inc_absorb $(FIPS202_NAMESPACE)shake256_inc_finalize $(FIPS202_NAMESPACE)shake256_inc_squeeze $(FIPS202_NAMESPACE)shake256_inc_init +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--bitwuzla + +FUNCTION_NAME = $(MLKEM_NAMESPACE)mlkem_shake256_rkprf + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +# This function is large enough to need... +CBMC_OBJECT_BITS = 8 + +# If you require access to a file-local ("static") function or object to conduct +# your proof, set the following (and do not include the original source file +# ("mlkem/poly.c") in PROJECT_SOURCES). +# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i +# include ../Makefile.common +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mlkem/poly.c +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar +# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz +# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must +# be set before including Makefile.common, but any use of variables on the +# left-hand side requires those variables to be defined. Hence, _SOURCE, +# _FUNCTIONS, _OBJECTS is set after including Makefile.common. + +include ../Makefile.common diff --git a/cbmc/proofs/mlkem_shake256_rkprf/cbmc-proof.txt b/cbmc/proofs/mlkem_shake256_rkprf/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/mlkem_shake256_rkprf/cbmc-proof.txt @@ -0,0 +1,3 @@ +# SPDX-License-Identifier: Apache-2.0 + +# This file marks this directory as containing a CBMC proof. diff --git a/cbmc/proofs/mlkem_shake256_rkprf/mlkem_shake256_rkprf_harness.c b/cbmc/proofs/mlkem_shake256_rkprf/mlkem_shake256_rkprf_harness.c new file mode 100644 index 000000000..1244a420f --- /dev/null +++ b/cbmc/proofs/mlkem_shake256_rkprf/mlkem_shake256_rkprf_harness.c @@ -0,0 +1,28 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 + +/* + * Insert copyright notice + */ + + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include +#include "symmetric.h" + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) +{ + uint8_t *out; + uint8_t *key; + uint8_t *input; + mlkem_shake256_rkprf(out, key, input); +} diff --git a/fips202/fips202.h b/fips202/fips202.h index 68c71c26f..69c0210df 100644 --- a/fips202/fips202.h +++ b/fips202/fips202.h @@ -61,21 +61,43 @@ void shake128_ctx_release(shake128ctx *state); /* Initialize incremental hashing API */ #define shake256_inc_init FIPS202_NAMESPACE(shake256_inc_init) -void shake256_inc_init(shake256incctx *state); +void shake256_inc_init(shake256incctx *state) +__contract__( + requires(memory_no_alias(state, sizeof(shake256incctx))) + assigns(memory_slice(state, sizeof(shake256incctx))) +); + + #define shake256_inc_absorb FIPS202_NAMESPACE(shake256_inc_absorb) void shake256_inc_absorb(shake256incctx *state, const uint8_t *input, - size_t inlen); + size_t inlen) +__contract__( + requires(memory_no_alias(state, sizeof(shake256incctx))) + requires(memory_no_alias(input, inlen)) + assigns(memory_slice(state, sizeof(shake256incctx))) +); + + /* Prepares for squeeze phase */ #define shake256_inc_finalize FIPS202_NAMESPACE(shake256_inc_finalize) -void shake256_inc_finalize(shake256incctx *state); +void shake256_inc_finalize(shake256incctx *state) +__contract__( + requires(memory_no_alias(state, sizeof(shake256incctx))) + assigns(memory_slice(state, sizeof(shake256incctx))) +); /* Squeeze output out of the sponge. * * Supports being called multiple times */ #define shake256_inc_squeeze FIPS202_NAMESPACE(shake256_inc_squeeze) -void shake256_inc_squeeze(uint8_t *output, size_t outlen, - shake256incctx *state); +void shake256_inc_squeeze(uint8_t *output, size_t outlen, shake256incctx *state) +__contract__( + requires(memory_no_alias(state, sizeof(shake256incctx))) + requires(memory_no_alias(output, outlen)) + assigns(memory_slice(output, outlen)) + assigns(memory_slice(state, sizeof(shake256incctx))) +); /* Free the state */ #define shake256_inc_ctx_release FIPS202_NAMESPACE(shake256_inc_ctx_release) diff --git a/fips202/fips202x4.h b/fips202/fips202x4.h index e7bddacc5..59cb6aeb8 100644 --- a/fips202/fips202x4.h +++ b/fips202/fips202x4.h @@ -16,8 +16,15 @@ #define shake128x4_absorb FIPS202_NAMESPACE(shake128x4_absorb) void shake128x4_absorb(keccakx4_state *state, const uint8_t *in0, const uint8_t *in1, const uint8_t *in2, - const uint8_t *in3, size_t inlen); - + const uint8_t *in3, size_t inlen) +__contract__( + requires(memory_no_alias(state, sizeof(keccakx4_state))) + requires(memory_no_alias(in0, inlen)) + requires(memory_no_alias(in1, inlen)) + requires(memory_no_alias(in2, inlen)) + requires(memory_no_alias(in3, inlen)) + assigns(object_whole(state)) +); #define shake256x4_absorb FIPS202_NAMESPACE(shake256x4_absorb) void shake256x4_absorb(keccakx4_state *state, const uint8_t *in0,