A bunch of frama-c proofs running through for noise.c

3 files changed, 109 insertions, 7 deletions

diff --git a/src/noise.c b/src/noise.c
index 6cae368..e03fc45 100644
--- a/src/noise.c
+++ b/src/noise.c
@@ -22,22 +22,72 @@
     } while(0);
 #endif
 
+#ifdef VERIFICATION
+
+/*@ requires \valid(s + (0..n-1));
+  @ assigns s[0..n-1] \from c;
+  @ assigns \result \from s;
+  @ ensures result_ptr: \result == s;
+  @*/
+uint8_t *fc_memset_uint8(uint8_t *s, int c, size_t n);
+
+/*@ requires \valid(dest + (0..n-1));
+  @ requires \valid_read(src + (0..n-1));
+  @ assigns dest[0..n-1] \from src[0..n-1];
+  @ assigns \result \from dest;
+  @ ensures result_ptr: \result == dest;
+  @ ensures equals: \forall integer i; 0 <= i <= n-1 ==> dest[i] == src[i];
+  @*/
+uint8_t *fc_memcpy_uint8(uint8_t *dest, const uint8_t *src, size_t n);
+
+#else
+#define fc_memset_uint8 memset
+#define fc_memcpy_uint8 memcpy
+#endif
+
 
 volatile uint8_t host_packet_buf[MAX_HOST_PACKET_SIZE];
 volatile int host_packet_length = 0;
 
 
+/*@
+    requires \valid(st);
+    requires \valid_read(remote_key_reference + (0..31)) && \valid_read(local_key + (0..31));
+
+    ensures \valid_read(st->remote_key_reference + (0..31)) && \valid_read(st->local_key + (0..31));
+    ensures st->handshake_state == HANDSHAKE_UNINITIALIZED;
+    ensures st->failed_handshakes == 0;
+    ensures st->tx_cipher == NULL && st->rx_cipher == NULL && st->handshake == NULL;
+    assigns *st;
+ */
 void noise_state_init(struct NoiseState *st, uint8_t *remote_key_reference, uint8_t *local_key) {
     st->handshake_state = HANDSHAKE_UNINITIALIZED;
     st->handshake = NULL;
     st->tx_cipher = NULL;
     st->rx_cipher = NULL;
-    memset(st->handshake_hash, 0, sizeof(st->handshake_hash));
+    fc_memset_uint8(st->handshake_hash, 0, sizeof(st->handshake_hash));
     st->remote_key_reference = remote_key_reference;
     st->local_key = local_key;
     st->failed_handshakes = 0;
 }
 
+/*@
+    requires \valid(st);
+    requires \valid(st->handshake_hash + (0..31));
+    requires \separated(st->handshake_hash + (0..31), st, st->rx_cipher, st->tx_cipher, st->handshake);
+
+    ensures \result == 0 ==> (
+        \valid(st->handshake) &&
+        (st->handshake_state == HANDSHAKE_IN_PROGRESS));
+
+    ensures \result != 0 ==> (
+        (st->handshake == NULL) &&
+        (st->handshake_state == HANDSHAKE_UNINITIALIZED));
+
+    ensures \result \in {0, -1};
+
+    assigns st->handshake, st->handshake_state, st->rx_cipher, st->tx_cipher;
+ */
 int reset_protocol_handshake(struct NoiseState *st) {
     uninit_handshake(st, HANDSHAKE_UNINITIALIZED);
     disarm_key_scrubber();
@@ -45,10 +95,25 @@ int reset_protocol_handshake(struct NoiseState *st) {
     noise_cipherstate_free(st->rx_cipher);
     st->tx_cipher = NULL;
     st->rx_cipher = NULL;
+    st->handshake = NULL;
     memset(st->handshake_hash, 0, sizeof(st->handshake_hash));
     return start_protocol_handshake(st);
 }
 
+/*@ requires \valid(st) && \valid_read(st->local_key + (0..31));
+  
+    ensures \result == 0 ==> (
+        \valid(st->handshake) &&
+        (st->handshake_state == HANDSHAKE_IN_PROGRESS));
+
+    ensures \result != 0 ==> (
+        (st->handshake == \old(st->handshake)) &&
+        (st->handshake_state == \old(st->handshake_state)));
+
+    ensures \result \in {0, -1};
+
+    assigns st->handshake, st->handshake_state;
+ */
 int start_protocol_handshake(struct NoiseState *st) {
     /* TODO Noise-C is nice for prototyping, but we should really get rid of it for mostly three reasons:
      *   * We don't need cipher/protocol agility, and by baking the final protocol into the firmware we can save a lot
@@ -79,6 +144,11 @@ errout:
     return -1;
 }
 
+/*@ requires \valid(st);
+    requires \valid(st->local_key + (0..31));
+    requires \separated(st, st->local_key + (0..31));
+    assigns st->local_key[0..31];
+ */
 int generate_identity_key(struct NoiseState *st) {
     NoiseDHState *dh;
     int err;
@@ -87,10 +157,11 @@ int generate_identity_key(struct NoiseState *st) {
     HANDLE_NOISE_ERROR(noise_dhstate_generate_keypair(dh), "generating key pair");
 
     uint8_t unused[CURVE25519_KEY_LEN]; /* the noise api is a bit bad here. */
-    memset(st->local_key, 0, sizeof(*st->local_key)); /* FIXME sizeof is wrong here */
+    fc_memset_uint8(st->local_key, 0, CURVE25519_KEY_LEN);
 
     HANDLE_NOISE_ERROR(noise_dhstate_get_keypair(dh, st->local_key, CURVE25519_KEY_LEN, unused, sizeof(unused)), "saving key pair");
 
+    noise_dhstate_free(dh);
     return 0;
 errout:
     if (dh)
@@ -106,6 +177,8 @@ errout:
             new_state == HANDSHAKE_DONE_KNOWN_HOST;
    ensures st->handshake_state == new_state;
    ensures st->handshake == NULL;
+
+   assigns st->handshake, st->handshake_state;
  @*/
 void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) {
     if (st->handshake)
@@ -119,6 +192,7 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) {
 //@ ghost int key_match_trace = 0;
 /*@ requires empty_trace: key_checked_trace == 0;
     requires \valid(st);
+    requires \valid(usart2_out);
     requires \valid(st->handshake);
 
     requires \valid(st->remote_key + (0..sizeof(st->remote_key)-1));
@@ -194,7 +268,7 @@ int try_continue_noise_handshake(struct NoiseState * const st, uint8_t *buf, siz
         uint8_t remote_fp[BLAKE2S_HASH_SIZE];
         BLAKE2s_context_t bc;
         BLAKE2s_reset(&bc);
-        BLAKE2s_update(&bc, st->remote_key, sizeof(st->remote_key));
+        fc_BLAKE2s_update_uint8(&bc, st->remote_key, sizeof(st->remote_key));
         BLAKE2s_finish(&bc, remote_fp);
 
         //@ ghost key_checked_trace = 1;
@@ -229,15 +303,33 @@ errout:
     return -1;
 }
 
+/*@
+    requires \valid(st);
+    requires \valid_read(st->remote_key + (0..sizeof(st->remote_key)-1));
+    requires \valid(st->remote_key_reference + (0..31));
+
+    ensures st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST;
+    assigns st->remote_key_reference[0..31], st->handshake_state;
+ */
 void persist_remote_key(struct NoiseState *st) {
     BLAKE2s_context_t bc;
     BLAKE2s_reset(&bc);
-    BLAKE2s_update(&bc, st->remote_key, sizeof(st->remote_key));
+    fc_BLAKE2s_update_uint8(&bc, st->remote_key, sizeof(st->remote_key));
     BLAKE2s_finish(&bc, st->remote_key_reference);
     st->handshake_state = HANDSHAKE_DONE_KNOWN_HOST;
 }
 
-int send_encrypted_message(struct NoiseState *st, uint8_t *msg, size_t len) {
+/*@
+  requires \valid(st);
+  requires \valid(usart2_out);
+  requires \valid(st->tx_cipher);
+  requires \valid_read(msg + (0..len-1));
+  requires 0 <= len <= 65536;
+
+  ensures \result \in {0, -1, -2, -3};
+  assigns *st->tx_cipher;
+ */
+int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len) {
     int err;
     NoiseBuffer noise_buf;
     struct {
@@ -256,7 +348,7 @@ int send_encrypted_message(struct NoiseState *st, uint8_t *msg, size_t len) {
     }
 
     pkt.header.type = HOST_DATA;
-    memcpy(pkt.payload, msg, len); /* This is necessary because noises API doesn't support separate in and out buffers. D'oh! */
+    fc_memcpy_uint8(pkt.payload, msg, len); /* This is necessary because noises API doesn't support separate in and out buffers. D'oh! */
     noise_buffer_set_inout(noise_buf, pkt.payload, len, sizeof(pkt.payload));
 
     HANDLE_NOISE_ERROR(noise_cipherstate_encrypt(st->tx_cipher, &noise_buf), "encrypting data");
diff --git a/src/noise.h b/src/noise.h
index 672174f..3f56854 100644
--- a/src/noise.h
+++ b/src/noise.h
@@ -45,9 +45,12 @@ int start_protocol_handshake(struct NoiseState *st);
 int reset_protocol_handshake(struct NoiseState *st);
 int generate_identity_key(struct NoiseState *st);
 int try_continue_noise_handshake(struct NoiseState * const st, uint8_t *buf, size_t len);
-int send_encrypted_message(struct NoiseState *st, uint8_t *msg, size_t len);
+int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len);
 
+/*@ assigns \nothing; */
 void arm_key_scrubber(void);
+
+/*@ assigns \nothing; */
 void disarm_key_scrubber(void);
 
 #endif
diff --git a/src/packet_interface.h b/src/packet_interface.h
index 4d1be07..86afb0e 100644
--- a/src/packet_interface.h
+++ b/src/packet_interface.h
@@ -46,6 +46,13 @@ struct control_packet {
 } __attribute__((__packed__));
 
 
+/*@
+    requires \valid(f);
+    requires \valid_read(data + (0..len-1));
+    requires len > 0;
+
+    assigns \nothing;
+ */
 void send_packet(struct dma_usart_file *f, const uint8_t *data, size_t len);
 
 #endif