trusted boot: use XMSS signatures instead of a SHA256 hash

components/include/cn_array_utils.h

@@ -2,6 +2,12 @@
 #define CN_ARRAY_UTILS_H_
 
 /*$
+predicate (map<u64,u8>) Array_u8 (pointer p, u64 l)
+{
+  take pv = each(u64 i; i >= 0u64 && i < l) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
+  return pv;
+}
+
 predicate (map<u64,u8>) ArrayOrNull_u8 (pointer p, u64 l)
 {
   if (!is_null(p)) {

components/include/cn_memory.h

@@ -69,4 +69,6 @@ ensures
     take i = each(u64 j; j >= 0u64 && j < n) {Block<uint8_t>(array_shift<uint8_t>(return, j))};
 $*/
 
+void *_realloc(void *ptr, size_t size);
+
 #endif // CN_MEMCPY_H_

components/platform_crypto/shave_trusted_boot/Makefile

@@ -21,7 +21,7 @@ TRUSTED_BOOT_BIN = trusted_boot$(TARGET_SUFFIX)
 
 SRC = $(wildcard $(ROOT_DIR)/*.c)
 OBJ = $(SRC:$(ROOT_DIR)/%.c=$(BUILD_DIR)/%.o)
-CFLAGS = -I$(ROOT_DIR)
+CFLAGS = -I$(ROOT_DIR) -DNO_XMSS
 
 CN_FLAGS=-I$(ROOT_DIR) -I$(ROOT_DIR)/../../include --include=$(ROOT_DIR)/../../include/wars.h --magic-comment-char-dollar
 CN=cn verify $(CN_FLAGS)
@@ -39,12 +39,16 @@ clean:
 	rm -rf build/ build.*/
 	rm -f $(TRUSTED_BOOT_BIN)
 
-.PHONY: cn_proof_trusted_boot cn_proof_firmware cn_proof_firmware_with_attest
-cn_proof: cn_proof_trusted_boot cn_proof_firmware cn_proof_firmware_with_attest
+.PHONY: cn_proof_trusted_boot cn_proof_firmware cn_proof_firmware_with_attest cn_proof_xmss
+cn_proof: cn_proof_trusted_boot cn_proof_firmware cn_proof_firmware_with_attest cn_proof_xmss
+
+cn_proof_xmss:
+	cn verify --magic-comment-char-dollar -Ixmss-library/src -Ixmss-library/include -I xmss-library/build/include -I xmss-library/build/src test-xmss_sign_verify.c
 
 cn_proof_trusted_boot: $(ROOT_DIR)/trusted_boot.c
 	$(CN) --skip=parse_hex_str $<
 cn_proof_firmware: $(ROOT_DIR)/firmware.c
-	$(CN) $<
+	$(CN) -DNO_XMSS $<
+	$(CN) -Ixmss-library/src -Ixmss-library/include -I xmss-library/build/include -I xmss-library/build/src  $< --skip=native_to_big_endian_256,native_to_big_endian,inplace_native_to_big_endian,big_endian_to_native,big_endian_to_native_256,inplace_big_endian_to_native,inplace_big_endian_to_native_256,inplace_native_to_big_endian_256,convert_big_endian_word,xmss_get_signature_struct,compare_values_256,compare_native_values_256,xmss_F,xmss_H,xmss_H_msg_init,xmss_H_msg_update,xmss_H_msg_finalize,xmss_PRFkeygen,xmss_PRFindex,xmss_digest,xmss_native_digest,sign_verify_test
 cn_proof_firmware_with_attest: $(ROOT_DIR)/firmware.c
 	$(CN) -DWITH_ATTEST $<

components/platform_crypto/shave_trusted_boot/firmware.c

@@ -5,6 +5,7 @@
 #include <stddef.h>
 #include <stdint.h>
 #include <string.h>
+#include <stdbool.h>
 
 #include "sha_256.h"
 #include "hmac_sha256.h"
@@ -14,6 +15,240 @@
 #include "cn_array_utils.h"
 #define memcpy(f,b,s) _memcpy(f,b,s)
 #define memcmp(f,b,s) _memcmp(f,b,s)
+#define free _free
+#define realloc _realloc
+#endif
+
+//#define _Static_assert(...) extern int bogus
+#if !defined(NO_XMSS)
+#define union struct
+#define __STDC_NO_ATOMICS__ 1
+#include "endianness.h"
+#include "signing.h"
+#include "signing_private.h"
+#include "verification.h"
+#endif
+
+
+#if 0
+/*
+ * Run sign and verify test, in which a single signature is generated and verified as a sanity check.
+ * Generates a key for the provided parameter set, places a signature and verifies that the signature verifies.
+*/
+static bool sign_verify_test(XmssParameterSetOID test_parameter_set)
+{
+    bool success = true;
+
+    XmssSigningContext *context_ptr_dynamic = NULL;
+    XmssKeyContext *key_context = NULL;
+    XmssPrivateKeyStatelessBlob *stateless_blob = NULL;
+    XmssPrivateKeyStatefulBlob *stateful_blob = NULL;
+    XmssKeyGenerationContext *keygen_context = NULL;
+    XmssPublicKeyInternalBlob *public_key_blob = NULL;
+    XmssInternalCache *internal_cache = NULL;
+    XmssInternalCache *generation_cache = NULL;
+    XmssPublicKey exported_public_key = { 0 };
+    XmssSignatureBlob *signature_blob = NULL;
+
+    success = success && XMSS_OKAY == xmss_context_initialize(&context_ptr_dynamic, test_parameter_set, realloc, free, NULL);
+
+    uint8_t random[32] = {0};
+    uint8_t secure_random[96] = {0};
+
+    XmssBuffer random_buffer = {sizeof(random), random};
+    XmssBuffer secure_random_buffer = {sizeof(secure_random), secure_random};
+    XmssIndexObfuscationSetting index_obfuscation_setting = XMSS_INDEX_OBFUSCATION_OFF;
+
+    uint8_t message_buffer[1 * 136] = {0};
+    XmssBuffer message = {sizeof(message_buffer), message_buffer};
+
+    XmssVerificationContext verification_ctx = {0};
+    XmssSignature *signature = NULL;
+
+    const uint8_t *volatile part_verify = NULL;
+
+    /*$ assert(is_null(signature_blob)); $*/
+    #if 0
+    for (size_t i = 0; i < sizeof(secure_random); i++)
+    /*$ inv
+      i <= sizeof<uint8_t[96]>;
+      take cpdi = Owned<XmssSigningContext>(context_ptr_dynamic);
+    $*/
+    {
+        /*$ extract Owned<uint8_t>, (u64) i; $*/
+        secure_random[i] = (uint8_t)i;
+    }
+    #endif
+    /*$ assert(is_null(signature_blob)); $*/
+
+    /* Call xmss_generate_private_key with some reasonable params. */
+    success = success && xmss_generate_private_key(&key_context, &stateless_blob, &stateful_blob,
+            &secure_random_buffer, index_obfuscation_setting, &random_buffer, context_ptr_dynamic) == XMSS_OKAY;
+
+    success = success && XMSS_OKAY == xmss_generate_public_key(&keygen_context, &internal_cache, &generation_cache,
+            key_context, XMSS_CACHE_TOP, 0, 1);
+    /*$ assert(success != 0u8); $*/
+    success = success && XMSS_OKAY == xmss_calculate_public_key_part(keygen_context, 0);
+    success = success && XMSS_OKAY == xmss_finish_calculate_public_key(&public_key_blob, &keygen_context,
+            key_context);
+    success = success && (keygen_context == NULL);
+
+    success = success && XMSS_OKAY == xmss_export_public_key(&exported_public_key, key_context);
+    success = success && XMSS_OKAY == xmss_request_future_signatures(&stateful_blob, key_context, 1);
+
+    /*$ assert(is_null(signature_blob)); $*/
+    // The message, 10 * the maximum block size (136 for SHAKE)
+    #if 0
+    uint8_t message_buffer[10 * 136];
+    #endif
+    #if 0
+    for (size_t i = 0; i < sizeof(message_buffer); i++)
+    /*$ inv
+      i <= 136u64;
+    $*/
+    {
+        // some "random" stuff, doesn't really matter
+        /*$ extract Owned<uint8_t>, i; $*/
+        message_buffer[i] = (uint8_t)((13ull + 31ull * i) & 0xffull);
+    }
+    #endif
+    #if 0
+    XmssBuffer message = {sizeof(message_buffer), message_buffer};
+    #endif
+
+    // Sign the message
+    /*$ assert(is_null(signature_blob)); $*/
+    /*$ assert(success != 0u8); $*/
+    success = success && XMSS_OKAY == xmss_sign_message(&signature_blob, key_context, &message);
+    /*$ assert(!is_null(signature_blob)); $*/
+
+    // Verify that the signature verifies
+    signature = xmss_get_signature_struct(signature_blob);
+    success = success && XMSS_OKAY == xmss_verification_init(&verification_ctx, &exported_public_key, signature,
+        signature_blob->data_size);
+    #if 1
+    success = success && XMSS_OKAY == xmss_verification_update(&verification_ctx, message.data, message.data_size,
+        &part_verify);
+    success = success && part_verify == message.data;
+    success = success && XMSS_OKAY == xmss_verification_check(&verification_ctx, &exported_public_key);
+    // redundant, for fault tolerance
+    success = success && XMSS_OKAY == xmss_verification_check(&verification_ctx, &exported_public_key);
+    #endif
+
+    #if 0
+    // Verify message with different "corner case" part sizes (block size SHA256: 64, SHAKE256/256: 136)
+    // We'll test every combination of first part size + part size for the remainder (i.e., this is 400+ test cases).
+    size_t part_sizes[] = {
+        0,
+        1,
+        2,
+        64 - 2,
+        64 - 1,
+        64,
+        64 + 1,
+        64 + 2,
+        136 - 2,
+        136 - 1,
+        136,
+        136 + 1,
+        136 + 2,
+        2 * 64 - 2,
+        2 * 64 - 1,
+        2 * 64,
+        2 * 64 + 1,
+        2 * 64 + 2,
+        2 * 136 - 2,
+        2 * 136 - 1,
+        2 * 136,
+        2 * 136 + 1,
+        2 * 136 + 2,
+        sizeof(message_buffer) - 2,
+        sizeof(message_buffer) - 1,
+    };
+    for (size_t first_index = 0; first_index < sizeof(part_sizes) / sizeof(size_t); ++first_index) {
+        // We need to skip size 0 for the remaining parts
+        for (size_t other_index = 1; other_index < sizeof(part_sizes) / sizeof(size_t); ++other_index) {
+            const uint8_t *part = message.data;
+            size_t remaining = message.data_size;
+            // size of the first part
+            size_t part_size = part_sizes[first_index];
+
+            success = success && XMSS_OKAY == xmss_verification_init(&verification_ctx, &exported_public_key, signature,
+                signature_blob->data_size);
+            while (remaining > 0) {
+                if (part_size > remaining) {
+                    // we've reached the end, this is the final part
+                    part_size = remaining;
+                }
+
+                success = success && XMSS_OKAY == xmss_verification_update(&verification_ctx, part, part_size,
+                    &part_verify);
+                success = success && part_verify == part;
+
+                part += part_size;
+                remaining -= part_size;
+                // size of the remaining parts, if any
+                part_size = part_sizes[other_index];
+            }
+            success = success && XMSS_OKAY == xmss_verification_check(&verification_ctx, &exported_public_key);
+            // redundant, for fault tolerance
+            success = success && XMSS_OKAY == xmss_verification_check(&verification_ctx, &exported_public_key);
+        }
+    }
+    #endif
+
+    free(signature_blob);
+    free(keygen_context);
+    xmss_free_key_context(key_context);
+    free(public_key_blob);
+    free(stateless_blob);
+    free(stateful_blob);
+    free(context_ptr_dynamic);
+    free(internal_cache);
+    free(generation_cache);
+
+    return success;
+}
+#endif
+
+#if !defined(NO_XMSS)
+static bool xmss_verify_signature(XmssPublicKey *exported_public_key, uint8_t *msg, size_t msg_size, XmssSignatureBlob *signature_blob)
+/*$
+  requires
+    take epki = Owned<XmssPublicKey>(exported_public_key);
+    take mi = Array_u8(msg, msg_size);
+    take sbi = Owned<XmssSignatureBlob>(signature_blob);
+
+  ensures
+    take epko = Owned<XmssPublicKey>(exported_public_key);
+    take mo = Array_u8(msg, msg_size);
+    take sbo = Owned<XmssSignatureBlob>(signature_blob);
+$*/
+{
+    bool success = true;
+
+    XmssBuffer message = {msg_size, msg};
+
+    XmssVerificationContext verification_ctx = {0};
+    XmssSignature *signature = NULL;
+
+    const uint8_t *volatile part_verify = NULL;
+
+    // Verify that the signature verifies
+    signature = xmss_get_signature_struct(signature_blob);
+    success = success && XMSS_OKAY == xmss_verification_init(&verification_ctx, exported_public_key, signature,
+        signature_blob->data_size);
+    success = success && XMSS_OKAY == xmss_verification_update(&verification_ctx, message.data, message.data_size,
+        &part_verify);
+    success = success && part_verify == message.data;
+    success = success && XMSS_OKAY == xmss_verification_check(&verification_ctx, exported_public_key);
+    // redundant, for fault tolerance
+    success = success && XMSS_OKAY == xmss_verification_check(&verification_ctx, exported_public_key);
+
+    /*$ apply Unxmss_get_signature_struct(signature_blob, signature); $*/
+
+    return success;
+}
 #endif
 
 typedef unsigned char byte;
@@ -26,6 +261,13 @@ uint64_t c_MEASURE_SIZE() /*$ cn_function MEASURE_SIZE; $*/ { return MEASURE_SIZ
 #if defined(WITH_ATTEST) || defined(CN_ENV)
 // must go in special protected storage (writable only by firmware/hardware)
 static byte last_measure[MEASURE_SIZE];  // initial contents unimportant
+#if defined(NO_XMSS)
+static bool public_key;
+static bool xmss_signature;
+#else
+static XmssPublicKey public_key;
+static XmssSignatureBlob xmss_signature;
+#endif
 #endif
 
 static unsigned int boot_once __attribute__ ((section (".tbootdata") ));
@@ -54,6 +296,8 @@ int reset(void *start_address,
   // TODO need a trick for start and end address. In particular note than this range can contain expected_measure
 /*$ accesses boot_once;
   accesses last_measure;
+  accesses public_key;
+  accesses xmss_signature;
   requires
     take si = each(u64 i; i >= 0u64 && i < (((u64)end_address) - ((u64)start_address))) { Owned<uint8_t>(array_shift<uint8_t>(start_address, i))};
     take emi = ArrayOrNull_u8(expected_measure, MEASURE_SIZE());
@@ -86,6 +330,7 @@ int reset(void *start_address,
   size_t region_size = (e < s) ? 0 : (e - s);
 #endif
 
+#if defined(NO_XMSS)
   // apply SHA-256 to region
   SHA256((byte *)start_address,region_size,&last_measure[0]);
 
@@ -94,6 +339,11 @@ int reset(void *start_address,
       &&
       (memcmp(last_measure,expected_measure_,MEASURE_SIZE) != 0))
     return HASH_MISMATCH;
+#else
+  if (!xmss_verify_signature(&public_key, start_address, region_size, &xmss_signature)) {
+    return HASH_MISMATCH;
+  }
+#endif
 
   boot_once = 1;