From 7e9cbb54675171f9b882078e8dcc3c3c031fc2d4 Mon Sep 17 00:00:00 2001 From: septract Date: Wed, 27 Nov 2024 16:48:04 -0800 Subject: [PATCH 1/4] Verify a few of the functions, with some modifications --- .../mission_key_management/client-reduced.c | 335 ++++++++++++++++++ components/mission_key_management/cn_stubs.h | 34 +- 2 files changed, 358 insertions(+), 11 deletions(-) create mode 100644 components/mission_key_management/client-reduced.c diff --git a/components/mission_key_management/client-reduced.c b/components/mission_key_management/client-reduced.c new file mode 100644 index 00000000..114b85a6 --- /dev/null +++ b/components/mission_key_management/client-reduced.c @@ -0,0 +1,335 @@ +// Client state machine. Each connection has a separate `struct client` +// object, which tracks progress through the key request protocol for that +// connection. + +#include +#include + +#include "client.h" +#include "mkm.h" + +#ifndef CN_ENV +# include +# include +# include +#else +# include "cn_stubs.h" +#endif + + +uint32_t client_state_epoll_events(enum client_state state) { + switch (state) { + case CS_RECV_KEY_ID: + return EPOLLIN; + case CS_SEND_CHALLENGE: + return EPOLLOUT; + case CS_RECV_RESPONSE: + return EPOLLIN; + case CS_SEND_KEY: + return EPOLLOUT; + case CS_DONE: + return 0; + + default: + // Unreachable + return 0; + } +} + +// struct client* client_new(int fd) { +// struct client* c = malloc(sizeof(struct client)); +// if (c == NULL) { +// perror("malloc (client_new)"); +// return NULL; +// } +// c->fd = fd; +// c->pos = 0; +// c->state = CS_RECV_KEY_ID; +// return c; +// } + +// void client_delete(struct client* c) { +// int ret = close(c->fd); +// if (ret != 0) { +// perror("close (client_delete)"); +// // Keep going. On Linux, `close` always closes the file descriptor, +// // but may report I/O errors afterward. +// } +// free(c); +// } + + +inline uint8_t* client_read_buffer(struct client* c) +/*$ +requires + take Client = Owned(c); +ensures + take Client_ = Owned(c); + Client_ == Client; + ( ((i32) Client.state) == CS_RECV_KEY_ID ? + ptr_eq( return, member_shift(c, key_id) ) + : + ( ((i32) Client.state) == CS_RECV_RESPONSE ? + ptr_eq( return, member_shift(c, response) ) + : + is_null(return) + ) + ); +$*/ +{ + switch (c->state) { + case CS_RECV_KEY_ID: + return c->key_id; + case CS_RECV_RESPONSE: + return c->response; + default: + return NULL; + } +} + +// const uint8_t* client_write_buffer(struct client* c) +// /*$ +// accesses mission_keys; +// requires +// take Client = Owned(c); +// ensures +// take Client_ = Owned(c); +// Client_ == Client; +// let key_id = Client.key_id[0u64]; +// ( ((i32) Client.state) == CS_SEND_CHALLENGE ? +// ptr_eq( return, member_shift(c, challenge) ) +// : +// ( ((i32) Client.state) == CS_SEND_KEY ? +// // TODO: +// // The result of get_mission_key(key_id) is mission_keys[key_id] +// ptr_eq( return, &mission_keys ) +// : +// is_null(return) +// ) +// ); +// $*/ +// { +// switch (c->state) { +// case CS_SEND_CHALLENGE: +// return c->challenge; +// case CS_SEND_KEY: { +// /*$ extract Owned, 0u64; $*/ +// return get_mission_key(c->key_id[0]); +// } +// default: +// return NULL; +// } +// } + +inline size_t client_buffer_size(struct client* c) +/*$ +requires + take Client = Owned(c); +ensures + take Client_ = Owned(c); + Client_ == Client; + return == + ( ((i32) Client.state) == CS_RECV_KEY_ID ? + 1u64 + : + ( ((i32) Client.state) == CS_SEND_CHALLENGE ? + 32u64 + : + ( ((i32) Client.state) == CS_RECV_RESPONSE ? + 32u64 + : + ( ((i32) Client.state) == CS_SEND_KEY ? + 32u64 + : + 0u64 + ) + ) + ) + ); +$*/ +{ + switch (c->state) { + case CS_RECV_KEY_ID: + return sizeof(c->key_id); + case CS_SEND_CHALLENGE: + return sizeof(c->challenge); + case CS_RECV_RESPONSE: + return sizeof(c->response); + case CS_SEND_KEY: + return SECRET_KEY_SIZE; + case CS_DONE: + return 0; + + default: + // Unreachable + return 0; + } +} + + +int client_epoll_ctl(struct client* c, int epfd, int op) { +#ifndef CN_ENV + struct epoll_event ev; + ev.data.ptr = c; + ev.events = client_state_epoll_events(c->state); + return epoll_ctl(epfd, op, c->fd, &ev); +#else + return 0; +#endif +} + +// // Returns the value pointed to by p. +// int library_function(int *p); +// /*$ +// spec library_function(pointer p); +// requires +// take p_in = Owned(p); +// ensures +// take p_out = Owned(p); +// return == p_out; +// $*/ + +enum client_event_result client_read(struct client* c) +/*$ +requires + take Client_in = Owned(c); + // TODO: case splitting isn't handled properly + // Client_in.state == (u32) CS_RECV_KEY_ID + // || + // ( Client_in.state == (u32) CS_SEND_CHALLENGE + // || + // ( Client_in.state == (u32) CS_RECV_RESPONSE + // || + // ( Client_in.state == (u32) CS_SEND_KEY + // || + // ( Client_in.state == (u32) CS_DONE )))); +ensures + take Client_out = Owned(c); +$*/ +{ + uint8_t* buf = client_read_buffer(c); + if (buf == NULL) { + // There's no read operation to perform. + return RES_DONE; + } + + size_t buf_size = client_buffer_size(c); + if (c->pos >= buf_size) { + // Read operation has already finished. + return RES_DONE; + } + + /*$ split_case(Client_in.state == (u32) CS_RECV_KEY_ID); $*/ + // TODO: array subsetting isn't handled + 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) { + // perror("read (client_read)"); + return RES_ERROR; + } else if (ret == 0) { + return RES_EOF; + } + c->pos += ret; + + return c->pos == buf_size ? RES_DONE : RES_PENDING; +} + +// enum client_event_result client_write(struct client* c) { +// const uint8_t* buf = client_write_buffer(c); +// if (buf == NULL) { +// // There's no write operation to perform. +// return RES_DONE; +// } + +// size_t buf_size = client_buffer_size(c); +// if (c->pos >= buf_size) { +// // Write operation has already finished. +// return RES_DONE; +// } + +// int ret = write(c->fd, buf + c->pos, buf_size - c->pos); +// if (ret < 0) { +// perror("write (client_write)"); +// return RES_ERROR; +// } else if (ret == 0) { +// return RES_EOF; +// } +// c->pos += ret; + +// return c->pos == buf_size ? RES_DONE : RES_PENDING; +// } + + +// void client_change_state(struct client* c, enum client_state new_state) { +// c->state = new_state; +// 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; +// } diff --git a/components/mission_key_management/cn_stubs.h b/components/mission_key_management/cn_stubs.h index 6e71db46..b2254f83 100644 --- a/components/mission_key_management/cn_stubs.h +++ b/components/mission_key_management/cn_stubs.h @@ -37,18 +37,30 @@ void perror(const char *msg); // From `unistd.h` +// ssize_t _read(int fildes, void *buf, size_t n); +// /*$ spec _read(i32 fildes, pointer buf, u64 n); +// // accesses errno; +// requires +// take bufi = ArrayBlock_u8(buf, n); +// ensures +// return >= -1i64 && return <= (i64)n; +// // return == -1 -> no owned, all block +// // return >= 0 < n -> 0 <= owned < return, return <= block < n +// // return == n -> 0 <= owned < n, return <= block < n +// take bufo = each(u64 i; (return == -1i64) ? false : (0u64 <= i && i <(u64)return)) {Owned(array_shift(buf, i))}; +// 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); -/*$ spec _read(i32 fildes, pointer buf, u64 n); - // accesses errno; - requires - take bufi = ArrayBlock_u8(buf, n); - ensures - return >= -1i64 && return <= (i64)n; - // return == -1 -> no owned, all block - // return >= 0 < n -> 0 <= owned < return, return <= block < n - // return == n -> 0 <= owned < n, return <= block < n - take bufo = each(u64 i; (return == -1i64) ? false : (0u64 <= i && i <(u64)return)) {Owned(array_shift(buf, i))}; - take bufb = each(u64 i; (return == -1i64) ? (0u64 <= i && i < n) : ((u64)return <= i && i < n)) {Block(array_shift(buf, i))}; +/*$ +spec _read(i32 fildes, pointer buf, u64 n); +requires + 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))}; $*/ #define read(f,b,s) _read(f,b,s) From e55a3fb7862905bda0e5a04d66caf584b29d9946 Mon Sep 17 00:00:00 2001 From: septract Date: Wed, 27 Nov 2024 17:39:36 -0800 Subject: [PATCH 2/4] mkm: verify memory safety of more functions --- .../mission_key_management/client-reduced.c | 290 ++++++++++-------- 1 file changed, 157 insertions(+), 133 deletions(-) diff --git a/components/mission_key_management/client-reduced.c b/components/mission_key_management/client-reduced.c index 114b85a6..acf8f99a 100644 --- a/components/mission_key_management/client-reduced.c +++ b/components/mission_key_management/client-reduced.c @@ -36,45 +36,61 @@ uint32_t client_state_epoll_events(enum client_state state) { } } -// struct client* client_new(int fd) { -// struct client* c = malloc(sizeof(struct client)); -// if (c == NULL) { -// perror("malloc (client_new)"); -// return NULL; -// } -// c->fd = fd; -// c->pos = 0; -// c->state = CS_RECV_KEY_ID; -// return c; -// } +struct client* client_new(int fd) +/*$ +trusted; +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; +$*/ +{ + struct client* c = malloc(sizeof(struct client)); + if (c == NULL) { + perror("malloc (client_new)"); + return NULL; + } + c->fd = fd; + c->pos = 0; + c->state = CS_RECV_KEY_ID; + return c; +} -// void client_delete(struct client* c) { -// int ret = close(c->fd); -// if (ret != 0) { -// perror("close (client_delete)"); -// // Keep going. On Linux, `close` always closes the file descriptor, -// // but may report I/O errors afterward. -// } -// free(c); -// } +void client_delete(struct client* c) +/*$ +trusted; +requires + take Client_in = Owned(c); +// TODO: handle close / perror properly +$*/ +{ + int ret = close(c->fd); + if (ret != 0) { + perror("close (client_delete)"); + // Keep going. On Linux, `close` always closes the file descriptor, + // but may report I/O errors afterward. + } + free(c); +} inline uint8_t* client_read_buffer(struct client* c) /*$ requires - take Client = Owned(c); + take Client_in = Owned(c); ensures - take Client_ = Owned(c); - Client_ == Client; - ( ((i32) Client.state) == CS_RECV_KEY_ID ? - ptr_eq( return, member_shift(c, key_id) ) - : - ( ((i32) Client.state) == CS_RECV_RESPONSE ? + take Client_out = Owned(c); + Client_out == Client_in; + if (((i32) Client_in.state) == CS_RECV_KEY_ID) { + ptr_eq( return, member_shift(c, key_id) ) + } else { + if (((i32) Client_in.state) == CS_RECV_RESPONSE) { ptr_eq( return, member_shift(c, response) ) - : + } else { is_null(return) - ) - ); + }}; $*/ { switch (c->state) { @@ -87,65 +103,58 @@ ensures } } -// const uint8_t* client_write_buffer(struct client* c) -// /*$ -// accesses mission_keys; -// requires -// take Client = Owned(c); -// ensures -// take Client_ = Owned(c); -// Client_ == Client; -// let key_id = Client.key_id[0u64]; -// ( ((i32) Client.state) == CS_SEND_CHALLENGE ? -// ptr_eq( return, member_shift(c, challenge) ) -// : -// ( ((i32) Client.state) == CS_SEND_KEY ? -// // TODO: -// // The result of get_mission_key(key_id) is mission_keys[key_id] -// ptr_eq( return, &mission_keys ) -// : -// is_null(return) -// ) -// ); -// $*/ -// { -// switch (c->state) { -// case CS_SEND_CHALLENGE: -// return c->challenge; -// case CS_SEND_KEY: { -// /*$ extract Owned, 0u64; $*/ -// return get_mission_key(c->key_id[0]); -// } -// default: -// return NULL; -// } -// } +const uint8_t* client_write_buffer(struct client* c) +/*$ +requires + take Client_in = Owned(c); +ensures + take Client_out = Owned(c); + Client_in == Client_out; + // let key_id = Client.key_id[0u64]; + if (((i32) Client_in.state) == CS_SEND_CHALLENGE) { + ptr_eq( return, member_shift(c, challenge) ) + } else { + if (((i32) Client_in.state) == CS_SEND_KEY) { + // TODO: fix this case + is_null(return) + } else { + is_null(return) + }}; +$*/ +{ + switch (c->state) { + case CS_SEND_CHALLENGE: + 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; + } + default: + return NULL; + } +} inline size_t client_buffer_size(struct client* c) -/*$ +/*$ requires - take Client = Owned(c); + take Client_in = Owned(c); ensures - take Client_ = Owned(c); - Client_ == Client; - return == - ( ((i32) Client.state) == CS_RECV_KEY_ID ? - 1u64 - : - ( ((i32) Client.state) == CS_SEND_CHALLENGE ? - 32u64 - : - ( ((i32) Client.state) == CS_RECV_RESPONSE ? - 32u64 - : - ( ((i32) Client.state) == CS_SEND_KEY ? + take Client_out = Owned(c); + Client_out == Client_in; + // TODO: have to concretize the array sizes + return == ( + if (((i32) Client_in.state) == CS_RECV_KEY_ID) { + 1u64 + } else { + if ( ((i32) Client_in.state) == CS_SEND_CHALLENGE || + ((i32) Client_in.state) == CS_RECV_RESPONSE || + ((i32) Client_in.state) == CS_SEND_KEY ) { 32u64 - : + } else { 0u64 - ) - ) - ) - ); + }} ); $*/ { switch (c->state) { @@ -167,7 +176,16 @@ ensures } -int client_epoll_ctl(struct client* c, int epfd, int op) { +int client_epoll_ctl(struct client* c, int epfd, int op) +/*$ +// TODO: fill in an actual spec here, depending what's needed +trusted; +requires + true; +ensures + true; +$*/ +{ #ifndef CN_ENV struct epoll_event ev; ev.data.ptr = c; @@ -178,33 +196,12 @@ int client_epoll_ctl(struct client* c, int epfd, int op) { #endif } -// // Returns the value pointed to by p. -// int library_function(int *p); -// /*$ -// spec library_function(pointer p); -// requires -// take p_in = Owned(p); -// ensures -// take p_out = Owned(p); -// return == p_out; -// $*/ - enum client_event_result client_read(struct client* c) /*$ requires - take Client_in = Owned(c); - // TODO: case splitting isn't handled properly - // Client_in.state == (u32) CS_RECV_KEY_ID - // || - // ( Client_in.state == (u32) CS_SEND_CHALLENGE - // || - // ( Client_in.state == (u32) CS_RECV_RESPONSE - // || - // ( Client_in.state == (u32) CS_SEND_KEY - // || - // ( Client_in.state == (u32) CS_DONE )))); + take Client_in = Owned(c); ensures - take Client_out = Owned(c); + take Client_out = Owned(c); $*/ { uint8_t* buf = client_read_buffer(c); @@ -220,11 +217,12 @@ ensures } /*$ split_case(Client_in.state == (u32) CS_RECV_KEY_ID); $*/ - // TODO: array subsetting isn't handled + // 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)"); return RES_ERROR; } else if (ret == 0) { @@ -235,36 +233,62 @@ ensures return c->pos == buf_size ? RES_DONE : RES_PENDING; } -// enum client_event_result client_write(struct client* c) { -// const uint8_t* buf = client_write_buffer(c); -// if (buf == NULL) { -// // There's no write operation to perform. -// return RES_DONE; -// } +enum client_event_result client_write(struct client* c) +/*$ +requires + take Client_in = Owned(c); +ensures + take Client_out = Owned(c); +$*/ +{ + const uint8_t* buf = client_write_buffer(c); + if (buf == NULL) { + // There's no write operation to perform. + return RES_DONE; + } -// size_t buf_size = client_buffer_size(c); -// if (c->pos >= buf_size) { -// // Write operation has already finished. -// return RES_DONE; -// } + size_t buf_size = client_buffer_size(c); + if (c->pos >= buf_size) { + // Write operation has already finished. + return RES_DONE; + } -// int ret = write(c->fd, buf + c->pos, buf_size - c->pos); -// if (ret < 0) { -// perror("write (client_write)"); -// return RES_ERROR; -// } else if (ret == 0) { -// return RES_EOF; -// } -// c->pos += ret; + // TODO: array subsetting isn't handled. 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); -// return c->pos == buf_size ? RES_DONE : RES_PENDING; -// } + if (ret < 0) { + // TODO: re-enable this + // perror("write (client_write)"); + return RES_ERROR; + } else if (ret == 0) { + return RES_EOF; + } + c->pos += ret; + return c->pos == buf_size ? RES_DONE : RES_PENDING; +} -// void client_change_state(struct client* c, enum client_state new_state) { -// c->state = new_state; -// c->pos = 0; -// } + +void client_change_state(struct client* c, enum client_state new_state) +/*$ +requires + take Client_in = Owned(c); +ensures + take Client_out = Owned(c); + Client_out.state == new_state; + Client_out.pos == 0u8; + + // TODO: tedious, is there some way to say nothing else changed? + Client_out.fd == Client_in.fd; + Client_out.challenge == Client_in.challenge; + Client_out.response == Client_in.response; + Client_out.key_id == Client_in.key_id; +$*/ +{ + c->state = new_state; + c->pos = 0; +} // enum client_event_result client_event(struct client* c, uint32_t events) { // if (events & EPOLLIN) { From 042f28119c8b49796a240e1535dc70a45ef664f4 Mon Sep 17 00:00:00 2001 From: Mike Dodds Date: Thu, 28 Nov 2024 13:55:49 -0800 Subject: [PATCH 3/4] 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); +$*/ From 055581e0e8b310d3437db35315881ed59e144b75 Mon Sep 17 00:00:00 2001 From: Gus O'Hanley Date: Wed, 11 Dec 2024 15:43:29 -0600 Subject: [PATCH 4/4] use shared opensut CN definitions --- components/mission_key_management/Makefile | 7 ++ .../mission_key_management/client-reduced.c | 22 ++++-- components/mission_key_management/cn_stubs.h | 73 +++---------------- 3 files changed, 32 insertions(+), 70 deletions(-) diff --git a/components/mission_key_management/Makefile b/components/mission_key_management/Makefile index 8c19b568..dee76e40 100644 --- a/components/mission_key_management/Makefile +++ b/components/mission_key_management/Makefile @@ -1,5 +1,8 @@ ROOT_DIR:=$(shell dirname $(realpath $(firstword $(MAKEFILE_LIST)))) +$(opam env) +CN=cn verify --magic-comment-char-dollar --include=$(ROOT_DIR)/../include/wars.h -I $(ROOT_DIR)/../include -I $(OPAM_SWITCH_PREFIX)/lib/cerberus/runtime/libc/include/posix + ifeq ($(TARGET),x86_64) CC = x86_64-linux-gnu-gcc CXX = x86_64-linux-gnu-g++ @@ -35,3 +38,7 @@ $(BUILD_DIR)/%.o: $(ROOT_DIR)/%.c .PHONY: clean clean: rm -rf build/ build.*/ + +.PHONY: cn_proof +cn_proof: + $(CN) client-reduced.c diff --git a/components/mission_key_management/client-reduced.c b/components/mission_key_management/client-reduced.c index 12368331..b5de71b3 100644 --- a/components/mission_key_management/client-reduced.c +++ b/components/mission_key_management/client-reduced.c @@ -10,12 +10,12 @@ #ifndef CN_ENV # include -# include -# include -#else -# include "cn_stubs.h" #endif +#include +#include +#include "cn_memory.h" +#include "cn_stubs.h" uint32_t client_state_epoll_events(enum client_state state) { switch (state) { @@ -41,6 +41,7 @@ struct client* client_new(int fd) // TODO: Doesn't handle the case where malloc fails ensures take Client_out = Owned(return); + take log = Alloc(return); Client_out.fd == fd; Client_out.pos == 0u8; ((i32) Client_out.state) == CS_RECV_KEY_ID; @@ -52,16 +53,23 @@ ensures perror("malloc (client_new)"); return NULL; } + /*$ from_bytes Block(c); $*/ c->fd = fd; c->pos = 0; c->state = CS_RECV_KEY_ID; + memset(c->challenge,0,32); + memset(c->response,0,32); + memset(c->key_id,0,1); return c; } void client_delete(struct client* c) /*$ requires - take Client_in = Owned(c); + take Client_in = Owned(c); + take log = Alloc(c); + log.base == (u64)c; + log.size == sizeof; $*/ { int ret = close(c->fd); @@ -70,6 +78,7 @@ requires // Keep going. On Linux, `close` always closes the file descriptor, // but may report I/O errors afterward. } + /*$ to_bytes Block(c); $*/ free(c); } @@ -292,6 +301,7 @@ ensures enum client_event_result client_event(struct client* c, uint32_t events) /*$ +accesses __stderr; requires take Client_in = Owned(c); ensures @@ -330,7 +340,7 @@ ensures // 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); + memcpy(c->challenge, challenge, 32); client_change_state(c, CS_SEND_CHALLENGE); break; } diff --git a/components/mission_key_management/cn_stubs.h b/components/mission_key_management/cn_stubs.h index 5578d263..2ef80b41 100644 --- a/components/mission_key_management/cn_stubs.h +++ b/components/mission_key_management/cn_stubs.h @@ -1,11 +1,5 @@ #pragma once -// Provides substitutes for some declarations that CN has trouble with. - -// Cerberus puts some POSIX headers under the `posix/` directory. -#include - - // From `sys/epoll.h` #define EPOLLIN 1 #define EPOLLOUT 4 @@ -13,6 +7,11 @@ // From `stdio.h` +/*$ spec fprintf(pointer f, pointer s); +requires true; +ensures true; +$*/ + #ifndef WAR_CN_309 // not possible to call this due to CN issue #309 // this spec isn't right but can't develop it at all without #309 @@ -33,8 +32,6 @@ ensures ensures true; $*/ -#define fprintf(...) 0 -#define snprintf(...) 0 // From `unistd.h` @@ -86,59 +83,7 @@ ensures $*/ #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) +#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)