Skip to content

Commit

Permalink
mkm: Prove memory safety for remaining fns
Browse files Browse the repository at this point in the history
  • Loading branch information
@septract
septract committed Dec 20, 2024
1 parent 405d646 commit de0ba91
Show file tree
Hide file tree
Showing 3 changed files with 98 additions and 49 deletions.
124 changes: 76 additions & 48 deletions components/mission_key_management/client.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,25 +17,40 @@
#endif

/*$
predicate (u8) KeyPred (pointer p)
predicate (boolean) KeyPred (pointer p)
{
if (! is_null(p)) {
take K = each(u64 i; i < KEY_SIZE()) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
return 0u8;
return true;
} else {
return 1u8;
return false;
}
}
// TODO: should be implicit from the fact client_state is an enum
function (boolean) ValidState (u32 state) {
((state == (u32) CS_RECV_KEY_ID) ||
(state == (u32) CS_SEND_CHALLENGE) ||
(state == (u32) CS_RECV_RESPONSE) ||
(state == (u32) CS_SEND_KEY) ||
(state == (u32) CS_DONE) )
}
predicate (struct client) ClientPred (pointer p)
{
take C = Owned<struct client>(p);
assert ( ValidState(C.state) ) ;
take K = KeyPred(C.key);
return C;
}
$*/

uint32_t client_state_epoll_events(enum client_state state) {

uint32_t client_state_epoll_events(enum client_state state)
/*$
requires ValidState( state );
$*/
{
switch (state) {
case CS_RECV_KEY_ID:
return EPOLLIN;
Expand All @@ -48,9 +63,12 @@ uint32_t client_state_epoll_events(enum client_state state) {
case CS_DONE:
return 0;

default:
default:{ // TODO: block needed for assert()
// Prove this state is unreachable:
/*$ assert ( false ); $*/
// Unreachable
return 0;
}
}
}

Expand All @@ -75,30 +93,35 @@ ensures take Client_out = ClientPred(return);
return c;
}

// void client_delete(struct client* c)
// /*$ requires take Client_in = ClientPred(c); $*/
// {
// int ret = shutdown(c->fd, SHUT_RDWR);
// if (ret != 0) {
// perror("shutdown (client_delete)");
// // Keep going. Even if TCP shutdown fails, we still need to close the
// // file descriptor.
// }
// 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)
/*$
requires
take Client_in = ClientPred(c);
$*/
{
int ret = shutdown(c->fd, SHUT_RDWR);
if (ret != 0) {
perror("shutdown (client_delete)");
// Keep going. Even if TCP shutdown fails, we still need to close the
// file descriptor.
}
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.
}
key_release(c->key); // Ghost function returning ownership of the key pointer
free(c);
}


uint8_t* client_read_buffer(struct client* c)
/*$
requires take Client_in = ClientPred(c);
ensures take Client_out = ClientPred(c);
Client_out == Client_in;
// TODO: ugly notation, should support if-elif-elif-...-else
if (((i32) Client_in.state) == CS_RECV_KEY_ID) {
ptr_eq( return, member_shift(c, key_id) )
} else {
Expand Down Expand Up @@ -175,10 +198,12 @@ ensures take Client_out = ClientPred(c);
case CS_DONE:
return 0;

default:
default: { // TODO: block needed for assert()
// Prove this state is unreachable:
/*$ assert(false); $*/
// Unreachable
// TODO: prove this state is unreachable
return 0;
}
}
}

Expand Down Expand Up @@ -293,6 +318,7 @@ void client_change_state(struct client* c, enum client_state new_state)
/*$
requires
take Client_in = ClientPred(c);
ValidState(new_state);
ensures
take Client_out = ClientPred(c);
// TODO: more compact notation?
Expand All @@ -312,8 +338,8 @@ enum client_event_result client_event(struct client* c, uint32_t events)
/*$
requires
take Client_in = ClientPred(c);
! is_null(Client_in.key);
ensures
! is_null(Client_in.key); // TODO: should depend on state machine state
ensures
take Client_out = ClientPred(c);
$*/
{
Expand Down Expand Up @@ -348,35 +374,37 @@ ensures
return RES_ERROR;
}

// /*$ split_case(Client_in.state == (u32) CS_RECV_KEY_ID); $*/
// /*$ split_case(Client_in.state == (u32) CS_SEND_CHALLENGE); $*/
// /*$ split_case(Client_in.state == (u32) CS_RECV_RESPONSE); $*/
// /*$ split_case(Client_in.state == (u32) CS_SEND_KEY); $*/
// /*$ split_case(Client_in.state == (u32) CS_DONE); $*/

// 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, "random challenge", NONCE_SIZE);
// client_change_state(c, CS_SEND_CHALLENGE);
// break;

case CS_RECV_KEY_ID: { // <-- TODO: block needed for var 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);
uint8_t challenge[NONCE_SIZE] = "random challenge";
memcpy(c->challenge, &challenge, NONCE_SIZE);

client_change_state(c, CS_SEND_CHALLENGE);
break;
}

case CS_SEND_CHALLENGE:
client_change_state(c, CS_RECV_RESPONSE);
break;

// case CS_RECV_RESPONSE:
// c->key = policy_match(c->key_id, c->challenge,
// c->response, c->response + MEASURE_SIZE);
// 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]);
// return RES_ERROR;
// }
// client_change_state(c, CS_SEND_KEY);
// fprintf(stderr, "client %d: sending key %u\n", c->fd, c->key_id[0]);
// break;
case CS_RECV_RESPONSE:
// TODO: ghost code - give back the old key
key_release(c->key); // Should be removed eventually
c->key = policy_match(c->key_id, c->challenge,
c->response, c->response + MEASURE_SIZE);
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]);
return RES_ERROR;
}
client_change_state(c, CS_SEND_KEY);
fprintf(stderr, "client %d: sending key %u\n", c->fd, c->key_id[0]);
break;

case CS_SEND_KEY:
client_change_state(c, CS_DONE);
Expand Down
2 changes: 1 addition & 1 deletion components/mission_key_management/client.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ enum client_state {
CS_RECV_KEY_ID,
// In the process of sending a challenge for attestation.
CS_SEND_CHALLENGE,
// Waiting to receive the attestation response.
// Waiting to recieve the attestation response.
CS_RECV_RESPONSE,
// In the process of sending the key.
CS_SEND_KEY,
Expand Down
21 changes: 21 additions & 0 deletions components/mission_key_management/cn_stubs.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,27 @@ static uint64_t c_HMAC_KEY_SIZE() /*$ cn_function HMAC_KEY_SIZE; $*/ { return HM
/*$ function (u64) KEY_SIZE () $*/
static uint64_t c_KEY_SIZE() /*$ cn_function KEY_SIZE; $*/ { return KEY_SIZE; }

// 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],
uint8_t measure[MEASURE_SIZE], uint8_t hmac[HMAC_SIZE]);
/*$ spec policy_match(pointer key_id, pointer nonce, pointer measure, pointer hmac);
requires
true;
ensures
take Key_out = KeyPred(return);
$*/

// 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);
requires
take Key_in = KeyPred(key);
ensures
true;
$*/

// From `stdio.h`

#ifndef WAR_CN_309
Expand Down

0 comments on commit de0ba91

Please sign in to comment.