From 6a59c43b7bdd19ddaa426b75f2064e4d75e2f8a4 Mon Sep 17 00:00:00 2001 From: septract Date: Fri, 27 Dec 2024 17:27:19 -0800 Subject: [PATCH] mkm: minor proof cleanup --- components/mission_key_management/client.c | 32 +++++++++++-------- components/mission_key_management/client.h | 23 ++++++++++++- .../mission_key_management/process-cn-test.sh | 14 ++++---- 3 files changed, 46 insertions(+), 23 deletions(-) diff --git a/components/mission_key_management/client.c b/components/mission_key_management/client.c index 5d7bc3a..d11874f 100644 --- a/components/mission_key_management/client.c +++ b/components/mission_key_management/client.c @@ -29,9 +29,13 @@ #endif /* TODO list: - - Fix some of the TODOs - - Run the test generator on the code - - make the key access table into a global?? + [ ] Fix more of the TODOs + [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 + [x] Get the generator working + [ ] Get one function working */ uint32_t client_state_epoll_events(enum client_state state) @@ -51,9 +55,9 @@ requires ValidState( state ); case CS_DONE: return 0; - default:{ // TODO: block needed for assert() + default: { // NOTE: additional block needed for assert() // Prove this state is unreachable: - /*$ assert ( false ); $*/ + /*$ assert(false); $*/ // Unreachable return 0; } @@ -64,7 +68,6 @@ struct client* client_new(int fd) // TODO: Specification doesn't handle the case where malloc fails /*$ ensures take Client_out = ClientPred(return); - take log = Alloc(return); Client_out.fd == fd; ((i32) Client_out.state) == CS_RECV_KEY_ID; $*/ @@ -87,11 +90,7 @@ ensures take Client_out = ClientPred(return); void client_delete(struct client* c) /*$ -requires - take Client_in = ClientPred(c); - take log = Alloc(c); - log.base == (u64)c; - log.size == sizeof; +requires take Client_in = ClientPred(c); $*/ { int ret = shutdown(c->fd, SHUT_RDWR); @@ -150,6 +149,7 @@ ensures take Client_out = ClientPred(c); ptr_eq( return, member_shift(c, challenge) ) } else { if (((i32) Client_in.state) == CS_SEND_KEY) { // TODO: very confusing distinction from the previous case! + // Caused by the fact challenge is an array, and key is a value ptr_eq( return, Client_in.key ) } else { is_null(return) @@ -196,7 +196,7 @@ ensures take Client_out = ClientPred(c); case CS_DONE: return 0; - default: { // TODO: block needed for assert() + default: { // NOTE: additional block needed for assert() // Prove this state is unreachable: /*$ assert(false); $*/ // Unreachable @@ -300,7 +300,8 @@ ensures // TODO: Mysterious why this particular case split is needed /*$ split_case(Client_in.state == (u32) CS_SEND_CHALLENGE); $*/ - // TODO: Why is this is needed for write() but not read() ? + // TODO: Why is this is needed for write() but not read() ? + // I think this is because of the particular path conditions /*$ extract Owned, pos; $*/ /*$ apply SplitAt_Owned_u8(buf, buf_size, pos, buf_size - pos ); $*/ @@ -386,10 +387,13 @@ requires // The async operation for the current state is finished. We can now // transition to the next state. switch (c->state) { - case CS_RECV_KEY_ID: { // <-- TODO: block needed for var declaration + case CS_RECV_KEY_ID: { // NOTE: additional block needed for declaration + // TODO: We can't call memcpy with a string argument because CN // doesn't support that properly yet // memcpy(c->challenge, "random challenge", NONCE_SIZE); + + // Instead, declare the string as a variable: uint8_t challenge[NONCE_SIZE] = "random challenge"; memcpy(c->challenge, challenge, NONCE_SIZE); diff --git a/components/mission_key_management/client.h b/components/mission_key_management/client.h index 5167bf8..9f4d18a 100644 --- a/components/mission_key_management/client.h +++ b/components/mission_key_management/client.h @@ -88,12 +88,33 @@ 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 +/*$ +predicate ({u64 base,u64 size}) ClientAlloc (pointer p) +{ + take Log = Alloc(p); + assert ( Log.base == (u64)p ); + assert ( Log.size == sizeof ); + return Log; +} +$*/ +#else +/*$ +predicate ({u64 base,u64 size}) ClientAlloc (pointer p) +{ + return default< {u64 base,u64 size} >; +} +$*/ +#endif + // Predicate representing a valid client object /*$ -// TODO: wrap up the alloc() in the ClientPred predicate? predicate (struct client) ClientPred (pointer p) { take C = Owned(p); + take Log = ClientAlloc(p); assert ( ValidState(C.state) ) ; take K = KeyPred(C.key); // Discard the key return C; diff --git a/components/mission_key_management/process-cn-test.sh b/components/mission_key_management/process-cn-test.sh index 256c818..315bf70 100755 --- a/components/mission_key_management/process-cn-test.sh +++ b/components/mission_key_management/process-cn-test.sh @@ -38,23 +38,21 @@ eval "$(opam env)" # gcc flags, stored in an array for robustness GCC_FLAGS=( - "-H" # Print the include tree - useful for debugging + # "-H" # Print the include tree - useful for debugging "-E" "-P" "-CC" "-x" "c" - # TODO: revisit the line below. This is needed when running `cn verify`, but I - # think is redundant here: - # "--include=${ROOT_DIR}/../include/wars.h" "-I${ROOT_DIR}/../include" "-I." "-I${OPAM_SWITCH_PREFIX}/lib/cerberus/runtime/libc/include/posix" "-DCN_ENV" "-DWAR_CN_309" + "-DCN_TEST" # A few things need to be modified for cn-test ) # Print the exact command for debug purposes -echo "Running gcc command:" -echo gcc "${GCC_FLAGS[@]}" "${TMP_DIR}/split_1" -o "${TMP_DIR}/split_1_out.c" -echo "" +# echo "Running gcc command:" +# echo gcc "${GCC_FLAGS[@]}" "${TMP_DIR}/split_1" -o "${TMP_DIR}/split_1_out.c" +# echo "" -echo "Include tree:" +# 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