Skip to content

Commit

Permalink
Specify XmssSignatureBlob with length prefix
Browse files Browse the repository at this point in the history
  • Loading branch information
@peterohanley
peterohanley committed Feb 12, 2025
1 parent 0708ae7 commit 9217268
Show file tree
Hide file tree
Showing 3 changed files with 78 additions and 210 deletions.
17 changes: 9 additions & 8 deletions components/platform_crypto/shave_trusted_boot/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,16 +39,17 @@ 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_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
.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

cn_proof_trusted_boot: $(ROOT_DIR)/trusted_boot.c
$(CN) --skip=parse_hex_str $<
cn_proof_firmware: $(ROOT_DIR)/firmware.c
$(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: cn_proof_firmware_sha cn_proof_firmware_xmss
cn_proof_firmware_sha: $(ROOT_DIR)/firmware.c
$(CN) $<

# many functions in header files that we are not currently concerned with are skipped
cn_proof_firmware_xmss: $(ROOT_DIR)/firmware.c
$(CN) -DUSE_XMSS -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
cn_proof_firmware_with_attest: $(ROOT_DIR)/firmware.c
$(CN) -DWITH_ATTEST $<
239 changes: 43 additions & 196 deletions components/platform_crypto/shave_trusted_boot/firmware.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,13 @@
#include "cn_array_utils.h"
#define memcpy(f,b,s) _memcpy(f,b,s)
#define memcmp(f,b,s) _memcmp(f,b,s)
#define malloc(x) _malloc(x)
#define free _free
#define realloc _realloc
#endif

//#define _Static_assert(...) extern int bogus
#if !defined(NO_XMSS)
#if defined(USE_XMSS)
#define union struct
#define __STDC_NO_ATOMICS__ 1
#include "endianness.h"
Expand All @@ -30,199 +31,19 @@
#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)
#if defined(USE_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);
take sbi = XmssSignatureBlobP(signature_blob);
ensures
take epko = Owned<XmssPublicKey>(exported_public_key);
take mo = Array_u8(msg, msg_size);
take sbo = Owned<XmssSignatureBlob>(signature_blob);
take sbo = XmssSignatureBlobP(signature_blob);
data_size(sbi) == data_size(sbo);
$*/
{
bool success = true;
Expand Down Expand Up @@ -253,20 +74,22 @@ static bool xmss_verify_signature(XmssPublicKey *exported_public_key, uint8_t *m

typedef unsigned char byte;

#ifdef USE_XMSS
#define MEASURE_SIZE (XMSS_SIGNATURE_BLOB_SIZE(XMSS_PARAM_SHA2_10_256)-sizeof(size_t))
#else
#define MEASURE_SIZE (32)
#endif
/*$ function (u64) MEASURE_SIZE() $*/
static
uint64_t c_MEASURE_SIZE() /*$ cn_function MEASURE_SIZE; $*/ { return MEASURE_SIZE; }

#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
#if defined(USE_XMSS)
static XmssPublicKey public_key;
static XmssSignatureBlob xmss_signature;
#else
static bool public_key;
#endif
#endif

Expand Down Expand Up @@ -297,7 +120,6 @@ int reset(void *start_address,
/*$ 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());
Expand Down Expand Up @@ -330,7 +152,36 @@ int reset(void *start_address,
size_t region_size = (e < s) ? 0 : (e - s);
#endif

#if defined(NO_XMSS)
#if defined(USE_XMSS)
if (expected_measure == NULL) {
return NOT_ALLOWED;
}

_Static_assert(XMSS_SIGNATURE_BLOB_SIZE(XMSS_PARAM_SHA2_10_256) == (MEASURE_SIZE+sizeof(size_t)), "MEASURE_SIZE is big enough");
size_t blob_size = XMSS_SIGNATURE_BLOB_SIZE(XMSS_PARAM_SHA2_10_256);
XmssSignatureBlob *sig = malloc(blob_size);
if (!sig) {
return NOT_ALLOWED;
}

void *sig_data_ = &sig->data;
/*$ apply SplitAt_Block_u8(sig, blob_size, 0u64, sizeof<size_t>); $*/
/*$ apply ViewShift_Block_u8(sig, sig_data_, sizeof<size_t>, blob_size-sizeof<size_t>); $*/
/*$ from_bytes Block<size_t>(member_shift<XmssSignatureBlob>(sig, data_size)); $*/
sig->data_size = MEASURE_SIZE;
memcpy(sig_data_, expected_measure_, MEASURE_SIZE);
if (!xmss_verify_signature(&public_key, start_address, region_size, sig)) {
/*$ to_bytes Block<size_t>(member_shift<XmssSignatureBlob>(sig, data_size)); $*/
/*$ apply UnViewShift_Owned_u8(sig, sig_data_, sizeof<size_t>, blob_size-sizeof<size_t>); $*/
/*$ apply UnSplitAt_Block_u8(sig, blob_size, 0u64, sizeof<size_t>); $*/
free(sig);
return HASH_MISMATCH;
}
/*$ to_bytes Block<size_t>(member_shift<XmssSignatureBlob>(sig, data_size)); $*/
/*$ apply UnViewShift_Block_u8(sig, sig_data_, sizeof<size_t>, blob_size-sizeof<size_t>); $*/
/*$ apply UnSplitAt_Block_u8(sig, blob_size, 0u64, sizeof<size_t>); $*/
free(sig);
#else
// apply SHA-256 to region
SHA256((byte *)start_address,region_size,&last_measure[0]);

Expand All @@ -339,10 +190,6 @@ 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;
Expand Down
32 changes: 26 additions & 6 deletions components/platform_crypto/shave_trusted_boot/xmss-library/include/structures.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -211,6 +211,28 @@ typedef struct XmssSignatureBlob {
uint8_t data[1];
} XmssSignatureBlob;

/*$
datatype XmssSignatureBlobT {
XmssSigBlobF {size_t data_size, map<u64,u8> data}
}
predicate (datatype XmssSignatureBlobT) XmssSignatureBlobP(pointer p)
{
take sz = Owned<size_t>(member_shift<XmssSignatureBlob>(p, data_size));
assert(sz >= 0u64);
take cont = Array_u8(member_shift<XmssSignatureBlob>(p, data), sz);
return XmssSigBlobF { data_size: sz, data: cont };
}
// No dot notation for datatype member access
function (size_t) data_size(datatype XmssSignatureBlobT a)
{
match a {
XmssSigBlobF {data_size: p, data: q} => {
p
}
}
}
$*/

/**
* @brief
* Provide access to an XmssSignatureBlob's data as a structured type.
Expand All @@ -221,12 +243,11 @@ typedef struct XmssSignatureBlob {
static inline XmssSignature *xmss_get_signature_struct(const XmssSignatureBlob *const signature)
/*$
requires
take si = Owned<XmssSignatureBlob>(signature);
take si = XmssSignatureBlobP(signature);
ensures
take so = Owned<XmssSignature>(return);
take sz = Owned<size_t>(member_shift<XmssSignatureBlob>(signature, data_size));
sz == si.data_size;
// TODO there is more to this structure, it has an included flex array
data_size(si) == sz;
$*/
{
if (signature == NULL) {
Expand All @@ -240,10 +261,9 @@ lemma Unxmss_get_signature_struct(pointer blob, pointer sig)
requires
take so = Owned<XmssSignature>(sig);
take sz = Owned<size_t>(member_shift<XmssSignatureBlob>(blob, data_size));
// TODO there is more to this structure, it has an included flex array
ensures
take si = Owned<XmssSignatureBlob>(blob);
//sz == si.data_size;
take si = XmssSignatureBlobP(blob);
sz == data_size(si);
$*/

Expand Down

0 comments on commit 9217268

Please sign in to comment.