diff --git a/.clang-format b/.clang-format index 7e80c9ac5..267b80165 100644 --- a/.clang-format +++ b/.clang-format @@ -18,5 +18,6 @@ IncludeBlocks: Preserve BreakBeforeBraces: Allman WhitespaceSensitiveMacros: ['__contract__', '__loop__' ] Macros: - - __contract__(x)={} void foo() + # Make this artifically long to avoid function bodies after short contracts + - __contract__(x)={ void a; void b; void c; void d; void e; void f; } void abcdefghijklmnopqrstuvw() - __loop__(x)={} diff --git a/README.md b/README.md index 0c73cd09d..6ab78e8e1 100644 --- a/README.md +++ b/README.md @@ -27,13 +27,6 @@ functionally verified. are imported into a consuming project's source tree and built using that project's build system. The build system provided in this repository is for experimental and development purposes only. -#### Secure Compilation - -**mlkem-native** includes functions that are susceptible to compiler-induced variable-time code when inlined into -their call-sites. Those functions are contained in [`mlkem/verify.c`](mlkem/verify.c). To ensure secure compilation, you -MUST NOT enable link time optimization (LTO) for `mlkem/verify.c`. To the best of our knowledge, it is safe to compile -the rest of the source tree with LTO. - ### Current state **mlkem-native** is work in progress. **WE DO NOT CURRENTLY RECOMMEND RELYING ON THIS LIBRARY IN A PRODUCTION diff --git a/cbmc/proofs/crypto_kem_dec/Makefile b/cbmc/proofs/crypto_kem_dec/Makefile index ccd705c30..f883ca965 100644 --- a/cbmc/proofs/crypto_kem_dec/Makefile +++ b/cbmc/proofs/crypto_kem_dec/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)dec -USE_FUNCTION_CONTRACTS= $(FIPS202_NAMESPACE)sha3_512 $(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)indcpa_dec $(MLKEM_NAMESPACE)mlkem_shake256_rkprf $(MLKEM_NAMESPACE)verify $(MLKEM_NAMESPACE)cmov memcmp +USE_FUNCTION_CONTRACTS= $(FIPS202_NAMESPACE)sha3_512 $(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)indcpa_dec $(MLKEM_NAMESPACE)mlkem_shake256_rkprf $(MLKEM_NAMESPACE)ct_memcmp $(MLKEM_NAMESPACE)ct_cmov_zero memcmp APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/cbmc/proofs/cmov_int16/Makefile b/cbmc/proofs/ct_cmask_neg_i16/Makefile similarity index 85% rename from cbmc/proofs/cmov_int16/Makefile rename to cbmc/proofs/ct_cmask_neg_i16/Makefile index c4f35d51b..b941c4606 100644 --- a/cbmc/proofs/cmov_int16/Makefile +++ b/cbmc/proofs/ct_cmask_neg_i16/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = cmov_int16_harness +HARNESS_FILE = ct_cmask_neg_i16_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 = cmov_int16 +PROOF_UID = ct_cmask_neg_i16 DEFINES += INCLUDES += @@ -16,10 +16,10 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Dummy because the Makefile wants _some_ project source -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)cmov_int16 -USE_FUNCTION_CONTRACTS= +CHECK_FUNCTION_CONTRACTS=ct_cmask_neg_i16 +USE_FUNCTION_CONTRACTS=value_barrier_i32 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = $(MLKEM_NAMESPACE)cmov_int16 +FUNCTION_NAME = ct_cmask_neg_i16 # 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 diff --git a/cbmc/proofs/cmov/cbmc-proof.txt b/cbmc/proofs/ct_cmask_neg_i16/cbmc-proof.txt similarity index 100% rename from cbmc/proofs/cmov/cbmc-proof.txt rename to cbmc/proofs/ct_cmask_neg_i16/cbmc-proof.txt diff --git a/cbmc/proofs/cmov_int16/cmov_int16_harness.c b/cbmc/proofs/ct_cmask_neg_i16/ct_cmask_neg_i16_harness.c similarity index 77% rename from cbmc/proofs/cmov_int16/cmov_int16_harness.c rename to cbmc/proofs/ct_cmask_neg_i16/ct_cmask_neg_i16_harness.c index e8f64c481..fab9d37fb 100644 --- a/cbmc/proofs/cmov_int16/cmov_int16_harness.c +++ b/cbmc/proofs/ct_cmask_neg_i16/ct_cmask_neg_i16_harness.c @@ -7,8 +7,8 @@ */ /** - * @file cmov_int16_harness.c - * @brief Implements the proof harness for cmov_int16 function. + * @file ct_csel_int16_harness.c + * @brief Implements the proof harness for ct_csel_int16 function. */ #include "verify.h" @@ -24,8 +24,8 @@ */ void harness(void) { + int16_t a; uint16_t b; - int16_t *r, v; - cmov_int16(r, v, b); + b = ct_cmask_neg_i16(a); } diff --git a/cbmc/proofs/ct_cmask_nonzero_u16/Makefile b/cbmc/proofs/ct_cmask_nonzero_u16/Makefile new file mode 100644 index 000000000..1055bb752 --- /dev/null +++ b/cbmc/proofs/ct_cmask_nonzero_u16/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = ct_cmask_nonzero_u16_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 = ct_cmask_nonzero_u16 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Dummy because the Makefile wants _some_ project source + +CHECK_FUNCTION_CONTRACTS=ct_cmask_nonzero_u16 +USE_FUNCTION_CONTRACTS=value_barrier_u32 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = ct_cmask_nonzero_u16 + +# 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/cmov_int16/cbmc-proof.txt b/cbmc/proofs/ct_cmask_nonzero_u16/cbmc-proof.txt similarity index 100% rename from cbmc/proofs/cmov_int16/cbmc-proof.txt rename to cbmc/proofs/ct_cmask_nonzero_u16/cbmc-proof.txt diff --git a/cbmc/proofs/ct_cmask_nonzero_u16/ct_cmask_nonzero_u16_harness.c b/cbmc/proofs/ct_cmask_nonzero_u16/ct_cmask_nonzero_u16_harness.c new file mode 100644 index 000000000..be99a3528 --- /dev/null +++ b/cbmc/proofs/ct_cmask_nonzero_u16/ct_cmask_nonzero_u16_harness.c @@ -0,0 +1,30 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file ct_csel_int16_harness.c + * @brief Implements the proof harness for ct_csel_int16 function. + */ +#include "verify.h" + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) +{ + uint16_t a, b; + + b = ct_cmask_nonzero_u16(a); +} diff --git a/cbmc/proofs/ct_cmask_nonzero_u8/Makefile b/cbmc/proofs/ct_cmask_nonzero_u8/Makefile new file mode 100644 index 000000000..d74000c7e --- /dev/null +++ b/cbmc/proofs/ct_cmask_nonzero_u8/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = ct_cmask_nonzero_u8_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 = ct_cmask_nonzero_u8 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Dummy because the Makefile wants _some_ project source + +CHECK_FUNCTION_CONTRACTS=ct_cmask_nonzero_u8 +USE_FUNCTION_CONTRACTS=value_barrier_u32 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = ct_cmask_nonzero_u8 + +# 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/verify/cbmc-proof.txt b/cbmc/proofs/ct_cmask_nonzero_u8/cbmc-proof.txt similarity index 100% rename from cbmc/proofs/verify/cbmc-proof.txt rename to cbmc/proofs/ct_cmask_nonzero_u8/cbmc-proof.txt diff --git a/cbmc/proofs/ct_cmask_nonzero_u8/ct_cmask_nonzero_u8_harness.c b/cbmc/proofs/ct_cmask_nonzero_u8/ct_cmask_nonzero_u8_harness.c new file mode 100644 index 000000000..26e302c39 --- /dev/null +++ b/cbmc/proofs/ct_cmask_nonzero_u8/ct_cmask_nonzero_u8_harness.c @@ -0,0 +1,30 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file ct_csel_int16_harness.c + * @brief Implements the proof harness for ct_csel_int16 function. + */ +#include "verify.h" + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) +{ + uint8_t a, b; + + b = ct_cmask_nonzero_u8(a); +} diff --git a/cbmc/proofs/cmov/Makefile b/cbmc/proofs/ct_cmov_zero/Makefile similarity index 86% rename from cbmc/proofs/cmov/Makefile rename to cbmc/proofs/ct_cmov_zero/Makefile index a7f2006c3..06f1b2f3c 100644 --- a/cbmc/proofs/cmov/Makefile +++ b/cbmc/proofs/ct_cmov_zero/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = cmov_harness +HARNESS_FILE = ct_cmov_zero_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 = cmov +PROOF_UID = ct_cmov_zero DEFINES += INCLUDES += @@ -16,10 +16,10 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Dummy source -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)cmov -USE_FUNCTION_CONTRACTS= +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ct_cmov_zero +USE_FUNCTION_CONTRACTS=ct_sel_uint8 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--smt2 -FUNCTION_NAME = $(MLKEM_NAMESPACE)cmov +FUNCTION_NAME = $(MLKEM_NAMESPACE)ct_cmov_zero # 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 diff --git a/cbmc/proofs/ct_cmov_zero/cbmc-proof.txt b/cbmc/proofs/ct_cmov_zero/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/ct_cmov_zero/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/cmov/cmov_harness.c b/cbmc/proofs/ct_cmov_zero/ct_cmov_zero_harness.c similarity index 80% rename from cbmc/proofs/cmov/cmov_harness.c rename to cbmc/proofs/ct_cmov_zero/ct_cmov_zero_harness.c index d60c4a501..547451bf8 100644 --- a/cbmc/proofs/cmov/cmov_harness.c +++ b/cbmc/proofs/ct_cmov_zero/ct_cmov_zero_harness.c @@ -7,8 +7,8 @@ */ /** - * @file cmov_harness.c - * @brief Implements the proof harness for cmov function. + * @file ct_cmov_zero_harness.c + * @brief Implements the proof harness for ct_cmov_zero function. */ #include "verify.h" @@ -27,5 +27,5 @@ void harness(void) uint8_t *x, *y; size_t len; uint8_t b; - cmov(x, y, len, b); + ct_cmov_zero(x, y, len, b); } diff --git a/cbmc/proofs/verify/Makefile b/cbmc/proofs/ct_memcmp/Makefile similarity index 87% rename from cbmc/proofs/verify/Makefile rename to cbmc/proofs/ct_memcmp/Makefile index a471595a4..452701127 100644 --- a/cbmc/proofs/verify/Makefile +++ b/cbmc/proofs/ct_memcmp/Makefile @@ -3,11 +3,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = verify_harness +HARNESS_FILE = ct_memcmp_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 = verify +PROOF_UID = ct_memcmp DEFINES += INCLUDES += @@ -16,10 +16,10 @@ REMOVE_FUNCTION_BODY += UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)verify -USE_FUNCTION_CONTRACTS= +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ct_memcmp +USE_FUNCTION_CONTRACTS=value_barrier_u8 ct_cmask_nonzero_u8 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1 EXTERNAL_SAT_SOLVER= CBMCFLAGS=--bitwuzla -FUNCTION_NAME = $(MLKEM_NAMESPACE)verify +FUNCTION_NAME = $(MLKEM_NAMESPACE)ct_memcmp # 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 diff --git a/cbmc/proofs/ct_memcmp/cbmc-proof.txt b/cbmc/proofs/ct_memcmp/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/ct_memcmp/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/verify/verify_harness.c b/cbmc/proofs/ct_memcmp/ct_memcmp_harness.c similarity index 95% rename from cbmc/proofs/verify/verify_harness.c rename to cbmc/proofs/ct_memcmp/ct_memcmp_harness.c index c7f7cf5e5..cb1047200 100644 --- a/cbmc/proofs/verify/verify_harness.c +++ b/cbmc/proofs/ct_memcmp/ct_memcmp_harness.c @@ -28,5 +28,5 @@ void harness(void) uint8_t *b; size_t len; int r; - r = verify(a, b, len); + r = ct_memcmp(a, b, len); } diff --git a/cbmc/proofs/ct_sel_int16/Makefile b/cbmc/proofs/ct_sel_int16/Makefile new file mode 100644 index 000000000..75303e496 --- /dev/null +++ b/cbmc/proofs/ct_sel_int16/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = ct_sel_int16_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 = ct_sel_int16 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Dummy because the Makefile wants _some_ project source + +CHECK_FUNCTION_CONTRACTS=ct_sel_int16 +USE_FUNCTION_CONTRACTS=value_barrier_u16 ct_cmask_nonzero_u16 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = ct_sel_int16 + +# 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/ct_sel_int16/cbmc-proof.txt b/cbmc/proofs/ct_sel_int16/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/ct_sel_int16/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/ct_sel_int16/ct_sel_int16_harness.c b/cbmc/proofs/ct_sel_int16/ct_sel_int16_harness.c new file mode 100644 index 000000000..1d8569db7 --- /dev/null +++ b/cbmc/proofs/ct_sel_int16/ct_sel_int16_harness.c @@ -0,0 +1,31 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file ct_csel_int16_harness.c + * @brief Implements the proof harness for ct_csel_int16 function. + */ +#include "verify.h" + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) +{ + int16_t a, b, c; + uint16_t cond; + + c = ct_sel_int16(a, b, cond); +} diff --git a/cbmc/proofs/ct_sel_uint8/Makefile b/cbmc/proofs/ct_sel_uint8/Makefile new file mode 100644 index 000000000..13d6cb84a --- /dev/null +++ b/cbmc/proofs/ct_sel_uint8/Makefile @@ -0,0 +1,54 @@ +# SPDX-License-Identifier: Apache-2.0 + +include ../Makefile_params.common + +HARNESS_ENTRY = harness +HARNESS_FILE = ct_sel_uint8_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 = ct_sel_uint8 + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Dummy because the Makefile wants _some_ project source + +CHECK_FUNCTION_CONTRACTS=ct_sel_uint8 +USE_FUNCTION_CONTRACTS=value_barrier_u8 ct_cmask_nonzero_u8 +APPLY_LOOP_CONTRACTS=on +USE_DYNAMIC_FRAMES=1 + +# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead +EXTERNAL_SAT_SOLVER= +CBMCFLAGS=--smt2 + +FUNCTION_NAME = ct_sel_uint8 + +# 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/ct_sel_uint8/cbmc-proof.txt b/cbmc/proofs/ct_sel_uint8/cbmc-proof.txt new file mode 100644 index 000000000..3d1913ebf --- /dev/null +++ b/cbmc/proofs/ct_sel_uint8/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/ct_sel_uint8/ct_sel_uint8_harness.c b/cbmc/proofs/ct_sel_uint8/ct_sel_uint8_harness.c new file mode 100644 index 000000000..3665498c4 --- /dev/null +++ b/cbmc/proofs/ct_sel_uint8/ct_sel_uint8_harness.c @@ -0,0 +1,30 @@ +// Copyright (c) 2024 The mlkem-native project authors +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: MIT-0 AND Apache-2.0 + +/* + * Insert copyright notice + */ + +/** + * @file ct_csel_uint8_harness.c + * @brief Implements the proof harness for ct_csel_uint8 function. + */ +#include "verify.h" + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ + +/** + * @brief Starting point for formal analysis + * + */ +void harness(void) +{ + uint8_t a, b, c, cond; + + c = ct_sel_uint8(a, b, cond); +} diff --git a/cbmc/proofs/poly_compress_du/Makefile b/cbmc/proofs/poly_compress_du/Makefile index ff7ecef3c..cdb450aab 100644 --- a/cbmc/proofs/poly_compress_du/Makefile +++ b/cbmc/proofs/poly_compress_du/Makefile @@ -17,7 +17,6 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_du # For K = 2 or 3, the code calls scalar_compress_d10, so diff --git a/cbmc/proofs/poly_compress_dv/Makefile b/cbmc/proofs/poly_compress_dv/Makefile index 920294b68..9cc1378f1 100644 --- a/cbmc/proofs/poly_compress_dv/Makefile +++ b/cbmc/proofs/poly_compress_dv/Makefile @@ -17,7 +17,6 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_compress_dv ifeq ($(MLKEM_K),4) diff --git a/cbmc/proofs/poly_decompress_du/Makefile b/cbmc/proofs/poly_decompress_du/Makefile index 625a2f88a..e4d98e174 100644 --- a/cbmc/proofs/poly_decompress_du/Makefile +++ b/cbmc/proofs/poly_decompress_du/Makefile @@ -17,7 +17,6 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_du diff --git a/cbmc/proofs/poly_decompress_dv/Makefile b/cbmc/proofs/poly_decompress_dv/Makefile index 45bbabe0c..025ff60d0 100644 --- a/cbmc/proofs/poly_decompress_dv/Makefile +++ b/cbmc/proofs/poly_decompress_dv/Makefile @@ -17,7 +17,6 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c -PROJECT_SOURCES += $(SRCDIR)/mlkem/verify.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_decompress_dv diff --git a/cbmc/proofs/poly_frommsg/Makefile b/cbmc/proofs/poly_frommsg/Makefile index d1953ab84..06c1a3e21 100644 --- a/cbmc/proofs/poly_frommsg/Makefile +++ b/cbmc/proofs/poly_frommsg/Makefile @@ -19,13 +19,13 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)poly_frommsg -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)cmov_int16 +USE_FUNCTION_CONTRACTS=ct_sel_int16 value_barrier_u8 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 +CBMCFLAGS=--bitwuzla FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_frommsg @@ -36,7 +36,7 @@ FUNCTION_NAME = $(MLKEM_NAMESPACE)poly_frommsg # EXPENSIVE = true # This function is large enough to need... -CBMC_OBJECT_BITS = 8 +CBMC_OBJECT_BITS = 9 # 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 diff --git a/cbmc/proofs/scalar_signed_to_unsigned_q/Makefile b/cbmc/proofs/scalar_signed_to_unsigned_q/Makefile index 93494d8ab..9bb6f8b8b 100644 --- a/cbmc/proofs/scalar_signed_to_unsigned_q/Makefile +++ b/cbmc/proofs/scalar_signed_to_unsigned_q/Makefile @@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)scalar_signed_to_unsigned_q -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)cmov_int16 +USE_FUNCTION_CONTRACTS=ct_sel_int16 ct_cmask_neg_i16 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/mk/schemes.mk b/mk/schemes.mk index c74dd6c1d..6a4e7fec8 100644 --- a/mk/schemes.mk +++ b/mk/schemes.mk @@ -13,11 +13,6 @@ MLKEM512_DIR = $(BUILD_DIR)/mlkem512 MLKEM768_DIR = $(BUILD_DIR)/mlkem768 MLKEM1024_DIR = $(BUILD_DIR)/mlkem1024 -# Even when link-time optimization is used for the rest of the code, -# make sure not to use it for verify.c: Those are functions which, when -# inlined, can be subject to compiler-induced variable-time code. -%/verify.c.o: CPPFLAGS += -fno-lto - $(MLKEM512_DIR)/bin/%: CPPFLAGS += -DMLKEM_K=2 $(ALL_TESTS:%=$(MLKEM512_DIR)/bin/%512):$(MLKEM512_DIR)/bin/%512: $(MLKEM512_DIR)/test/%.c.o $(call MAKE_OBJS,$(MLKEM512_DIR), $(SOURCES)) diff --git a/mlkem/common.h b/mlkem/common.h index f8a0beb99..85ea459ee 100644 --- a/mlkem/common.h +++ b/mlkem/common.h @@ -5,9 +5,12 @@ #define DEFAULT_ALIGN 32 #if defined(_WIN32) + #define ALIGN __declspec(align(DEFAULT_ALIGN)) #define ALWAYS_INLINE __forceinline +#define asm __asm #else +#define asm __asm__ #define ALIGN __attribute__((aligned(DEFAULT_ALIGN))) #define ALWAYS_INLINE __attribute__((always_inline)) #endif diff --git a/mlkem/kem.c b/mlkem/kem.c index 780eac8b9..e785d9064 100644 --- a/mlkem/kem.c +++ b/mlkem/kem.c @@ -144,7 +144,7 @@ int crypto_kem_enc(uint8_t *ct, uint8_t *ss, const uint8_t *pk) int crypto_kem_dec(uint8_t *ss, const uint8_t *ct, const uint8_t *sk) { - int fail; + uint8_t fail; ALIGN uint8_t buf[2 * MLKEM_SYMBYTES]; /* Will contain key, coins */ ALIGN uint8_t kr[2 * MLKEM_SYMBYTES]; @@ -166,13 +166,13 @@ int crypto_kem_dec(uint8_t *ss, const uint8_t *ct, const uint8_t *sk) /* coins are in kr+MLKEM_SYMBYTES */ indcpa_enc(cmp, buf, pk, kr + MLKEM_SYMBYTES); - fail = verify(ct, cmp, MLKEM_CIPHERTEXTBYTES); + fail = ct_memcmp(ct, cmp, MLKEM_CIPHERTEXTBYTES); /* Compute rejection key */ rkprf(ss, sk + MLKEM_SECRETKEYBYTES - MLKEM_SYMBYTES, ct); - /* Copy true key to return buffer if fail is false */ - cmov(ss, kr, MLKEM_SYMBYTES, !fail); + /* Copy true key to return buffer if fail is 0 */ + ct_cmov_zero(ss, kr, MLKEM_SYMBYTES, fail); return 0; } diff --git a/mlkem/poly.c b/mlkem/poly.c index f0d300e3e..ccf214f06 100644 --- a/mlkem/poly.c +++ b/mlkem/poly.c @@ -319,8 +319,9 @@ void poly_frommsg(poly *r, const uint8_t msg[MLKEM_INDCPA_MSGBYTES]) invariant(i >= 0 && i < MLKEM_N / 8 && j >= 0 && j <= 8) invariant(array_bound(r->coeffs, 0, (8 * i + j - 1), 0, (MLKEM_Q - 1)))) { - r->coeffs[8 * i + j] = 0; - cmov_int16(&r->coeffs[8 * i + j], HALF_Q, (msg[i] >> j) & 1); + // Prevent the compiler from recognizing this as a bit selection + uint8_t mask = value_barrier_u8(1u << j); + r->coeffs[8 * i + j] = ct_sel_int16(HALF_Q, 0, msg[i] & mask); } } POLY_BOUND_MSG(r, MLKEM_Q, "poly_frommsg output"); @@ -335,8 +336,7 @@ void poly_tomsg(uint8_t msg[MLKEM_INDCPA_MSGBYTES], const poly *a) { msg[i] = 0; for (int j = 0; j < 8; j++) - __loop__( - invariant(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)) + __loop__(invariant(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)) { uint32_t t = scalar_compress_d1(a->coeffs[8 * i + j]); msg[i] |= t << j; diff --git a/mlkem/poly.h b/mlkem/poly.h index bf6f62507..132e44814 100644 --- a/mlkem/poly.h +++ b/mlkem/poly.h @@ -300,7 +300,7 @@ __contract__( ensures(return_value == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q))) { // Add Q if c is negative, but in constant time - cmov_int16(&c, c + MLKEM_Q, c < 0); + c = ct_sel_int16(c + MLKEM_Q, c, ct_cmask_neg_i16(c)); cassert(c >= 0, "scalar_signed_to_unsigned_q result lower bound"); cassert(c < MLKEM_Q, "scalar_signed_to_unsigned_q result upper bound"); diff --git a/mlkem/verify.c b/mlkem/verify.c index c60222e61..ea99afcbb 100644 --- a/mlkem/verify.c +++ b/mlkem/verify.c @@ -1,81 +1,5 @@ // Copyright (c) 2024 The mlkem-native project authors // SPDX-License-Identifier: Apache-2.0 #include "verify.h" -#include -#include -// -// WARNING: -// -// The functions in this compilation unit may be susceptible to -// compiler-induced variable-time code when inlined into their call-sites. -// The purpose of having a separate compilation here is to prevent -// such potentially insecure inlining. -// -// You MUST NOT compile this file using link time optimization. -// - -int verify(const uint8_t *a, const uint8_t *b, const size_t len) -{ - uint8_t r = 0; - uint64_t u; - - // Switch to a _signed_ ilen value, so that our loop counter - // can also be signed, and thus (i - 1) in the loop invariant - // can yield -1 as required. - const int ilen = (int)len; - - for (int i = 0; i < ilen; i++) - __loop__( - invariant(i >= 0 && i <= ilen) - invariant((r == 0) == (forall(int, k, 0, (i - 1), (a[k] == b[k]))))) - { - r |= a[i] ^ b[i]; - } - -#ifdef CBMC -#pragma CPROVER check push -#pragma CPROVER check disable "unsigned-overflow" -#endif - u = (-(uint64_t)r) >> 63; -#ifdef CBMC -#pragma CPROVER check pop -#endif - - return (int)u; -} - -void cmov(uint8_t *r, const uint8_t *x, size_t len, uint8_t b) -{ - size_t i; - - b = (-b) & 0xFF; - for (i = 0; i < len; i++) - __loop__(invariant(i <= len)) - { - r[i] ^= b & (r[i] ^ x[i]); - } -} - -/************************************************* - * Note: - * - * Constant-time implementation. Relies on basic - * properties of bitwise ^ or and &. - **************************************************/ -void cmov_int16(int16_t *r, const int16_t v, const uint16_t b) -{ -// CBMC issues false alarms here for the implicit conversions between -// uint16_t and int, so disable "conversion-check" here for now. -#pragma CPROVER check push -#pragma CPROVER check disable "conversion" - - // b == 0 => mask = 0x0000 - // b == 1 => mask = 0xFFFF - const uint16_t mask = -b; - - // mask == 0x0000 => *r == (*r ^ 0x0000) == *r - // mask == 0xFFFF => *r == (*r ^ (*r ^ v)) == (*r ^ *r) ^ v == 0 ^ v == v - *r ^= mask & ((*r) ^ v); -#pragma CPROVER check pop -} +volatile uint64_t ct_opt_blocker_u64; diff --git a/mlkem/verify.h b/mlkem/verify.h index b58680515..e64fda993 100644 --- a/mlkem/verify.h +++ b/mlkem/verify.h @@ -9,9 +9,172 @@ #include "cbmc.h" #include "params.h" -#define verify MLKEM_NAMESPACE(verify) +#if !defined(CBMC) && !defined(_WIN32) +#define MLKEM_USE_ASM_VALUE_BARRIER +#endif + +#define ct_opt_blocker_u64 MLKEM_NAMESPACE(ct_opt_blocker_u64) +extern volatile uint64_t ct_opt_blocker_u64; + +STATIC_INLINE_TESTABLE uint8_t get_optblocker_u8(void) +__contract__(ensures(return_value == 0)) { return (uint8_t)ct_opt_blocker_u64; } + +STATIC_INLINE_TESTABLE uint16_t get_optblocker_u16(void) +__contract__(ensures(return_value == 0)) { return ct_opt_blocker_u64; } + +STATIC_INLINE_TESTABLE uint32_t get_optblocker_u32(void) +__contract__(ensures(return_value == 0)) { return ct_opt_blocker_u64; } + +STATIC_INLINE_TESTABLE uint64_t get_optblocker_u64(void) +__contract__(ensures(return_value == 0)) { return ct_opt_blocker_u64; } + +STATIC_INLINE_TESTABLE uint8_t value_barrier_u8(uint8_t b) +__contract__(ensures(return_value == b)) +{ +#if defined(MLKEM_USE_ASM_VALUE_BARRIER) + asm("" : "+r"(b)); + return b; +#else + return (b ^ get_optblocker_u8()); +#endif +} + +STATIC_INLINE_TESTABLE uint16_t value_barrier_u16(uint16_t b) +__contract__(ensures(return_value == b)) +{ +#if defined(MLKEM_USE_ASM_VALUE_BARRIER) + asm("" : "+r"(b)); + return b; +#else + return (b ^ get_optblocker_u8()); +#endif +} + +STATIC_INLINE_TESTABLE uint32_t value_barrier_u32(uint32_t b) +__contract__(ensures(return_value == b)) +{ +#if defined(MLKEM_USE_ASM_VALUE_BARRIER) + asm("" : "+r"(b)); + return b; +#else + return (b ^ get_optblocker_u8()); +#endif +} + +STATIC_INLINE_TESTABLE int32_t value_barrier_i32(int32_t b) +__contract__(ensures(return_value == b)) +{ +#if defined(MLKEM_USE_ASM_VALUE_BARRIER) + asm("" : "+r"(b)); + return b; +#else + return (b ^ get_optblocker_u8()); +#endif +} + +// The ct_cmask_nonzero_xxx functions below make deliberate use of unsigned +// overflow, which is fully defined behaviour in C. It is thus safe to disable +// this warning. +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "unsigned-overflow" +#endif + +STATIC_INLINE_TESTABLE uint16_t ct_cmask_nonzero_u16(uint16_t x) +__contract__(ensures(return_value == ((x == 0) ? 0 : 0xFFFF))) +{ + uint32_t tmp = value_barrier_u32(-((uint32_t)x)); + tmp >>= 16; + return tmp; +} + +STATIC_INLINE_TESTABLE uint8_t ct_cmask_nonzero_u8(uint8_t x) +__contract__(ensures(return_value == ((x == 0) ? 0 : 0xFF))) +{ + uint32_t tmp = value_barrier_u32(-((uint32_t)x)); + tmp >>= 24; + return tmp; +} + +// Put unsigned overflow warnings in CBMC back into scope +#ifdef CBMC +#pragma CPROVER check pop +#endif + +// The ct_cmask_neg_i16 function below makes deliberate use of +// signed to unsigned integer conversion, which is fully defined +// behaviour in C. It is thus safe to disable this warning. +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "conversion" +#endif + +STATIC_INLINE_TESTABLE uint16_t ct_cmask_neg_i16(int16_t x) +__contract__(ensures(return_value == ((x < 0) ? 0xFFFF : 0))) +{ + int32_t tmp = value_barrier_i32((int32_t)x); + tmp >>= 16; + return (int16_t)tmp; +} + +// Put unsigned-to-signed warnings in CBMC back into scope +#ifdef CBMC +#pragma CPROVER check pop +#endif + +// The ct_csel_xxx functions below make deliberate use of unsigned +// to signed integer conversion, which is implementation-defined +// behaviour. Here, we assume that uint16_t -> int16_t is inverse +// to int16_t -> uint16_t. +#ifdef CBMC +#pragma CPROVER check push +#pragma CPROVER check disable "conversion" +#endif + /************************************************* - * Name: verify + * Name: ct_sel_int16 + * + * Description: Functionally equivalent to cond ? a : b, + * but implemented with guards against + * compiler-introduced branches. + * + * Arguments: int16_t a: First alternative + * int16_t b: Second alternative + * uint16_t cond: Condition variable. + **************************************************/ +STATIC_INLINE_TESTABLE int16_t ct_sel_int16(int16_t a, int16_t b, uint16_t cond) +__contract__(ensures(return_value == (cond ? a : b))) +{ + uint16_t au = a, bu = b; + uint16_t res = bu ^ (ct_cmask_nonzero_u16(cond) & (au ^ bu)); + return (int16_t)res; +} + +// Put unsigned-to-signed warnings in CBMC back into scope +#ifdef CBMC +#pragma CPROVER check pop +#endif + +/************************************************* + * Name: ct_sel_uint8 + * + * Description: Functionally equivalent to cond ? a : b, + * but implemented with guards against + * compiler-introduced branches. + * + * Arguments: uint8_t a: First alternative + * uint8_t b: Second alternative + * uuint8_t cond: Condition variable. + **************************************************/ +STATIC_INLINE_TESTABLE uint8_t ct_sel_uint8(uint8_t a, uint8_t b, uint8_t cond) +__contract__(ensures(return_value == (cond ? a : b))) +{ + return b ^ (ct_cmask_nonzero_u8(cond) & (a ^ b)); +} + +#define ct_memcmp MLKEM_NAMESPACE(ct_memcmp) +/************************************************* + * Name: ct_memcmp * * Description: Compare two arrays for equality in constant time. * @@ -19,56 +182,68 @@ * const uint8_t *b: pointer to second byte array * size_t len: length of the byte arrays * - * Returns 0 if the byte arrays are equal, 1 otherwise + * Returns 0 if the byte arrays are equal, a non-zero value otherwise **************************************************/ -int verify(const uint8_t *a, const uint8_t *b, const size_t len) +STATIC_INLINE_TESTABLE uint8_t ct_memcmp(const uint8_t *a, const uint8_t *b, + const size_t len) __contract__( requires(memory_no_alias(a, len)) requires(memory_no_alias(b, len)) requires(len <= INT_MAX) - ensures(return_value == (1 - forall(int, i, 0, ((int)len - 1), (a[i] == b[i])))) -); + ensures((return_value == 0) == forall(int, i, 0, ((int)len - 1), (a[i] == b[i])))) +{ + uint8_t r = 0, s = 0; + + // Switch to a _signed_ ilen value, so that our loop counter + // can also be signed, and thus (i - 1) in the loop invariant + // can yield -1 as required. + const int ilen = (int)len; -#define cmov MLKEM_NAMESPACE(cmov) + for (int i = 0; i < ilen; i++) + __loop__( + invariant(i >= 0 && i <= ilen) + invariant((r == 0) == (forall(int, k, 0, (i - 1), (a[k] == b[k]))))) + { + r |= a[i] ^ b[i]; + // s is useless, but prevents the loop from being aborted once r=0xff. + s ^= a[i] ^ b[i]; + } + + // - Convert r into a mask; this may not be necessary, but is an additional + // safeguard + // towards leaking information about a and b. + // - XOR twice with s, separated by a value barrier, to prevent the compiler + // from dropping the s computation in the loop. + return (value_barrier_u8(ct_cmask_nonzero_u8(r) ^ s) ^ s); +} + +#define ct_cmov_zero MLKEM_NAMESPACE(ct_cmov_zero) /************************************************* - * Name: cmov + * Name: ct_cmov_zero * - * Description: Copy len bytes from x to r if b is 1; - * don't modify x if b is 0. Requires b to be in {0,1}; + * Description: Copy len bytes from x to r if b is zero; + * don't modify x if b is non-zero. * assumes two's complement representation of negative integers. * Runs in constant time. * * Arguments: uint8_t *r: pointer to output byte array * const uint8_t *x: pointer to input byte array * size_t len: Amount of bytes to be copied - * uint8_t b: Condition bit; has to be in {0,1} + * uint8_t b: Condition value. **************************************************/ -void cmov(uint8_t *r, const uint8_t *x, size_t len, uint8_t b) +STATIC_INLINE_TESTABLE +void ct_cmov_zero(uint8_t *r, const uint8_t *x, size_t len, uint8_t b) __contract__( requires(memory_no_alias(r, len)) requires(memory_no_alias(x, len)) - requires(b == 0 || b == 1) - assigns(memory_slice(r, len)) -); - -#define cmov_int16 MLKEM_NAMESPACE(cmov_int16) -/************************************************* - * Name: cmov_int16 - * - * Description: Copy input v to *r if b is 1, don't modify *r if b is 0. - * Requires b to be in {0,1}; - * Runs in constant time. - * - * Arguments: int16_t *r: pointer to output int16_t - * int16_t v: input int16_t. Must not be NULL - * uint16_t b: Condition bit; has to be in {0,1} - **************************************************/ -void cmov_int16(int16_t *r, const int16_t v, const uint16_t b) -__contract__( - requires(b == 0 || b == 1) - requires(memory_no_alias(r, sizeof(int16_t))) - assigns(memory_slice(r, sizeof(int16_t))) - ensures(*r == (b ? v : old(*r))) -); + assigns(memory_slice(r, len))) +{ + size_t i; + for (i = 0; i < len; i++) + __loop__(invariant(i <= len)) + { + r[i] = ct_sel_uint8(r[i], x[i], b); + } +} #endif