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 <[email protected]>

.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)={}

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

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
 

cbmc/proofs/cmov_int16/Makefile → 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,18 +16,18 @@ 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
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 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

cbmc/proofs/cmov_int16/cmov_int16_harness.c → 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);
 }

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

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);
+}

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

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);
+}

cbmc/proofs/cmov/Makefile → 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,18 +16,18 @@ 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
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 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

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.

cbmc/proofs/cmov/cmov_harness.c → 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);
 }

cbmc/proofs/verify/Makefile → 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,18 +16,18 @@ 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
 
 # Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
 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

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.

cbmc/proofs/verify/verify_harness.c → 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);
 }