Skip to content

Commit

Permalink
mkm: make proof use CN standard predicates
Browse files Browse the repository at this point in the history
  • Loading branch information
@septract
septract committed Dec 20, 2024
1 parent de0ba91 commit 4f4b81e
Show file tree
Hide file tree
Showing 3 changed files with 94 additions and 64 deletions.
7 changes: 7 additions & 0 deletions components/mission_key_management/Makefile
View file
Original file line number Diff line number Diff line change
@@ -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++
Expand Down Expand Up @@ -34,3 +37,7 @@ $(BUILD_DIR)/%.o: $(ROOT_DIR)/%.c
.PHONY: clean
clean:
rm -rf build/ build.*/

.PHONY: cn_proof
cn_proof:
$(CN) client.c
24 changes: 18 additions & 6 deletions components/mission_key_management/client.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,14 @@

#ifndef CN_ENV
# include <sys/epoll.h>
#endif

# include <sys/socket.h>
# include <unistd.h>
# include <stdio.h>
#else

# include "cn_memory.h"
# include "cn_stubs.h"
#endif

/*$
predicate (boolean) KeyPred (pointer p)
Expand All @@ -36,6 +38,7 @@ function (boolean) ValidState (u32 state) {
(state == (u32) CS_DONE) )
}
// TODO: wrap up the alloc() in the ClientPred predicate
predicate (struct client) ClientPred (pointer p)
{
take C = Owned<struct client>(p);
Expand Down Expand Up @@ -76,8 +79,8 @@ struct client* client_new(int fd)
// TODO: Specification doesn't handle the case where malloc fails
/*$
ensures take Client_out = ClientPred(return);
take log = Alloc(return);
Client_out.fd == fd;
Client_out.pos == 0u8;
((i32) Client_out.state) == CS_RECV_KEY_ID;
$*/
{
Expand All @@ -86,17 +89,24 @@ ensures take Client_out = ClientPred(return);
perror("malloc (client_new)");
return NULL;
}
/*$ from_bytes Block<struct client>(c); $*/
c->fd = fd;
c->pos = 0;
c->state = CS_RECV_KEY_ID;
c->key = NULL;
memset(c->challenge,0,NONCE_SIZE);
memset(c->response,0,MEASURE_SIZE + HMAC_SIZE);
memset(c->key_id,0,KEY_ID_SIZE);
return c;
}

void client_delete(struct client* c)
/*$
requires
take Client_in = ClientPred(c);
take log = Alloc(c);
log.base == (u64)c;
log.size == sizeof<struct client>;
$*/
{
int ret = shutdown(c->fd, SHUT_RDWR);
Expand All @@ -112,6 +122,7 @@ requires
// but may report I/O errors afterward.
}
key_release(c->key); // Ghost function returning ownership of the key pointer
/*$ to_bytes Block<struct client>(c); $*/
free(c);
}

Expand Down Expand Up @@ -336,6 +347,7 @@ ensures

enum client_event_result client_event(struct client* c, uint32_t events)
/*$
accesses __stderr;
requires
take Client_in = ClientPred(c);
! is_null(Client_in.key); // TODO: should depend on state machine state
Expand Down Expand Up @@ -378,11 +390,11 @@ requires
// transition to the next state.
switch (c->state) {
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
// 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);
memcpy(c->challenge, challenge, NONCE_SIZE);

client_change_state(c, CS_SEND_CHALLENGE);
break;
Expand Down
127 changes: 69 additions & 58 deletions components/mission_key_management/cn_stubs.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,11 @@ ensures

// 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
Expand All @@ -72,8 +77,8 @@ void perror(const char *msg);
ensures true;
$*/

#define fprintf(...) 0
#define snprintf(...) 0
// #define fprintf(...) 0
// #define snprintf(...) 0


// From `unistd.h`
Expand Down Expand Up @@ -118,59 +123,65 @@ int _shutdown(int fildes, int how);
$*/
#define shutdown(x,h) _shutdown(x,h)

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)
#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)


// 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)

0 comments on commit 4f4b81e

Please sign in to comment.