mkm: make cn test work for most of the mkm fns

GaloisInc · Dec 31, 2024 · c520554 · c520554
1 parent 6a59c43
commit c520554
Show file tree

Hide file tree

Showing 5 changed files with 116 additions and 34 deletions.
diff --git a/components/mission_key_management/client.c b/components/mission_key_management/client.c
@@ -6,36 +6,41 @@
 #include <string.h>
 #include <stdint.h>
 
-#ifndef CN_ENV
-# include <sys/epoll.h>
-#endif
-
 # include <sys/socket.h>
 # include <unistd.h>
 # include <stdio.h>
 
-#ifdef CN_ENV
-# include <sys/types.h>
-#endif 
-
 //SYSTEM_HEADERS
 
-#include "client.h"
+# include "client.h" 
 
-#ifdef CN_ENV
-# include "cn_memory.h"
+#if ! defined(CN_ENV)
+# include <sys/types.h>
+# include <sys/epoll.h>
+#else  
 # include "cn_stubs.h"
+#endif
+
+#if defined(CN_ENV) && ! defined(CN_TEST) 
+# include "cn_memory.h"
 # include "cn_array_utils.h"
 #endif 
 
+#if defined(CN_TEST) 
+# define NULL ((void *)0)
+#endif 
+
 /* TODO list: 
- [ ] Fix more of the TODOs
-    [x] Move the Alloc into ClientPred 
+ [ ] Proof: 
+    [x] Move the Alloc into ClientPred() 
     [ ] make the key access table into a global? Not sure if this will work 
     [ ] ... 
- [ ] Run the test generator on the code 
+ [ ] Test generation: 
     [x] Get the generator working 
-    [ ] Get one function working 
+    [x] Get one function working 
+    [x] Get more functions working 
+    [ ] Fix memory handling functions 
+    [ ] Fix policy functions 
 */
 
 uint32_t client_state_epoll_events(enum client_state state) 
@@ -64,6 +69,8 @@ requires ValidState( state );
     }
 }
 
+// TODO: Support memory functions 
+#if ! defined(CN_TEST) 
 struct client* client_new(int fd) 
 // TODO: Specification doesn't handle the case where malloc fails 
 /*$ 
@@ -105,14 +112,14 @@ requires take Client_in = ClientPred(c);
         // Keep going.  On Linux, `close` always closes the file descriptor,
         // but may report I/O errors afterward.
     }
-#ifdef CN_ENV
+#if defined(CN_ENV)
     // TODO: Ghost function returning ownership of the key pointer 
     key_release(c->key); 
 #endif
     /*$ to_bytes Block<struct client>(c); $*/
     free(c);
 }
-
+#endif 
 
 uint8_t* client_read_buffer(struct client* c) 
 /*$ 
@@ -254,14 +261,18 @@ 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)");
@@ -297,6 +308,7 @@ 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); $*/
 
@@ -306,9 +318,14 @@ 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)");
@@ -332,7 +349,7 @@ ensures
     // TODO: more compact notation? 
     Client_out.fd == Client_in.fd; 
     Client_out.challenge == Client_in.challenge; 
-    // ptr_eq(Client_out.key, Client_in.key); // <-- unnecessary 
+    ptr_eq(Client_out.key, Client_in.key); 
     Client_out.key_id == Client_in.key_id; 
     Client_out.pos == 0u8; 
     Client_out.state == new_state; 
@@ -343,8 +360,10 @@ ensures
 }
 
 enum client_event_result client_event(struct client* c, uint32_t events) 
+#if ! defined(CN_TEST) 
+/*$ accesses __stderr; $*/ 
+#endif 
 /*$ 
-accesses __stderr;
 requires 
     take Client_in = ClientPred(c); 
     ! is_null(Client_in.key); // TODO: should depend on state machine state 
@@ -406,12 +425,15 @@ requires
             break;
 
         case CS_RECV_RESPONSE:
-#ifdef CN_ENV
+#if defined(CN_ENV)
             // TODO: ghost code - give back the old key 
             key_release(c->key); // Should be removed eventually 
 #endif 
+#if ! defined(CN_TEST)
+            // TODO: write a mock for this function 
             c->key = policy_match(c->key_id, c->challenge,
                     c->response, c->response + MEASURE_SIZE);
+#endif 
             if (c->key == NULL) {
                 // No matching key was found for this request.
                 fprintf(stderr, "client %d: error: bad request for key %u\n", c->fd, c->key_id[0]);

diff --git a/components/mission_key_management/client.h b/components/mission_key_management/client.h
@@ -32,7 +32,11 @@ struct client {
     // to depends on the current state.  For the chosen buffer, `buf[i]` is
     // initialized only within the range `0 <= i < pos`.
     uint8_t pos;
+#if ! defined(CN_TEST)
     enum client_state state;
+#else 
+    unsigned int state; 
+#endif 
 };
 
 enum client_event_result {
@@ -63,6 +67,8 @@ int client_epoll_ctl(struct client* c, int epfd, int op);
 // netx to update the epoll event mask.
 enum client_event_result client_event(struct client* c, uint32_t events);
 
+// Testing doesn't handle `default` properly 
+#if ! defined(CN_TEST) 
 // Either the key is in memory and owned, or the pointer is null 
 /*$ 
 predicate (map<u64,u8>) KeyPred (pointer p) 
@@ -75,6 +81,20 @@ predicate (map<u64,u8>) KeyPred (pointer p)
     }
 }
 $*/ 
+#else
+/*$ 
+predicate (boolean) KeyPred (pointer p) 
+{
+    if (! is_null(p)) { 
+        take K = each(u64 i; i < 32u64) {Owned<uint8_t>(array_shift<uint8_t>(p,i))}; 
+        return true; 
+    } else {
+        return false; 
+    }
+}
+$*/ 
+#endif 
+
 
 // Pure predicate representing valid states of `enum client_state`. 
 // CN could easily generate this automatically (see #796) 
@@ -90,21 +110,21 @@ function (boolean) ValidState (u32 state) {
 
 // Wrapper predicate for the allocation record. We distinguish between cases
 // because `cn test` doesn't handle Alloc() yet
-#ifndef CN_TEST
+#if ! defined(CN_TEST)
 /*$
-predicate ({u64 base,u64 size}) ClientAlloc (pointer p)
+predicate (boolean) ClientAlloc (pointer p)
 {
     take Log = Alloc(p);
     assert ( Log.base == (u64)p );
     assert ( Log.size == sizeof<struct client> );
-    return Log; 
+    return true; 
 } 
 $*/
 #else 
 /*$
-predicate ({u64 base,u64 size}) ClientAlloc (pointer p)
+predicate (boolean) ClientAlloc (pointer p)
 {
-    return default< {u64 base,u64 size} >; 
+    return true; 
 } 
 $*/
 #endif

diff --git a/components/mission_key_management/cn_stubs.h b/components/mission_key_management/cn_stubs.h
@@ -5,7 +5,10 @@
 
 // Cerberus puts some POSIX headers under the `posix/` directory.
 #include "policy.h"
+
+#if ! defined(CN_TEST) // Dumb hack to avoid double-include 
 #include "client.h"
+#endif 
 
 // From `sys/epoll.h`
 #define EPOLLIN 1
@@ -16,6 +19,7 @@
 
 // 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
 
@@ -31,6 +35,15 @@ static uint64_t c_HMAC_SIZE() /*$ cn_function HMAC_SIZE; $*/ { return HMAC_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],
@@ -45,13 +58,18 @@ ensures
 // 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. 
-void key_release (const uint8_t *key); 
-/*$ spec key_release(pointer key); 
+void _key_release (const uint8_t *key); 
+/*$ spec _key_release(pointer key); 
 requires 
     take Key_in = KeyPred(key);
 ensures 
     true; 
 $*/
+#if ! defined(CN_TEST) 
+#define key_release(k) _key_release(k)
+#else 
+#define key_release(k) 0 
+#endif 
 
 // From `stdio.h`
 
@@ -72,12 +90,12 @@ void perror(const char *msg);
 #else
 # define perror(...) 0
 #endif
+
 /*$ spec exit(i32 v);
     requires true;
     ensures true;
 $*/
 
-
 // From `unistd.h`
 
 int _close(int fildes);
@@ -86,7 +104,9 @@ spec _close(i32 fildes);
 requires true;
 ensures true;
 $*/
+#if ! defined(CN_TEST)
 #define close(x) _close(x)
+#endif 
 
 ssize_t _read_uint8_t(int fd, void *buf, size_t count);
 /*$ 
@@ -98,7 +118,9 @@ ensures
     buf_out == buf_in; 
     return >= -1i64 && return <= (i64)count;
 $*/
+#if ! defined(CN_TEST) 
 #define read(f,b,c) _read_uint8_t(f,b,c)
+#endif 
 
 ssize_t _write_uint8_t(int fd, const void *buf, size_t count);
 /*$ 
@@ -110,17 +132,29 @@ ensures
     buf_in == buf_out;
     return >= -1i64 && return < (i64)count;
 $*/
+#if ! defined(CN_TEST) 
 #define write(f,b,c) _write_uint8_t(f,b,c)
+#endif 
 
 int _shutdown(int fildes, int how);
 /*$ spec _shutdown(i32 fildes, i32 how);
     requires true;
     ensures true;
 $*/
+#if ! defined(CN_TEST) 
 #define shutdown(x,h) _shutdown(x,h)
+#else 
+#define shutdown(...) 0 
+#endif 
 
 // Defined in ../../components/include/cn_memory.h
+#if ! defined(CN_TEST)
 #define memcpy(d,s,n) _memcpy(d,s,n)
 #define memcmp(s1,s2,n) _memcmp(s1,s2,n)
 #define malloc(x) _malloc(x)
 #define free(x) _free(x)
+#endif 
+
+#ifdef CN_TEST 
+#define fprintf(...) 0 
+#endif 
diff --git a/components/mission_key_management/process-cn-test.sh b/components/mission_key_management/process-cn-test.sh
@@ -18,7 +18,7 @@ fi
 
 INPUT_FILE="$1"
 OUTBASE="${INPUT_FILE%.c}"
-DEFAULT_OUTPUT="${OUTBASE}-out.c"
+DEFAULT_OUTPUT="${OUTBASE}-gen.c"
 
 # If user provided the second argument, use it; otherwise use our default
 OUTPUT_FILE="${2:-$DEFAULT_OUTPUT}"
@@ -52,10 +52,9 @@ GCC_FLAGS=(
 # echo gcc "${GCC_FLAGS[@]}" "${TMP_DIR}/split_1" -o "${TMP_DIR}/split_1_out.c"
 # echo ""
 
-# echo "Include tree:" 
 gcc "${GCC_FLAGS[@]}" "${TMP_DIR}/split_1" -o "${TMP_DIR}/split_1_out.c"
 
 # 3. Concatenate the first chunk and preprocessed second chunk
 cat "${TMP_DIR}/split_0" "${TMP_DIR}/split_1_out.c" > "$OUTPUT_FILE"
 
-echo "\nDone. Merged output is in: $OUTPUT_FILE"
+echo "Done. Merged output is in: $OUTPUT_FILE"