From 0f26179409297c921b4b7ffd9d6379bab84f964b Mon Sep 17 00:00:00 2001 From: jaseg Date: Mon, 17 Dec 2018 22:51:47 +0900 Subject: Document function specs some more --- src/cobs.c | 1 - src/noise.c | 115 ++++++++++++++++++++++++++++++------------------------------ 2 files changed, 57 insertions(+), 59 deletions(-) diff --git a/src/cobs.c b/src/cobs.c index d3889c3..19dcad2 100644 --- a/src/cobs.c +++ b/src/cobs.c @@ -73,7 +73,6 @@ ssize_t cobs_encode(char *dst, size_t dstlen, char *src, size_t srclen) { } /*@ requires \valid_read(src + (0..srclen-1)); - @ requires srclen < 1000000-2; @*/ #ifndef VERIFICATION int cobs_encode_incremental(void *f, int (*output)(void *f, unsigned char c), unsigned char *src, size_t srclen) { diff --git a/src/noise.c b/src/noise.c index 949a68d..1d545f4 100644 --- a/src/noise.c +++ b/src/noise.c @@ -51,12 +51,13 @@ volatile int host_packet_length = 0; /*@ - requires \valid(st); + requires validity: \valid(st); + + ensures equal: st->remote_key_reference == remote_key_reference && st->local_key == local_key; + ensures equal: st->handshake_state == HANDSHAKE_UNINITIALIZED; + ensures equal: st->failed_handshakes == 0; + ensures equal: st->tx_cipher == NULL && st->rx_cipher == NULL && st->handshake == NULL; - ensures st->remote_key_reference == remote_key_reference && st->local_key == local_key; - 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) { @@ -71,21 +72,18 @@ void noise_state_init(struct NoiseState *st, uint8_t *remote_key_reference, uint } /*@ - requires \valid(st); - requires \valid(st->handshake_hash + (0..31)); - requires \separated(st, st->rx_cipher, st->tx_cipher, st->handshake); + requires validity: \valid(st) && \valid(st->handshake_hash + (0..31)) && \valid_read(st->local_key + (0..31)); + requires separation: \separated(st, st->rx_cipher, st->tx_cipher, st->handshake); - ensures \result == 0 ==> ( + ensures result: \result \in {0, -1}; + ensures success: \result == 0 ==> ( \valid(st->handshake) && (st->handshake_state == HANDSHAKE_IN_PROGRESS)); - - ensures \result != 0 ==> ( + ensures failure: \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; + assigns *st, *st->rx_cipher, *st->tx_cipher; */ int reset_protocol_handshake(struct NoiseState *st) { uninit_handshake(st, HANDSHAKE_UNINITIALIZED); @@ -95,21 +93,19 @@ int reset_protocol_handshake(struct NoiseState *st) { st->tx_cipher = NULL; st->rx_cipher = NULL; st->handshake = NULL; - memset(st->handshake_hash, 0, sizeof(st->handshake_hash)); + fc_memset_uint8(st->handshake_hash, 0, sizeof(st->handshake_hash)); return start_protocol_handshake(st); } -/*@ requires \valid(st) && \valid_read(st->local_key + (0..31)); +/*@ requires validity: \valid(st) && \valid_read(st->local_key + (0..31)); - ensures \result == 0 ==> ( + ensures result: \result \in {0, -1}; + ensures success: \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}; + st->handshake_state == HANDSHAKE_IN_PROGRESS); + ensures failure: \result != 0 ==> ( + st->handshake == \old(st->handshake) && + st->handshake_state == \old(st->handshake_state)); assigns st->handshake, st->handshake_state; */ @@ -143,9 +139,9 @@ errout: return -1; } -/*@ requires \valid(st); - requires \valid(st->local_key + (0..31)); - requires \separated(st, st->local_key + (0..31)); +/*@ requires validity: \valid(st) && \valid(st->local_key + (0..31)); + requires separation: \separated(st, st->local_key + (0..31)); + assigns st->local_key[0..31]; */ int generate_identity_key(struct NoiseState *st) { @@ -168,14 +164,13 @@ errout: return -1; } -/*@requires \valid(st); - requires new_state == HANDSHAKE_UNINITIALIZED || - new_state == HANDSHAKE_NOT_STARTED || - new_state == HANDSHAKE_IN_PROGRESS || - new_state == HANDSHAKE_DONE_UNKNOWN_HOST || - new_state == HANDSHAKE_DONE_KNOWN_HOST; - ensures st->handshake_state == new_state; - ensures st->handshake == NULL; +/*@requires validity: \valid(st); + requires state_valid: new_state \in + {HANDSHAKE_UNINITIALIZED, HANDSHAKE_NOT_STARTED, HANDSHAKE_IN_PROGRESS, + HANDSHAKE_DONE_UNKNOWN_HOST, HANDSHAKE_DONE_KNOWN_HOST}; + + ensures state: st->handshake_state == new_state; + ensures handshake: st->handshake == NULL; assigns st->handshake, st->handshake_state; @*/ @@ -190,18 +185,25 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) { //@ ghost int key_checked_trace; //@ ghost int key_match_trace; /*@ - requires \valid(st); - requires \valid(usart2_out); - requires \valid(st->handshake); + requires validity: \valid(st) && \valid(usart2_out) && \valid(st->handshake); + + requires validity: \valid(st->remote_key + (0..sizeof(st->remote_key)-1)); + requires validity: \valid(st->handshake_hash + (0..sizeof(st->handshake_hash)-1)); + + requires separation: \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash); - requires \valid(st->remote_key + (0..sizeof(st->remote_key)-1)); - requires \valid(st->handshake_hash + (0..sizeof(st->handshake_hash)-1)); + ensures result: \result \in {0, -1}; - requires \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash); + ensures state_legal: st->handshake_state \in + {HANDSHAKE_UNINITIALIZED, HANDSHAKE_IN_PROGRESS, HANDSHAKE_DONE_KNOWN_HOST, HANDSHAKE_DONE_UNKNOWN_HOST}; + ensures transition_legal_advance: (\old(st->handshake_state) != HANDSHAKE_IN_PROGRESS) + ==> st->handshake_state == HANDSHAKE_UNINITIALIZED; + ensures transition_legal_failure: st->handshake_state == HANDSHAKE_UNINITIALIZED <==> \result == -1; - ensures (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_checked_trace == 1; - ensures (st->handshake_state != HANDSHAKE_IN_PROGRESS) ==> + ensures permission_valid: (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_checked_trace == 1; + ensures state_advance_condition: (st->handshake_state != HANDSHAKE_IN_PROGRESS) ==> key_match_trace == 1 || (st->failed_handshakes > \old(st->failed_handshakes)); + @*/ int try_continue_noise_handshake(struct NoiseState * const st, uint8_t *buf, size_t len) { //@ ghost key_checked_trace = 0; @@ -303,11 +305,11 @@ errout: } /*@ - requires \valid(st); - requires \valid_read(st->remote_key + (0..sizeof(st->remote_key)-1)); - requires \valid(st->remote_key_reference + (0..31)); + requires validity: \valid(st); + requires validity: \valid_read(st->remote_key + (0..sizeof(st->remote_key)-1)); + requires validity: \valid(st->remote_key_reference + (0..31)); - ensures st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST; + ensures state: st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST; assigns st->remote_key_reference[0..31], st->handshake_state; */ void persist_remote_key(struct NoiseState *st) { @@ -319,14 +321,11 @@ void persist_remote_key(struct NoiseState *st) { } /*@ - requires \valid(st); - requires \valid(usart2_out); - requires \valid(st->tx_cipher); - requires \valid_read(msg + (0..len-1)); - requires 0 <= len <= 65536; + requires validity: \valid(st) && \valid(usart2_out) && \valid(st->tx_cipher) && \valid_read(msg + (0..len-1)); + ensures length: !(0 <= len <= MAX_HOST_PACKET_SIZE) <==> \result == -3; ensures \result \in {0, -1, -2, -3}; - assigns *st->tx_cipher; + assigns *st->tx_cipher, *usart2_out; */ int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len) { int err; @@ -336,16 +335,16 @@ int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len uint8_t payload[MAX_HOST_PACKET_SIZE]; } pkt; - if (!st->tx_cipher) { - LOG_PRINTF("Cannot send encrypted packet: Data ciphers not yet initialized\n"); - return -1; - } - if (len > sizeof(pkt.payload)) { LOG_PRINTF("Packet too long\n"); return -3; } + if (!st->tx_cipher) { + LOG_PRINTF("Cannot send encrypted packet: Data ciphers not yet initialized\n"); + return -1; + } + pkt.header.type = HOST_DATA; 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)); -- cgit