From 557c6da91c1fa178c12816e1af0787bea2449a9b Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Fri, 29 Nov 2024 08:44:02 +0000 Subject: [PATCH] Harden constant time functions against inlining and optimizations The functions in `verify.c` are suspectible to be compiled into variable-time code when inlined. For this reason, we disable LTO for `verify.c` in our own build, and explicitly warn about it in the README.md and `verify.c`. Yet, with mlkem-native being intended as a code-package, there is risk that users will copy-paste the code and compile it with LTO enabled, overlooking the warning. This commit is an attempt to improve robustness towards LTO by rewriting verify.c so that it is safe even when inlined. The main idea is to mask values which the compiler can detect to be 0 or 1, to avoid branches being introduced for them. More precisely, we introduce a "value barrier" which is a functionally a no-op, but is written so that the compiler cannot reason that it is. Then, all 0/1 values are fed through a value barrier before further processing. We consider two approaches to implement a value barrier: - When supported, an empty inline asm block which marks the target value as clobbered. - XOR'ing with the value of a volatile global that's set to 0. The first approach is rather cheap because it only prevents the compiler from reasoning about the value of the variable past the barrier. The second generates redundant loads which therefore incur a runtime cost. Yet, it seems both more portable and more robust. Signed-off-by: Hanno Becker --- .clang-format | 3 +- README.md | 7 - cbmc/proofs/crypto_kem_dec/Makefile | 2 +- .../{cmov_int16 => ct_cmask_neg_i16}/Makefile | 12 +- .../{cmov => ct_cmask_neg_i16}/cbmc-proof.txt | 0 .../ct_cmask_neg_i16_harness.c} | 8 +- cbmc/proofs/ct_cmask_nonzero_u16/Makefile | 54 ++++ .../cbmc-proof.txt | 0 .../ct_cmask_nonzero_u16_harness.c | 30 +++ cbmc/proofs/ct_cmask_nonzero_u8/Makefile | 54 ++++ .../cbmc-proof.txt | 0 .../ct_cmask_nonzero_u8_harness.c | 30 +++ cbmc/proofs/{cmov => ct_cmov_zero}/Makefile | 12 +- cbmc/proofs/ct_cmov_zero/cbmc-proof.txt | 3 + .../ct_cmov_zero_harness.c} | 6 +- cbmc/proofs/{verify => ct_memcmp}/Makefile | 12 +- cbmc/proofs/ct_memcmp/cbmc-proof.txt | 3 + .../ct_memcmp_harness.c} | 2 +- cbmc/proofs/ct_sel_int16/Makefile | 54 ++++ cbmc/proofs/ct_sel_int16/cbmc-proof.txt | 3 + .../ct_sel_int16/ct_sel_int16_harness.c | 31 +++ cbmc/proofs/ct_sel_uint8/Makefile | 54 ++++ cbmc/proofs/ct_sel_uint8/cbmc-proof.txt | 3 + .../ct_sel_uint8/ct_sel_uint8_harness.c | 30 +++ cbmc/proofs/poly_compress_du/Makefile | 1 - cbmc/proofs/poly_compress_dv/Makefile | 1 - cbmc/proofs/poly_decompress_du/Makefile | 1 - cbmc/proofs/poly_decompress_dv/Makefile | 1 - cbmc/proofs/poly_frommsg/Makefile | 6 +- .../scalar_signed_to_unsigned_q/Makefile | 2 +- mk/schemes.mk | 5 - mlkem/common.h | 3 + mlkem/kem.c | 8 +- mlkem/poly.c | 8 +- mlkem/poly.h | 2 +- mlkem/verify.c | 78 +----- mlkem/verify.h | 245 +++++++++++++++--- 37 files changed, 605 insertions(+), 169 deletions(-) rename cbmc/proofs/{cmov_int16 => ct_cmask_neg_i16}/Makefile (85%) rename cbmc/proofs/{cmov => ct_cmask_neg_i16}/cbmc-proof.txt (100%) rename cbmc/proofs/{cmov_int16/cmov_int16_harness.c => ct_cmask_neg_i16/ct_cmask_neg_i16_harness.c} (77%) create mode 100644 cbmc/proofs/ct_cmask_nonzero_u16/Makefile rename cbmc/proofs/{cmov_int16 => ct_cmask_nonzero_u16}/cbmc-proof.txt (100%) create mode 100644 cbmc/proofs/ct_cmask_nonzero_u16/ct_cmask_nonzero_u16_harness.c create mode 100644 cbmc/proofs/ct_cmask_nonzero_u8/Makefile rename cbmc/proofs/{verify => ct_cmask_nonzero_u8}/cbmc-proof.txt (100%) create mode 100644 cbmc/proofs/ct_cmask_nonzero_u8/ct_cmask_nonzero_u8_harness.c rename cbmc/proofs/{cmov => ct_cmov_zero}/Makefile (86%) create mode 100644 cbmc/proofs/ct_cmov_zero/cbmc-proof.txt rename cbmc/proofs/{cmov/cmov_harness.c => ct_cmov_zero/ct_cmov_zero_harness.c} (80%) rename cbmc/proofs/{verify => ct_memcmp}/Makefile (87%) create mode 100644 cbmc/proofs/ct_memcmp/cbmc-proof.txt rename cbmc/proofs/{verify/verify_harness.c => ct_memcmp/ct_memcmp_harness.c} (95%) create mode 100644 cbmc/proofs/ct_sel_int16/Makefile create mode 100644 cbmc/proofs/ct_sel_int16/cbmc-proof.txt create mode 100644 cbmc/proofs/ct_sel_int16/ct_sel_int16_harness.c create mode 100644 cbmc/proofs/ct_sel_uint8/Makefile create mode 100644 cbmc/proofs/ct_sel_uint8/cbmc-proof.txt create mode 100644 cbmc/proofs/ct_sel_uint8/ct_sel_uint8_harness.c 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