From 40e9fb8153a218a243cff749d7d0b4e82d70ae94 Mon Sep 17 00:00:00 2001 From: jaseg Date: Mon, 17 Dec 2018 12:26:51 +0900 Subject: Invocation of noise.c from demo.c mostly proving in frama-c --- src/demo.c | 57 +++++++++++++++++++++++++++++++------------------- src/frama_c_cmdline | 1 + src/noise.c | 19 +++++++++-------- src/packet_interface.h | 2 +- src/tracing.h | 5 +++++ 5 files changed, 53 insertions(+), 31 deletions(-) create mode 100644 src/frama_c_cmdline diff --git a/src/demo.c b/src/demo.c index 0e16d5e..4d6a040 100644 --- a/src/demo.c +++ b/src/demo.c @@ -20,20 +20,6 @@ * */ -#include "usart_helpers.h" -#include "usbh_core.h" -#include "usbh_lld_stm32f4.h" -#include "usbh_driver_hid.h" -#include "usbh_driver_hub.h" -#include "rand_stm32.h" -#include "packet_interface.h" -#include "noise.h" -#include "hid_keycodes.h" -#include "words.h" -#include "tracing.h" - -#include "crypto/noise-c/src/protocol/internal.h" - #include #include #include @@ -49,6 +35,20 @@ #include #include +#include "usart_helpers.h" +#include "usbh_core.h" +#include "usbh_lld_stm32f4.h" +#include "usbh_driver_hid.h" +#include "usbh_driver_hub.h" +#include "rand_stm32.h" +#include "packet_interface.h" +#include "noise.h" +#include "hid_keycodes.h" +#include "words.h" +#include "tracing.h" + +#include "crypto/noise-c/src/protocol/internal.h" + #ifndef USE_STM32F4_USBH_DRIVER_FS #error The full-speed USB driver must be enabled with USE_STM32F4_USBH_DRIVER_FS in usbh_config.h! #endif @@ -439,7 +439,8 @@ void usart1_isr(void) { if (USART1_SR & USART_SR_ORE) { /* Overrun handling */ LOG_PRINTF("USART1 data register overrun\n"); /* Clear interrupt flag */ - return (void)USART1_DR; + int dummy = USART1_DR; + return; } uint8_t data = USART1_DR; /* This automatically acknowledges the IRQ */ @@ -487,7 +488,17 @@ void DMA_ISR(DEBUG_USART_DMA_NUM, DEBUG_USART_DMA_STREAM_NUM)(void) { TRACING_CLEAR(TR_DEBUG_OUT_DMA_IRQ); } -void handle_host_packet(struct control_packet *pkt, size_t payload_length) { +/*@ requires \valid_read(&pkt->type) && \valid_read(pkt->payload + (0..payload_length-1)); + requires \valid(st); + requires \valid(st->handshake); + requires \separated(st, st->rx_cipher, st->tx_cipher, st->handshake, (uint8_t *)pkt->payload, &usart2_out, &st->handshake_hash); + requires \valid(usart2_out); + + assigns pairing_buf_pos, *usart2_out, *st; + + assigns st->handshake, st->handshake_state, st->rx_cipher, st->tx_cipher; + @*/ +void handle_host_packet(struct NoiseState *st, const struct control_packet *pkt, size_t payload_length) { TRACING_SET(TR_HOST_PKT_HANDLER); if (pkt->type == HOST_INITIATE_HANDSHAKE) { /* It is important that we acknowledge this command right away. Starting the handshake involves key @@ -496,9 +507,9 @@ void handle_host_packet(struct control_packet *pkt, size_t payload_length) { if (payload_length > 0) { LOG_PRINTF("Extraneous data in INITIATE_HANDSHAKE message\n"); - } else if (noise_state.failed_handshakes < MAX_FAILED_HANDSHAKES) { + } else if (st->failed_handshakes < MAX_FAILED_HANDSHAKES) { LOG_PRINTF("Starting noise protocol handshake...\n"); - if (reset_protocol_handshake(&noise_state)) + if (reset_protocol_handshake(st)) LOG_PRINTF("Error starting protocol handshake.\n"); pairing_buf_pos = 0; /* Reset channel binding keyboard input buffer */ } else { @@ -510,7 +521,7 @@ void handle_host_packet(struct control_packet *pkt, size_t payload_length) { } else if (pkt->type == HOST_HANDSHAKE) { LOG_PRINTF("Handling handshake packet of length %d\n", payload_length); TRACING_SET(TR_NOISE_HANDSHAKE); - if (try_continue_noise_handshake(&noise_state, pkt->payload, payload_length)) { + if (try_continue_noise_handshake(st, pkt->payload, payload_length)) { TRACING_CLEAR(TR_NOISE_HANDSHAKE); LOG_PRINTF("Reporting handshake error to host\n"); struct control_packet out = { .type=HOST_CRYPTO_ERROR }; @@ -565,7 +576,11 @@ int main(void) LOG_PRINTF("Initializing RNG...\n"); rand_init(); + //@ assert \valid(&noise_state); + //@ assert \valid((uint8_t *)keystore.keys.remote_key_reference + (0..31)) && \valid((uint8_t *)keystore.keys.local_key + (0..31)); noise_state_init(&noise_state, keystore.keys.remote_key_reference, keystore.keys.local_key); + + //@ assert \valid(noise_state.local_key + (0..31)); /* FIXME load remote key from backup memory */ /* FIXME only run this on first boot and persist key in backup sram. Allow reset via jumper-triggered factory reset function. */ if (!keystore.mgmt.identity_key_valid) { @@ -633,13 +648,13 @@ int main(void) } if (host_packet_length > 0) { - handle_host_packet((struct control_packet *)host_packet_buf, host_packet_length - 1); + handle_host_packet(&noise_state, (struct control_packet *)host_packet_buf, host_packet_length - 1); host_packet_length = 0; /* Acknowledge to USART ISR the buffer has been handled */ } else if (host_packet_length < 0) { /* USART error */ host_packet_length = 0; /* Acknowledge to USART ISR the error has been handled */ if (noise_state.handshake_state < HANDSHAKE_DONE_UNKNOWN_HOST) { - LOG_PRINTF("USART error, aborting handshake\n") + LOG_PRINTF("USART error, aborting handshake\n"); struct control_packet pkt = { .type=HOST_COMM_ERROR }; send_packet(usart2_out, (uint8_t *)&pkt, sizeof(pkt)); diff --git a/src/frama_c_cmdline b/src/frama_c_cmdline new file mode 100644 index 0000000..d6c6adc --- /dev/null +++ b/src/frama_c_cmdline @@ -0,0 +1 @@ +frama-c-gui -c11 -cpp-extra-args="-DVERIFICATION -DSTM32F4 -DUSE_STM32F4_USBH_DRIVER_FS -DDEBUG_USART=USART1 -DDEBUG_USART_BAUDRATE=115200 -DDEBUG_USART_DMA_CHANNEL_NUM=4 -DDEBUG_USART_DMA_NUM=2 -DDEBUG_USART_DMA_STREAM_NUM=7 -I. -I"(frama-c -print-path)"/libc -I crypto/noise-c/include -I../include -I../libopencm3/include" -wp -wp-rte -wp-model +cint -wp-verbose 2 -slevel 8 -wp-out goals noise.c demo.c -wp-fct try_continue_noise_handshake diff --git a/src/noise.c b/src/noise.c index e03fc45..890b5b5 100644 --- a/src/noise.c +++ b/src/noise.c @@ -52,9 +52,8 @@ 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->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; @@ -74,7 +73,7 @@ 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->handshake_hash + (0..31), st, st->rx_cipher, st->tx_cipher, st->handshake); + requires \separated(st, st->rx_cipher, st->tx_cipher, st->handshake); ensures \result == 0 ==> ( \valid(st->handshake) && @@ -188,9 +187,9 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) { arm_key_scrubber(); } -//@ ghost int key_checked_trace = 0; -//@ ghost int key_match_trace = 0; -/*@ requires empty_trace: key_checked_trace == 0; +//@ ghost int key_checked_trace; +//@ ghost int key_match_trace; +/*@ requires \valid(st); requires \valid(usart2_out); requires \valid(st->handshake); @@ -198,15 +197,17 @@ void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) { requires \valid(st->remote_key + (0..sizeof(st->remote_key)-1)); requires \valid(st->handshake_hash + (0..sizeof(st->handshake_hash)-1)); - requires \separated(st, buf); - requires \separated(&usart2_out, \union(st, buf)); - requires \separated(&st->handshake, st); + requires \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash); + assigns key_checked_trace; + ensures (st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST) ==> key_checked_trace == 1; ensures (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; + //@ ghost key_match_trace = 0; int err; struct { struct control_packet header; diff --git a/src/packet_interface.h b/src/packet_interface.h index 86afb0e..35e9758 100644 --- a/src/packet_interface.h +++ b/src/packet_interface.h @@ -51,7 +51,7 @@ struct control_packet { requires \valid_read(data + (0..len-1)); requires len > 0; - assigns \nothing; + assigns *f; */ void send_packet(struct dma_usart_file *f, const uint8_t *data, size_t len); diff --git a/src/tracing.h b/src/tracing.h index 9aa9216..1970556 100644 --- a/src/tracing.h +++ b/src/tracing.h @@ -3,8 +3,13 @@ #include +#ifndef VERIFICATION #define TRACING_SET(i) gpio_set(GPIOD, (1<