diff options
| -rw-r--r-- | src/noise.c | 260 | ||||
| -rw-r--r-- | src/noise.h | 4 |
2 files changed, 175 insertions, 89 deletions
diff --git a/src/noise.c b/src/noise.c index 1d545f4..bd0974c 100644 --- a/src/noise.c +++ b/src/noise.c @@ -40,9 +40,19 @@ uint8_t *fc_memset_uint8(uint8_t *s, int c, size_t n); @*/ uint8_t *fc_memcpy_uint8(uint8_t *dest, const uint8_t *src, size_t n); +/*@ requires valid_s1: \valid_read(s1 + (0..n-1)); + @ requires valid_s2: \valid_read(s2 + (0..n-1)); + @ assigns \result \from + @ indirect:s1[0.. n-1], indirect:s2[0.. n-1]; + @ ensures logic_spec: \result == 0 <==> ( + \forall integer i; 0 <= i <= n-1 ==> s1[i] == s2[i]); + @*/ +int fc_memcmp_uint8(const uint8_t *s1, const uint8_t *s2, size_t n); + #else #define fc_memset_uint8 memset #define fc_memcpy_uint8 memcpy +#define fc_memcmp_uint8 memcmp #endif @@ -78,10 +88,11 @@ void noise_state_init(struct NoiseState *st, uint8_t *remote_key_reference, uint ensures result: \result \in {0, -1}; ensures success: \result == 0 ==> ( \valid(st->handshake) && - (st->handshake_state == HANDSHAKE_IN_PROGRESS)); + (st->handshake_state == HANDSHAKE_PHASE1)); ensures failure: \result != 0 ==> ( (st->handshake == NULL) && (st->handshake_state == HANDSHAKE_UNINITIALIZED)); + ensures unmodified: \old(st->failed_handshakes) == st->failed_handshakes; assigns *st, *st->rx_cipher, *st->tx_cipher; */ @@ -102,7 +113,7 @@ int reset_protocol_handshake(struct NoiseState *st) { ensures result: \result \in {0, -1}; ensures success: \result == 0 ==> ( \valid(st->handshake) && - st->handshake_state == HANDSHAKE_IN_PROGRESS); + st->handshake_state == HANDSHAKE_PHASE1); ensures failure: \result != 0 ==> ( st->handshake == \old(st->handshake) && st->handshake_state == \old(st->handshake_state)); @@ -131,7 +142,7 @@ int start_protocol_handshake(struct NoiseState *st) { HANDLE_NOISE_ERROR(noise_handshakestate_start(handshake), "starting handshake"); st->handshake = handshake; - st->handshake_state = HANDSHAKE_IN_PROGRESS; + st->handshake_state = HANDSHAKE_PHASE1; return 0; errout: @@ -140,7 +151,6 @@ errout: } /*@ 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]; */ @@ -166,8 +176,7 @@ errout: /*@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}; + {HANDSHAKE_UNINITIALIZED, HANDSHAKE_DONE_UNKNOWN_HOST, HANDSHAKE_DONE_KNOWN_HOST}; ensures state: st->handshake_state == new_state; ensures handshake: st->handshake == NULL; @@ -182,117 +191,193 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) { arm_key_scrubber(); } -//@ ghost int key_checked_trace; -//@ ghost int key_match_trace; /*@ 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 separation: \separated(usart2_out, st, buf, st->handshake); - ensures result: \result \in {0, -1}; + ensures \result \in {-1, 0}; - 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; + assigns *usart2_out, *st->handshake; + @*/ +int handshake_phase1(struct NoiseState * const st, uint8_t *buf, size_t len) { + int err; + struct { + struct control_packet header; + uint8_t payload[MAX_HOST_PACKET_SIZE]; + } pkt; + NoiseBuffer noise_msg; - 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)); + /* Read the next handshake message and discard the payload */ + noise_buffer_set_input(noise_msg, buf, len); + HANDLE_NOISE_ERROR(noise_handshakestate_read_message(st->handshake, &noise_msg, NULL), "reading handshake message"); + /* Write the next handshake message with a zero-length noise payload */ + pkt.header.type = HOST_HANDSHAKE; + noise_buffer_set_output(noise_msg, &pkt.payload, sizeof(pkt.payload)); + HANDLE_NOISE_ERROR(noise_handshakestate_write_message(st->handshake, &noise_msg, NULL), "writing handshake message"); + send_packet(usart2_out, (uint8_t *)&pkt, noise_msg.size + sizeof(pkt.header)); + + return 0; +errout: /* for HANDLE_NOISE_ERROR macro */ + return -1; +} + +//@ ghost int key_checked_trace; +//@ ghost int key_match_trace; +/*@ + 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_read(st->remote_key_reference + (0..sizeof(st->remote_key)-1)); + requires validity: \valid(st->handshake_hash + (0..sizeof(st->handshake_hash)-1)); + requires separation: \separated(usart2_out, st); + requires sanity: 0 <= st->failed_handshakes < 100; + + requires separation: \separated(&usart2_out, st, buf, st->handshake); + + ensures result: \result \in {-1, 0, 1}; + ensures sanity: 0 <= st->failed_handshakes <= 102; + ensures sanity: \result != 1 ==> st->failed_handshakes >= \old(st->failed_handshakes); + + ensures permission_valid: \result != -1 ==> key_checked_trace == 1; + ensures permission_valid: \result == 1 ==> key_match_trace == 1; + // + assigns *usart2_out, *st, *st->handshake, key_checked_trace, key_match_trace; @*/ -int try_continue_noise_handshake(struct NoiseState * const st, uint8_t *buf, size_t len) { - //@ ghost key_checked_trace = 0; - //@ ghost key_match_trace = 0; +int handshake_phase2(struct NoiseState * const st, uint8_t *buf, size_t len) { + //@ ghost int old_failed_handshakes = st->failed_handshakes; int err; struct { struct control_packet header; uint8_t payload[MAX_HOST_PACKET_SIZE]; } pkt; NoiseBuffer noise_msg; + //@ ghost key_checked_trace = 0; + // ghost key_match_trace = 0; - if (!st->handshake || st->handshake_state != HANDSHAKE_IN_PROGRESS) { - LOG_PRINTF("Error: Invalid handshake state\n"); + /* Read the next handshake message and discard the payload */ + noise_buffer_set_input(noise_msg, buf, len); + HANDLE_NOISE_ERROR(noise_handshakestate_read_message(st->handshake, &noise_msg, NULL), "reading handshake message"); + + HANDLE_NOISE_ERROR(noise_handshakestate_split(st->handshake, &st->tx_cipher, &st->rx_cipher), "splitting handshake state"); + LOG_PRINTF("Noise protocol handshake completed successfully, handshake hash:\n"); + + if (noise_handshakestate_get_handshake_hash(st->handshake, st->handshake_hash, sizeof(st->handshake_hash)) != NOISE_ERROR_NONE) { + LOG_PRINTF("Error fetching noise handshake state\n"); goto errout; + } else { + LOG_PRINTF(" "); + /*@ loop assigns i; @*/ + for (size_t i=0; i<sizeof(st->handshake_hash); i++) + LOG_PRINTF("%02x ", st->handshake_hash[i]); + LOG_PRINTF("\n"); } - /* Run the protocol handshake */ - switch (noise_handshakestate_get_action(st->handshake)) { - case NOISE_ACTION_WRITE_MESSAGE: - /* Write the next handshake message with a zero-length noise payload */ - pkt.header.type = HOST_HANDSHAKE; - noise_buffer_set_output(noise_msg, &pkt.payload, sizeof(pkt.payload)); - HANDLE_NOISE_ERROR(noise_handshakestate_write_message(st->handshake, &noise_msg, NULL), "writing handshake message"); - send_packet(usart2_out, (uint8_t *)&pkt, noise_msg.size + sizeof(pkt.header)); - if (buf) { - LOG_PRINTF("Warning: dropping unneeded host buffer of length %d bytes\n", len); - } - break; + + NoiseDHState *remote_dh = noise_handshakestate_get_remote_public_key_dh(st->handshake); + if (!remote_dh) { + LOG_PRINTF("Error: Host has not identified itself\n"); + goto errout; + } - case NOISE_ACTION_READ_MESSAGE: - if (buf) { - /* Read the next handshake message and discard the payload */ - noise_buffer_set_input(noise_msg, buf, len); - HANDLE_NOISE_ERROR(noise_handshakestate_read_message(st->handshake, &noise_msg, NULL), "reading handshake message"); - } - break; + HANDLE_NOISE_ERROR(noise_dhstate_get_public_key(remote_dh, st->remote_key, sizeof(st->remote_key)), "getting remote pubkey"); - case NOISE_ACTION_SPLIT: - HANDLE_NOISE_ERROR(noise_handshakestate_split(st->handshake, &st->tx_cipher, &st->rx_cipher), "splitting handshake state"); - LOG_PRINTF("Noise protocol handshake completed successfully, handshake hash:\n"); + /* TODO support list of known remote hosts here instead of just one */ + uint8_t remote_fp[BLAKE2S_HASH_SIZE]; + BLAKE2s_context_t bc; + BLAKE2s_reset(&bc); + fc_BLAKE2s_update_uint8(&bc, st->remote_key, sizeof(st->remote_key)); + BLAKE2s_finish(&bc, remote_fp); + + //@ ghost key_checked_trace = 1; + if (!fc_memcmp_uint8(remote_fp, st->remote_key_reference, sizeof(remote_fp))) { /* keys match */ + //@ ghost key_match_trace = 1; + uint8_t response = REPORT_PAIRING_SUCCESS; + if (send_encrypted_message(st, &response, sizeof(response))) + LOG_PRINTF("Error sending pairing response packet\n"); + + st->failed_handshakes = 0; + //@ assert 0 <= st->failed_handshakes <= 102; + return 1; + + } else { /* keys don't match */ + uint8_t response = REPORT_PAIRING_START; + if (send_encrypted_message(st, &response, sizeof(response))) + LOG_PRINTF("Error sending pairing response packet\n"); + + st->failed_handshakes++; + //@ assert 0 <= st->failed_handshakes <= 102; + //@ assert st->failed_handshakes >= old_failed_handshakes; + return 0; + } - //@ assert \valid(&st->handshake); - if (noise_handshakestate_get_handshake_hash(st->handshake, st->handshake_hash, sizeof(st->handshake_hash)) != NOISE_ERROR_NONE) { - LOG_PRINTF("Error fetching noise handshake state\n"); - } else { - LOG_PRINTF(" "); - for (size_t i=0; i<sizeof(st->handshake_hash); i++) - LOG_PRINTF("%02x ", st->handshake_hash[i]); - LOG_PRINTF("\n"); - } +errout: + //@ assert 0 <= st->failed_handshakes <= 102; + //@ assert st->failed_handshakes >= old_failed_handshakes; + return -1; +} +/*@ + 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->remote_key_reference + (0..sizeof(st->remote_key)-1)); + requires validity: \valid(st->handshake_hash + (0..sizeof(st->handshake_hash)-1)); + requires sanity: 0 <= st->failed_handshakes < 100; - - //@ assert \valid(&st->handshake); - NoiseDHState *remote_dh = noise_handshakestate_get_remote_public_key_dh(st->handshake); - if (!remote_dh) { - LOG_PRINTF("Error: Host has not identified itself\n"); - goto errout; - } + requires separation: \separated(usart2_out, st, buf, st->handshake); - HANDLE_NOISE_ERROR(noise_dhstate_get_public_key(remote_dh, st->remote_key, sizeof(st->remote_key)), "getting remote pubkey"); + ensures result: \result \in {0, -1}; - /* TODO support list of known remote hosts here instead of just one */ - uint8_t remote_fp[BLAKE2S_HASH_SIZE]; - BLAKE2s_context_t bc; - BLAKE2s_reset(&bc); - fc_BLAKE2s_update_uint8(&bc, st->remote_key, sizeof(st->remote_key)); - BLAKE2s_finish(&bc, remote_fp); + ensures state_legal: st->handshake_state \in + {HANDSHAKE_UNINITIALIZED, HANDSHAKE_PHASE1, HANDSHAKE_PHASE2, + HANDSHAKE_DONE_KNOWN_HOST, HANDSHAKE_DONE_UNKNOWN_HOST}; + ensures transition_legal: + \result != -1 ==> \old(st->handshake_state) \in {HANDSHAKE_PHASE1, HANDSHAKE_PHASE2}; + ensures transition_legal: (\old(st->handshake_state) == HANDSHAKE_PHASE1) + ==> st->handshake_state \in {HANDSHAKE_PHASE2, HANDSHAKE_UNINITIALIZED}; + ensures transition_legal: (\old(st->handshake_state) == HANDSHAKE_PHASE2) + ==> st->handshake_state \in {HANDSHAKE_DONE_KNOWN_HOST, HANDSHAKE_DONE_UNKNOWN_HOST, HANDSHAKE_UNINITIALIZED}; + ensures failure_handling: \result == -1 <==> st->handshake_state == HANDSHAKE_UNINITIALIZED; + ensures failure_handling: \result == -1 ==> st->failed_handshakes > \old(st->failed_handshakes); + + ensures state_advance_condition: (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_match_trace == 1; + + //assigns *usart2_out, *st, *st->rx_cipher, *st->tx_cipher, *st->handshake; + //assigns key_checked_trace, key_match_trace; + @*/ +int try_continue_noise_handshake(struct NoiseState * const st, uint8_t *buf, size_t len) { + //@ ghost key_checked_trace = 0; + //@ ghost key_match_trace = 0; + int rc; - //@ ghost key_checked_trace = 1; - if (!memcmp(remote_fp, st->remote_key_reference, sizeof(remote_fp))) { /* keys match */ - //@ ghost key_match_trace = 1; - uint8_t response = REPORT_PAIRING_SUCCESS; - if (send_encrypted_message(st, &response, sizeof(response))) - LOG_PRINTF("Error sending pairing response packet\n"); + if (!st->handshake) { + LOG_PRINTF("Error: Invalid handshake state\n"); + goto errout; + } - uninit_handshake(st, HANDSHAKE_DONE_KNOWN_HOST); - st->failed_handshakes = 0; + /* Run the protocol handshake */ + switch (st->handshake_state) { + case HANDSHAKE_PHASE1: + if (handshake_phase1(st, buf, len)) + goto errout; - } else { /* keys don't match */ - uint8_t response = REPORT_PAIRING_START; - if (send_encrypted_message(st, &response, sizeof(response))) - LOG_PRINTF("Error sending pairing response packet\n"); + st->handshake_state = HANDSHAKE_PHASE2; + return 0; + case HANDSHAKE_PHASE2: + rc = handshake_phase2(st, buf, len); + if (rc < 0) + goto errout; + + if (rc == 1) + uninit_handshake(st, HANDSHAKE_DONE_KNOWN_HOST); + else uninit_handshake(st, HANDSHAKE_DONE_UNKNOWN_HOST); - st->failed_handshakes++; - } break; default: + LOG_PRINTF("Invalid handshake state\n"); goto errout; } @@ -321,11 +406,12 @@ void persist_remote_key(struct NoiseState *st) { } /*@ - requires validity: \valid(st) && \valid(usart2_out) && \valid(st->tx_cipher) && \valid_read(msg + (0..len-1)); + requires validity: \valid(st) && \valid(usart2_out) && \valid(st->tx_cipher) && \valid_read(msg + (0..len-1)); + requires separation: \separated(usart2_out, st); - ensures length: !(0 <= len <= MAX_HOST_PACKET_SIZE) <==> \result == -3; - ensures \result \in {0, -1, -2, -3}; - assigns *st->tx_cipher, *usart2_out; + ensures length: !(0 <= len <= MAX_HOST_PACKET_SIZE) <==> \result == -3; + ensures \result \in {0, -1, -2, -3}; + assigns *st->tx_cipher, *usart2_out; */ int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len) { int err; diff --git a/src/noise.h b/src/noise.h index 3f56854..1969945 100644 --- a/src/noise.h +++ b/src/noise.h @@ -18,8 +18,8 @@ extern volatile int host_packet_length; enum handshake_state { HANDSHAKE_UNINITIALIZED, - HANDSHAKE_NOT_STARTED, - HANDSHAKE_IN_PROGRESS, + HANDSHAKE_PHASE1, + HANDSHAKE_PHASE2, HANDSHAKE_DONE_UNKNOWN_HOST, HANDSHAKE_DONE_KNOWN_HOST, }; |