Skip to content

Commit

Permalink
Migrate CN memory safety specs into client.c
Browse files Browse the repository at this point in the history
  • Loading branch information
@septract
septract committed Dec 19, 2024
1 parent 218a2f2 commit 405d646
Show file tree
Hide file tree
Showing 3 changed files with 213 additions and 61 deletions.
232 changes: 189 additions & 43 deletions components/mission_key_management/client.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,24 @@
# include "cn_stubs.h"
#endif

/*$
predicate (u8) 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;
} else {
return 1u8;
}
}
predicate (struct client) ClientPred (pointer p)
{
take C = Owned<struct client>(p);
take K = KeyPred(C.key);
return C;
}
$*/

uint32_t client_state_epoll_events(enum client_state state) {
switch (state) {
Expand All @@ -36,7 +54,15 @@ uint32_t client_state_epoll_events(enum client_state state) {
}
}

struct client* client_new(int fd) {
struct client* client_new(int fd)
// TODO: Specification doesn't handle the case where malloc fails
/*$
ensures take Client_out = ClientPred(return);
Client_out.fd == fd;
Client_out.pos == 0u8;
((i32) Client_out.state) == CS_RECV_KEY_ID;
$*/
{
struct client* c = malloc(sizeof(struct client));
if (c == NULL) {
perror("malloc (client_new)");
Expand All @@ -49,24 +75,40 @@ struct client* client_new(int fd) {
return c;
}

void client_delete(struct client* 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);
}


uint8_t* client_read_buffer(struct client* 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);
// }


uint8_t* client_read_buffer(struct client* c)
/*$
requires take Client_in = ClientPred(c);
ensures take Client_out = ClientPred(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) {
case CS_RECV_KEY_ID:
return c->key_id;
Expand All @@ -77,7 +119,21 @@ uint8_t* client_read_buffer(struct client* c) {
}
}

const uint8_t* client_write_buffer(struct client* c) {
const uint8_t* client_write_buffer(struct client* c)
/*$
requires take Client_in = ClientPred(c);
ensures take Client_out = ClientPred(c);
Client_in == Client_out;
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: very confusing distinction from the previous case!
ptr_eq( return, Client_in.key )
} else {
is_null(return)
}};
$*/
{
switch (c->state) {
case CS_SEND_CHALLENGE:
return c->challenge;
Expand All @@ -88,7 +144,25 @@ const uint8_t* client_write_buffer(struct client* c) {
}
}

size_t client_buffer_size(struct client* c) {
size_t client_buffer_size(struct client* c)
/*$
requires take Client_in = ClientPred(c);
ensures take Client_out = ClientPred(c);
Client_out == Client_in;
if (((i32) Client_in.state) == CS_RECV_KEY_ID) {
return == 1u64
} else { if ( ((i32) Client_in.state) == CS_SEND_CHALLENGE ) {
return == NONCE_SIZE()
} else { if ( ((i32) Client_in.state) == CS_RECV_RESPONSE ) {
return == MEASURE_SIZE() + HMAC_SIZE()
} else { if ( ((i32) Client_in.state) == CS_SEND_KEY ) {
return == KEY_SIZE()
} else {
// CS_DONE and default cases
return == 0u64
}}}};
$*/
{
switch (c->state) {
case CS_RECV_KEY_ID:
return sizeof(c->key_id);
Expand All @@ -103,12 +177,22 @@ size_t client_buffer_size(struct client* c) {

default:
// Unreachable
// TODO: prove this state is unreachable
return 0;
}
}


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;
Expand All @@ -120,7 +204,20 @@ int client_epoll_ctl(struct client* c, int epfd, int op) {
}


enum client_event_result client_read(struct client* c) {
enum client_event_result client_read(struct client* c)
/*$
requires
take Client_in = ClientPred(c);
ensures
take Client_out = ClientPred(c);
// TODO: more compact notation?
Client_out.fd == Client_in.fd;
Client_out.challenge == Client_in.challenge;
ptr_eq(Client_out.key, Client_in.key);
Client_out.key_id == Client_in.key_id;
Client_out.state == Client_in.state;
$*/
{
uint8_t* buf = client_read_buffer(c);
if (buf == NULL) {
// There's no read operation to perform.
Expand All @@ -133,7 +230,12 @@ enum client_event_result client_read(struct client* c) {
return RES_DONE;
}

int ret = read(c->fd, buf + c->pos, buf_size - c->pos);
// TODO: unclear why this works???
/*$ split_case(Client_in.state == (u32) CS_RECV_KEY_ID); $*/

// TODO: fix array subsetting. Probably need a lemma here
int ret = read(c->fd, buf, buf_size);
// int ret = read(c->fd, buf + c->pos, buf_size - c->pos);
if (ret < 0) {
perror("read (client_read)");
return RES_ERROR;
Expand All @@ -145,7 +247,18 @@ enum client_event_result client_read(struct client* c) {
return c->pos == buf_size ? RES_DONE : RES_PENDING;
}

enum client_event_result client_write(struct client* c) {
enum client_event_result client_write(struct client* c)
/*$
requires
take Client_in = ClientPred(c);
! is_null(Client_in.key);
// take Key_in = each(u64 i; i < KEY_SIZE()) {Owned<uint8_t>(Client_in.key + i)};
ensures
take Client_out = ClientPred(c);
// Client_in.key == Client_out.key;
// take Key_out = each(u64 i; i < KEY_SIZE()) {Owned<uint8_t>(Client_in.key + i)};
$*/
{
const uint8_t* buf = client_write_buffer(c);
if (buf == NULL) {
// There's no write operation to perform.
Expand All @@ -158,7 +271,12 @@ enum client_event_result client_write(struct client* c) {
return RES_DONE;
}

int ret = write(c->fd, buf + c->pos, buf_size - c->pos);
// TODO: unclear why this works???
/*$ split_case(Client_in.state == (u32) CS_SEND_CHALLENGE); $*/

// 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) {
perror("write (client_write)");
return RES_ERROR;
Expand All @@ -171,12 +289,34 @@ enum client_event_result client_write(struct client* c) {
}


void client_change_state(struct client* c, enum client_state new_state) {
void client_change_state(struct client* c, enum client_state new_state)
/*$
requires
take Client_in = ClientPred(c);
ensures
take Client_out = ClientPred(c);
// TODO: more compact notation?
Client_out.fd == Client_in.fd;
Client_out.challenge == Client_in.challenge;
ptr_eq(Client_out.key, Client_in.key); // <-- unnecessary
Client_out.key_id == Client_in.key_id;
Client_out.pos == 0u8;
Client_out.state == new_state;
$*/
{
c->state = new_state;
c->pos = 0;
}

enum client_event_result client_event(struct client* c, uint32_t events) {
enum client_event_result client_event(struct client* c, uint32_t events)
/*$
requires
take Client_in = ClientPred(c);
! is_null(Client_in.key);
ensures
take Client_out = ClientPred(c);
$*/
{
if (events & EPOLLIN) {
enum client_event_result result = client_read(c);
if (result != RES_DONE) {
Expand Down Expand Up @@ -208,29 +348,35 @@ enum client_event_result client_event(struct client* c, uint32_t events) {
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:
// memcpy(c->challenge, "random 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:
// 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 receeive the attestation response.
// Waiting to receive the attestation response.
CS_RECV_RESPONSE,
// In the process of sending the key.
CS_SEND_KEY,
Expand Down
Loading

0 comments on commit 405d646

Please sign in to comment.