summaryrefslogtreecommitdiff
path: root/fw/src/noise.c
diff options
context:
space:
mode:
Diffstat (limited to 'fw/src/noise.c')
-rw-r--r--fw/src/noise.c34
1 files changed, 17 insertions, 17 deletions
diff --git a/fw/src/noise.c b/fw/src/noise.c
index bd0974c..90aaf36 100644
--- a/fw/src/noise.c
+++ b/fw/src/noise.c
@@ -192,15 +192,15 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) {
}
/*@
- requires validity: \valid(st) && \valid(usart2_out) && \valid(st->handshake);
+ requires validity: \valid(st) && \valid(uart4_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);
+ requires separation: \separated(uart4_out, st, buf, st->handshake);
ensures \result \in {-1, 0};
- assigns *usart2_out, *st->handshake;
+ assigns *uart4_out, *st->handshake;
@*/
int handshake_phase1(struct NoiseState * const st, uint8_t *buf, size_t len) {
int err;
@@ -218,7 +218,7 @@ int handshake_phase1(struct NoiseState * const st, uint8_t *buf, size_t len) {
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));
+ send_packet(uart4_out, (uint8_t *)&pkt, noise_msg.size + sizeof(pkt.header));
return 0;
errout: /* for HANDLE_NOISE_ERROR macro */
@@ -228,14 +228,14 @@ errout: /* for HANDLE_NOISE_ERROR macro */
//@ ghost int key_checked_trace;
//@ ghost int key_match_trace;
/*@
- requires validity: \valid(st) && \valid(usart2_out) && \valid(st->handshake);
+ requires validity: \valid(st) && \valid(uart4_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 separation: \separated(uart4_out, st);
requires sanity: 0 <= st->failed_handshakes < 100;
- requires separation: \separated(&usart2_out, st, buf, st->handshake);
+ requires separation: \separated(&uart4_out, st, buf, st->handshake);
ensures result: \result \in {-1, 0, 1};
ensures sanity: 0 <= st->failed_handshakes <= 102;
@@ -244,7 +244,7 @@ errout: /* for HANDLE_NOISE_ERROR macro */
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;
+ assigns *uart4_out, *st, *st->handshake, key_checked_trace, key_match_trace;
@*/
int handshake_phase2(struct NoiseState * const st, uint8_t *buf, size_t len) {
//@ ghost int old_failed_handshakes = st->failed_handshakes;
@@ -288,7 +288,7 @@ int handshake_phase2(struct NoiseState * const st, uint8_t *buf, size_t len) {
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_update(&bc, st->remote_key, sizeof(st->remote_key));
BLAKE2s_finish(&bc, remote_fp);
//@ ghost key_checked_trace = 1;
@@ -319,13 +319,13 @@ errout:
return -1;
}
/*@
- requires validity: \valid(st) && \valid(usart2_out) && \valid(st->handshake);
+ requires validity: \valid(st) && \valid(uart4_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;
- requires separation: \separated(usart2_out, st, buf, st->handshake);
+ requires separation: \separated(uart4_out, st, buf, st->handshake);
ensures result: \result \in {0, -1};
@@ -343,7 +343,7 @@ errout:
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 *uart4_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) {
@@ -400,18 +400,18 @@ errout:
void persist_remote_key(struct NoiseState *st) {
BLAKE2s_context_t bc;
BLAKE2s_reset(&bc);
- fc_BLAKE2s_update_uint8(&bc, st->remote_key, sizeof(st->remote_key));
+ BLAKE2s_update(&bc, st->remote_key, sizeof(st->remote_key));
BLAKE2s_finish(&bc, st->remote_key_reference);
st->handshake_state = HANDSHAKE_DONE_KNOWN_HOST;
}
/*@
- requires validity: \valid(st) && \valid(usart2_out) && \valid(st->tx_cipher) && \valid_read(msg + (0..len-1));
- requires separation: \separated(usart2_out, st);
+ requires validity: \valid(st) && \valid(uart4_out) && \valid(st->tx_cipher) && \valid_read(msg + (0..len-1));
+ requires separation: \separated(uart4_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;
+ assigns *st->tx_cipher, *uart4_out;
*/
int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len) {
int err;
@@ -436,7 +436,7 @@ int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len
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");
- send_packet(usart2_out, (uint8_t *)&pkt, noise_buf.size + sizeof(pkt.header));
+ send_packet(uart4_out, (uint8_t *)&pkt, noise_buf.size + sizeof(pkt.header));
return 0;
errout:
generated by cgit (git 2.34.1) at 2024-05-18 10:01:45 +0000