From 055581e0e8b310d3437db35315881ed59e144b75 Mon Sep 17 00:00:00 2001 From: Gus O'Hanley Date: Wed, 11 Dec 2024 15:43:29 -0600 Subject: [PATCH] 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)