From a55fcb5a66d4856de0e3564d9d5955ac9c4f89b5 Mon Sep 17 00:00:00 2001 From: septract Date: Sun, 5 Jan 2025 11:38:55 -0800 Subject: [PATCH] mkm: use `default` in definitions (depends on cerberus PR #814) --- components/mission_key_management/client.c | 19 +++------- components/mission_key_management/client.h | 7 ++-- components/mission_key_management/cn_stubs.h | 39 +++++++------------- components/mission_key_management/policy.h | 26 +++++++++++++ 4 files changed, 47 insertions(+), 44 deletions(-) diff --git a/components/mission_key_management/client.c b/components/mission_key_management/client.c index c67bba7..f9e4426 100644 --- a/components/mission_key_management/client.c +++ b/components/mission_key_management/client.c @@ -6,9 +6,9 @@ #include #include -# include -# include -# include +#include +#include +#include //SYSTEM_HEADERS // ^^^ magic string used during preprocessing - do not move / remove @@ -20,13 +20,12 @@ # include #else # include "cn_stubs.h" +# include "cn_array_utils.h" #endif +// TODO `Alloc` construct not supported by `cn test` #if defined(CN_ENV) && ! defined(CN_TEST) -// TODO These don't affect `cn test` but can't be included as they use -// the `default` construct, which isn't currently supported # include "cn_memory.h" -# include "cn_array_utils.h" #endif #if defined(CN_TEST) @@ -280,18 +279,14 @@ ensures return RES_DONE; } -#if ! defined(CN_TEST) // TODO Mysterious why this particular case split is needed /*$ split_case(Client_in.state == (u32) CS_RECV_KEY_ID); $*/ /*$ apply SplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/ /*$ apply ViewShift_Owned_u8(buf, buf + pos, pos, buf_size - pos ); $*/ -#endif int ret = read(c->fd, buf + c->pos, buf_size - (uint64_t) c->pos); -#if ! defined(CN_TEST) /*$ apply UnViewShift_Owned_u8(buf, buf + pos, pos, buf_size - pos ); $*/ /*$ apply UnSplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/ -#endif if (ret < 0) { perror("read (client_read)"); @@ -326,7 +321,6 @@ ensures return RES_DONE; } -#if ! defined(CN_TEST) // TODO Mysterious why this particular case split is needed /*$ split_case(Client_in.state == (u32) CS_SEND_CHALLENGE); $*/ @@ -336,14 +330,11 @@ ensures /*$ apply SplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/ /*$ apply ViewShift_Owned_u8(buf, buf + pos, pos, buf_size - pos ); $*/ -#endif int ret = write(c->fd, buf + c->pos, buf_size - (uint64_t) c->pos); -#if ! defined(CN_TEST) /*$ apply UnViewShift_Owned_u8(buf, buf + pos, pos, buf_size - pos ); $*/ /*$ apply UnSplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/ -#endif if (ret < 0) { perror("write (client_write)"); diff --git a/components/mission_key_management/client.h b/components/mission_key_management/client.h index 2ccd486..7d9944a 100644 --- a/components/mission_key_management/client.h +++ b/components/mission_key_management/client.h @@ -69,14 +69,13 @@ enum client_event_result client_event(struct client* c, uint32_t events); // Either the key is in memory and owned, or the pointer is null /*$ -predicate (boolean) KeyPred (pointer p) +predicate (map) KeyPred (pointer p) { if (! is_null(p)) { take K = each(u64 i; i < KEY_SIZE()) {Owned(array_shift(p,i))}; - // TODO: should use `default` here, but it's not supported by `cn test` yet - return true; + return K; } else { - return false; + return default< map >; } } $*/ diff --git a/components/mission_key_management/cn_stubs.h b/components/mission_key_management/cn_stubs.h index 060908b..17025ea 100644 --- a/components/mission_key_management/cn_stubs.h +++ b/components/mission_key_management/cn_stubs.h @@ -32,32 +32,6 @@ void cn_free_sized(void *ptr, unsigned long size); // From `policy.h` -#if ! defined(CN_TEST) -// This is the idiomatic CN lifting of macro constants, per -// https://rems-project.github.io/cn-tutorial/getting-started/style-guide/#constants - -/*$ function (u64) KEY_ID_SIZE () $*/ -static uint64_t c_KEY_ID_SIZE() /*$ cn_function KEY_ID_SIZE; $*/ { return KEY_ID_SIZE; } -/*$ function (u64) NONCE_SIZE () $*/ -static uint64_t c_NONCE_SIZE() /*$ cn_function NONCE_SIZE; $*/ { return NONCE_SIZE; } -/*$ function (u64) MEASURE_SIZE () $*/ -static uint64_t c_MEASURE_SIZE() /*$ cn_function MEASURE_SIZE; $*/ { return MEASURE_SIZE; } -/*$ function (u64) HMAC_SIZE () $*/ -static uint64_t c_HMAC_SIZE() /*$ cn_function HMAC_SIZE; $*/ { return HMAC_SIZE; } -/*$ function (u64) HMAC_KEY_SIZE () $*/ -static uint64_t c_HMAC_KEY_SIZE() /*$ cn_function HMAC_KEY_SIZE; $*/ { return HMAC_KEY_SIZE; } -/*$ function (u64) KEY_SIZE () $*/ -static uint64_t c_KEY_SIZE() /*$ cn_function KEY_SIZE; $*/ { return KEY_SIZE; } -#else -// TODO: Have to hardcode the values as CN test doesn't support cn_function :( -/*$ function (u64) KEY_ID_SIZE () { 1u64} $*/ -/*$ function (u64) NONCE_SIZE () {16u64} $*/ -/*$ function (u64) MEASURE_SIZE () {32u64} $*/ -/*$ function (u64) HMAC_SIZE () {32u64} $*/ -/*$ function (u64) HMAC_KEY_SIZE () {32u64} $*/ -/*$ function (u64) KEY_SIZE () {32u64} $*/ -#endif - // Non-deterministically return a pointer to a key, or NULL const uint8_t* _policy_match(uint8_t key_id[KEY_ID_SIZE], uint8_t nonce[NONCE_SIZE], uint8_t measure[MEASURE_SIZE], uint8_t hmac[HMAC_SIZE]); @@ -74,6 +48,19 @@ ensures #define policy_match(...) cn_malloc(KEY_SIZE * sizeof(const uint8_t)) #endif +// Add an entry to the policy table. Returns 0 on success and -1 on failure. +int _policy_add( + const uint8_t key_id[KEY_ID_SIZE], + const uint8_t measure[MEASURE_SIZE], + const uint8_t key[KEY_SIZE]); +/*$ spec _policy_add(pointer key_id, pointer measure, pointer key); +requires + true; +ensures + return == 0i32 || return == -1i32; +$*/ +#define policy_add(k,m,h) _policy_add(k,m,h) + // Ghost function which releases the memory representing a key. Implicitly, this // is returning ownership of the memory to whatever internal state manages the // key list. diff --git a/components/mission_key_management/policy.h b/components/mission_key_management/policy.h index 71ee6af..9b93108 100644 --- a/components/mission_key_management/policy.h +++ b/components/mission_key_management/policy.h @@ -11,6 +11,32 @@ #define HMAC_KEY_SIZE 32 #define KEY_SIZE 32 +#if ! defined(CN_TEST) +// This is the idiomatic CN lifting of macro constants, per +// https://rems-project.github.io/cn-tutorial/getting-started/style-guide/#constants + +/*$ function (u64) KEY_ID_SIZE () $*/ +static uint64_t c_KEY_ID_SIZE() /*$ cn_function KEY_ID_SIZE; $*/ { return KEY_ID_SIZE; } +/*$ function (u64) NONCE_SIZE () $*/ +static uint64_t c_NONCE_SIZE() /*$ cn_function NONCE_SIZE; $*/ { return NONCE_SIZE; } +/*$ function (u64) MEASURE_SIZE () $*/ +static uint64_t c_MEASURE_SIZE() /*$ cn_function MEASURE_SIZE; $*/ { return MEASURE_SIZE; } +/*$ function (u64) HMAC_SIZE () $*/ +static uint64_t c_HMAC_SIZE() /*$ cn_function HMAC_SIZE; $*/ { return HMAC_SIZE; } +/*$ function (u64) HMAC_KEY_SIZE () $*/ +static uint64_t c_HMAC_KEY_SIZE() /*$ cn_function HMAC_KEY_SIZE; $*/ { return HMAC_KEY_SIZE; } +/*$ function (u64) KEY_SIZE () $*/ +static uint64_t c_KEY_SIZE() /*$ cn_function KEY_SIZE; $*/ { return KEY_SIZE; } +#else +// TODO: Have to hardcode the values as CN test doesn't support cn_function :( +/*$ function (u64) KEY_ID_SIZE () { 1u64} $*/ +/*$ function (u64) NONCE_SIZE () {16u64} $*/ +/*$ function (u64) MEASURE_SIZE () {32u64} $*/ +/*$ function (u64) HMAC_SIZE () {32u64} $*/ +/*$ function (u64) HMAC_KEY_SIZE () {32u64} $*/ +/*$ function (u64) KEY_SIZE () {32u64} $*/ +#endif + #define ALIGN_AS_POINTER _Alignas(_Alignof(void*)) // A single entry in the MKM policy. Each entry consists of a set of criteria