use shared opensut CN definitions

GaloisInc · Dec 11, 2024 · 055581e · 055581e
1 parent 042f281
commit 055581e
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 70 deletions.
diff --git 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
@@ -10,12 +10,12 @@
 
 #ifndef CN_ENV
 # include <sys/epoll.h>
-# include <unistd.h>
-# include <stdio.h>
-#else
-# include "cn_stubs.h"
 #endif
+#include <unistd.h>
+#include <stdio.h>
 
+#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<struct client>(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<struct client>(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<struct client>;
 $*/
 {
     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<struct client>(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
@@ -1,18 +1,17 @@
 #pragma once
 
-// Provides substitutes for some declarations that CN has trouble with.
-
-// Cerberus puts some POSIX headers under the `posix/` directory.
-#include <posix/sys/types.h>
-
-
 // From `sys/epoll.h`
 #define EPOLLIN 1
 #define EPOLLOUT 4
 
 
 // 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<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)