From 042f28119c8b49796a240e1535dc70a45ef664f4 Mon Sep 17 00:00:00 2001 From: Mike Dodds Date: Thu, 28 Nov 2024 13:55:49 -0800 Subject: [PATCH] mkm: verified memory safety of remaining client fns --- .../mission_key_management/client-reduced.c | 179 ++++++++++-------- components/mission_key_management/cn_stubs.h | 104 +++++++--- components/mission_key_management/mkm.h | 7 + 3 files changed, 185 insertions(+), 105 deletions(-) diff --git a/components/mission_key_management/client-reduced.c b/components/mission_key_management/client-reduced.c index acf8f99a..12368331 100644 --- a/components/mission_key_management/client-reduced.c +++ b/components/mission_key_management/client-reduced.c @@ -38,15 +38,15 @@ uint32_t client_state_epoll_events(enum client_state state) { struct client* client_new(int fd) /*$ -trusted; +// TODO: Doesn't handle the case where malloc fails ensures take Client_out = Owned(return); Client_out.fd == fd; Client_out.pos == 0u8; - // TODO: can't refer to the enum in a specification - // Client_out.state == C_RECV_KEY_ID; + ((i32) Client_out.state) == CS_RECV_KEY_ID; $*/ { + // TODO: malloc spec assumes alloction always succeeds struct client* c = malloc(sizeof(struct client)); if (c == NULL) { perror("malloc (client_new)"); @@ -60,10 +60,8 @@ ensures void client_delete(struct client* c) /*$ -trusted; requires take Client_in = Owned(c); -// TODO: handle close / perror properly $*/ { int ret = close(c->fd); @@ -115,7 +113,7 @@ ensures ptr_eq( return, member_shift(c, challenge) ) } else { if (((i32) Client_in.state) == CS_SEND_KEY) { - // TODO: fix this case + // TODO: fix the mission_key case is_null(return) } else { is_null(return) @@ -127,9 +125,9 @@ ensures return c->challenge; case CS_SEND_KEY: { // /*$ extract Owned, 0u64; $*/ - // return get_mission_key(c->key_id[0]); - // TODO: fix the mission keys stuff - return NULL; + const uint8_t* ret = NULL; // get_mission_key(c->key_id[0]); + return ret; + // TODO: Fix mission key stuff } default: return NULL; @@ -143,7 +141,8 @@ requires ensures take Client_out = Owned(c); Client_out == Client_in; - // TODO: have to concretize the array sizes + // TODO: ideally we'd get the field sizes implicitly. + // Here we have to write them as concrete values return == ( if (((i32) Client_in.state) == CS_RECV_KEY_ID) { 1u64 @@ -170,7 +169,8 @@ ensures return 0; default: - // Unreachable + // Prove that this state is unreachable: + /*@ assert false; @*/ return 0; } } @@ -216,14 +216,15 @@ ensures return RES_DONE; } + // TODO: unclear why this works??? /*$ split_case(Client_in.state == (u32) CS_RECV_KEY_ID); $*/ + // TODO: array subsetting isn't handled. Probably need a lemma here int ret = read(c->fd, buf, buf_size); // int ret = read(c->fd, buf + c->pos, buf_size - (size_t) c->pos); if (ret < 0) { - // TODO: commented out perror, should give it a spec - // perror("read (client_read)"); + perror("read (client_read)"); return RES_ERROR; } else if (ret == 0) { return RES_EOF; @@ -253,13 +254,12 @@ ensures return RES_DONE; } - // TODO: array subsetting isn't handled. Probably need a lemma here + // TODO: Fix array subsetting. Probably need a lemma here int ret = write(c->fd, buf, buf_size); // int ret = write(c->fd, buf + c->pos, buf_size - c->pos); if (ret < 0) { - // TODO: re-enable this - // perror("write (client_write)"); + perror("write (client_write)"); return RES_ERROR; } else if (ret == 0) { return RES_EOF; @@ -290,70 +290,83 @@ ensures c->pos = 0; } -// enum client_event_result client_event(struct client* c, uint32_t events) { -// if (events & EPOLLIN) { -// enum client_event_result result = client_read(c); -// if (result != RES_DONE) { -// return result; -// } -// } -// if (events & EPOLLOUT) { -// enum client_event_result result = client_write(c); -// if (result != RES_DONE) { -// return result; -// } -// } - -// if (c->pos < client_buffer_size(c)) { -// // Async read/write operation isn't yet finished. -// // -// // This should be unreachable. `client_event` should only be called -// // when progress can be made on a current async read or write -// // operation, and the call to `client_read`/`client_write` above will -// // return `RES_PENDING` (causing `client_event` to return early) if the -// // operation isn't finished. -// return RES_PENDING; -// } - -// // 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: -// memcpy(c->challenge, "This challenge is totally random", 32); -// client_change_state(c, CS_SEND_CHALLENGE); -// break; - -// case CS_SEND_CHALLENGE: -// client_change_state(c, CS_RECV_RESPONSE); -// break; - -// case CS_RECV_RESPONSE: -// { -// // TODO: properly validate the response -// int resp_ok = memcmp(c->challenge, c->response, 32) == 0; -// if (!resp_ok) { -// fprintf(stderr, "client %d: error: bad response\n", c->fd); -// return RES_ERROR; -// } -// uint8_t key_id = c->key_id[0]; -// if (key_id >= NUM_SECRET_KEYS) { -// fprintf(stderr, "client %d: error: bad request for key %u\n", c->fd, key_id); -// return RES_ERROR; -// } -// client_change_state(c, CS_SEND_KEY); -// fprintf(stderr, "client %d: sending key %u\n", c->fd, key_id); -// } -// break; - -// case CS_SEND_KEY: -// client_change_state(c, CS_DONE); -// break; - -// case CS_DONE: -// // No-op. This connection is finished, and the main loop should -// // disconnect. -// break; -// } - -// return RES_DONE; -// } +enum client_event_result client_event(struct client* c, uint32_t events) +/*$ +requires + take Client_in = Owned(c); +ensures + take Client_out = Owned(c); +$*/ +{ + if (events & EPOLLIN) { + enum client_event_result result = client_read(c); + if (result != RES_DONE) { + return result; + } + } + if (events & EPOLLOUT) { + enum client_event_result result = client_write(c); + if (result != RES_DONE) { + return result; + } + } + + if (c->pos < client_buffer_size(c)) { + // Async read/write operation isn't yet finished. + // + // This should be unreachable. `client_event` should only be called + // when progress can be made on a current async read or write + // operation, and the call to `client_read`/`client_write` above will + // return `RES_PENDING` (causing `client_event` to return early) if the + // operation isn't finished. + return RES_PENDING; + } + + // 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: note extra block needed for var declaration + // TODO: fix string argument nonsense here + // memcpy(c->challenge, "This challenge is totally random", 32); + uint8_t challenge[32] = "This challenge is totally random"; + memcpy(c->challenge, &challenge, 32); + client_change_state(c, CS_SEND_CHALLENGE); + break; + } + + case CS_SEND_CHALLENGE: + client_change_state(c, CS_RECV_RESPONSE); + break; + + case CS_RECV_RESPONSE: + { + // TODO: properly validate the response + int resp_ok = memcmp(c->challenge, c->response, 32) == 0; + if (!resp_ok) { + fprintf(stderr, "client %d: error: bad response\n", c->fd); + return RES_ERROR; + } + /*$ extract Owned, 0u64; $*/ + uint8_t key_id = c->key_id[0]; + if (key_id >= NUM_SECRET_KEYS) { + fprintf(stderr, "client %d: error: bad request for key %u\n", c->fd, key_id); + return RES_ERROR; + } + client_change_state(c, CS_SEND_KEY); + fprintf(stderr, "client %d: sending key %u\n", c->fd, key_id); + } + break; + + case CS_SEND_KEY: + client_change_state(c, CS_DONE); + break; + + case CS_DONE: + // No-op. This connection is finished, and the main loop should + // disconnect. + break; + } + + return RES_DONE; +} diff --git a/components/mission_key_management/cn_stubs.h b/components/mission_key_management/cn_stubs.h index b2254f83..5578d263 100644 --- a/components/mission_key_management/cn_stubs.h +++ b/components/mission_key_management/cn_stubs.h @@ -2,7 +2,6 @@ // Provides substitutes for some declarations that CN has trouble with. - // Cerberus puts some POSIX headers under the `posix/` directory. #include @@ -18,10 +17,13 @@ // not possible to call this due to CN issue #309 // this spec isn't right but can't develop it at all without #309 void perror(const char *msg); -/*$ spec perror(pointer msg); - requires take mi = Owned(msg); - ensures take mo = Owned(msg); - mi == mo; +/*$ +spec perror(pointer msg); +requires + take mi = Owned(msg); +ensures + take mo = Owned(msg); + mi == mo; $*/ #else # define perror(...) 0 @@ -37,6 +39,7 @@ void perror(const char *msg); // From `unistd.h` +// // Old version, updated by MDD below // ssize_t _read(int fildes, void *buf, size_t n); // /*$ spec _read(i32 fildes, pointer buf, u64 n); // // accesses errno; @@ -51,34 +54,91 @@ void perror(const char *msg); // take bufb = each(u64 i; (return == -1i64) ? (0u64 <= i && i < n) : ((u64)return <= i && i < n)) {Block(array_shift(buf, i))}; // $*/ -ssize_t _read(int fildes, void *buf, size_t n); +ssize_t _read_uint8_t(int fildes, void *buf, size_t n); /*$ -spec _read(i32 fildes, pointer buf, u64 n); +spec _read_uint8_t(i32 fildes, pointer buf, u64 n); requires - take buf_in = - each (u64 i; i < n) { Owned(array_shift(buf, i))}; + take buf_in = each (u64 i; i < n) { Owned(array_shift(buf, i))}; ensures return >= -1i64 && return <= (i64)n; - take buf_out = - each (u64 i; i < n) { Owned(array_shift(buf, i))}; + take buf_out = each (u64 i; i < n) { Owned(array_shift(buf, i))}; $*/ -#define read(f,b,s) _read(f,b,s) +#define read(f,b,s) _read_uint8_t(f,b,s) int _close(int fildes); -/*$ spec _close(i32 fildes); - requires true; - ensures true; +/*$ +spec _close(i32 fildes); +requires true; +ensures true; $*/ #define close(x) _close(x) -ssize_t _write(int fildes, const void *buf, size_t nbyte); -/*$ spec _write(i32 fildes, pointer buf, u64 nbyte); - requires +ssize_t _write_uint8_t(int fildes, const void *buf, size_t nbyte); +/*$ +spec _write_uint8_t(i32 fildes, pointer buf, u64 nbyte); +requires ((i32)nbyte) >= 0i32; - take bufi = each(u64 i; i >= 0u64 && i < nbyte) {Owned(array_shift(buf,i))}; - ensures - take bufo = each(u64 i; i >= 0u64 && i < nbyte) {Owned(array_shift(buf,i))}; + take bufi = each(u64 i; i < nbyte) {Owned(array_shift(buf,i))}; +ensures + take bufo = each(u64 i; i < nbyte) {Owned(array_shift(buf,i))}; bufi == bufo; return >= -1i64 && return < (i64)nbyte; $*/ -#define write(f,b,s) _write(f,b,s) +#define write(f,b,s) _write_uint8_t(f,b,s) + +void *_memcpy_uint8_t(void *dest, const void *src, size_t nbyte); +/*$ +spec _memcpy_uint8_t(pointer dest, pointer src, u64 nbyte); +requires + ((i32)nbyte) >= 0i32; + take src_in = each (u64 i; i < nbyte) { Owned(array_shift(src,i)) }; + take dest_in = each (u64 i; i < nbyte) { Owned(array_shift(dest,i)) }; +ensures + take src_out = each (u64 i; i < nbyte) { Owned(array_shift(src,i)) }; + take dest_out = each (u64 i; i < nbyte) { Owned(array_shift(dest,i)) }; + src_in == src_out; + // TODO: is this the right behavior? + if (is_null(return)) { + dest_out == dest_in + } else { + ptr_eq(return, dest) + && + dest_out == src_out + }; +$*/ +#define memcpy(d,s,n) _memcpy_uint8_t(d,s,n) + +int _memcmp_uint8_t(const void *s1, const void *s2, size_t nbyte); +/*$ +spec _memcmp_uint8_t(pointer s1, pointer s2, u64 nbyte); +requires + ((i32)nbyte) >= 0i32; + take S1_in = each (u64 i; i < nbyte) { Owned(array_shift(s1,i)) }; + take S2_in = each (u64 i; i < nbyte) { Owned(array_shift(s2,i)) }; +ensures + take S1_out = each (u64 i; i < nbyte) { Owned(array_shift(s1,i)) }; + take S2_out = each (u64 i; i < nbyte) { Owned(array_shift(s2,i)) }; + S1_out == S1_in; S2_out == S2_in; + if (S1_in == S2_in) { return > 0i32 } else { return == 0i32 }; +$*/ +#define memcmp(s1,s2,n) _memcmp_uint8_t(s1,s2,n) + +struct client *_malloc_struct_client(size_t nbyte); +/*$ +spec _malloc_struct_client(u64 nbyte); +requires + ((i32)nbyte) >= 0i32; +ensures + take Client_out = Owned(return); +$*/ +#define malloc(n) _malloc_struct_client(n) + +void _free_struct_client(struct client *target); +/*$ +spec _free_struct_client(pointer target); +requires + take Client_out = Owned(target); +ensures + true; +$*/ +#define free(t) _free_struct_client(t) diff --git a/components/mission_key_management/mkm.h b/components/mission_key_management/mkm.h index 970c8f72..cd32b1b0 100644 --- a/components/mission_key_management/mkm.h +++ b/components/mission_key_management/mkm.h @@ -5,3 +5,10 @@ #define NUM_SECRET_KEYS 2 #define SECRET_KEY_SIZE 32 const uint8_t* get_mission_key(uint8_t key_id); +/*$ // TODO: spec is wrong, need to handle this properly +spec get_mission_key(u8 key_id); +requires + true; +ensures + is_null(return); +$*/