mkm: use default in definitions (depends on cerberus PR #814)

components/mission_key_management/client.c

@@ -6,9 +6,9 @@
 #include <string.h>
 #include <stdint.h>
 
-# include <sys/socket.h>
-# include <unistd.h>
-# include <stdio.h>
+#include <sys/socket.h>
+#include <unistd.h>
+#include <stdio.h>
 
 //SYSTEM_HEADERS
 // ^^^ magic string used during preprocessing - do not move / remove 
@@ -20,13 +20,12 @@
 # include <sys/epoll.h>
 #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)");

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<u64, u8>) KeyPred (pointer p) 
 {
     if (! is_null(p)) { 
         take K = each(u64 i; i < KEY_SIZE()) {Owned<uint8_t>(array_shift<uint8_t>(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<u64, u8> >; 
     }
 }
 $*/ 

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. 

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