Skip to content

Commit

Permalink
mkm: verified memory safety of remaining client fns
Browse files Browse the repository at this point in the history
  • Loading branch information
@septract @peterohanley
septract authored and peterohanley committed Dec 11, 2024
1 parent e55a3fb commit 042f281
Show file tree
Hide file tree
Showing 3 changed files with 185 additions and 105 deletions.
179 changes: 96 additions & 83 deletions components/mission_key_management/client-reduced.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<struct client>(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)");
Expand All @@ -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);
Expand Down Expand Up @@ -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)
Expand All @@ -127,9 +125,9 @@ ensures
return c->challenge;
case CS_SEND_KEY: {
// /*$ extract Owned<uint8_t>, 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;
Expand All @@ -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
Expand All @@ -170,7 +169,8 @@ ensures
return 0;

default:
// Unreachable
// Prove that this state is unreachable:
/*@ assert false; @*/
return 0;
}
}
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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<uint8_t>, 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;
}
104 changes: 82 additions & 22 deletions components/mission_key_management/cn_stubs.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@

// Provides substitutes for some declarations that CN has trouble with.


// Cerberus puts some POSIX headers under the `posix/` directory.
#include <posix/sys/types.h>

Expand All @@ -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<char>(msg);
ensures take mo = Owned<char>(msg);
mi == mo;
/*$
spec perror(pointer msg);
requires
take mi = Owned<char>(msg);
ensures
take mo = Owned<char>(msg);
mi == mo;
$*/
#else
# define perror(...) 0
Expand All @@ -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;
Expand All @@ -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<uint8_t>(array_shift<uint8_t>(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<uint8_t>(array_shift<uint8_t>(buf, i))};
take buf_in = each (u64 i; i < n) { Owned<uint8_t>(array_shift<uint8_t>(buf, i))};
ensures
return >= -1i64 && return <= (i64)n;
take buf_out =
each (u64 i; i < n) { Owned<uint8_t>(array_shift<uint8_t>(buf, i))};
take buf_out = each (u64 i; i < n) { Owned<uint8_t>(array_shift<uint8_t>(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<uint8_t>(array_shift<uint8_t>(buf,i))};
ensures
take bufo = each(u64 i; i >= 0u64 && i < nbyte) {Owned<uint8_t>(array_shift<uint8_t>(buf,i))};
take bufi = each(u64 i; i < nbyte) {Owned<uint8_t>(array_shift<uint8_t>(buf,i))};
ensures
take bufo = each(u64 i; i < nbyte) {Owned<uint8_t>(array_shift<uint8_t>(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<uint8_t>(array_shift<uint8_t>(src,i)) };
take dest_in = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(dest,i)) };
ensures
take src_out = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(src,i)) };
take dest_out = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(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<uint8_t>(array_shift<uint8_t>(s1,i)) };
take S2_in = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(s2,i)) };
ensures
take S1_out = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(s1,i)) };
take S2_out = each (u64 i; i < nbyte) { Owned<uint8_t>(array_shift<uint8_t>(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<struct client>(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<struct client>(target);
ensures
true;
$*/
#define free(t) _free_struct_client(t)
Loading

0 comments on commit 042f281

Please sign in to comment.