Fix up firmware and demos

This commit is contained in:
jaseg 2021-03-23 19:04:11 +01:00
parent 88379634a8
commit 32da9c4e8c
22 changed files with 563 additions and 342 deletions

20
fw/.gdbinit Normal file
View file

@ -0,0 +1,20 @@
target remote localhost:3333
set print pretty on
set print elements 512
# Update GDB's Python paths with the `sys.path` values of the local Python installation,
# whether that is brew'ed Python, a virtualenv, or another system python.
# Convert GDB to interpret in Python
python
import os,subprocess,sys
# Execute a Python using the user's shell and pull out the sys.path (for site-packages)
paths = subprocess.check_output('python -c "import os,sys;print(os.linesep.join(sys.path).strip())"',shell=True).decode("utf-8").split()
# Extend GDB's Python's search path
sys.path.extend(paths)
end
source upstream/PyCortexMDebug/cmdebug/svd_gdb.py
svd_load upstream/stm32square/svd/STM32F407.svd

3
fw/.gitmodules vendored
View file

@ -1,3 +0,0 @@
[submodule "libopencm3"]
path = libopencm3
url = https://amirhammad@github.com/amirhammad/libopencm3

View file

@ -54,7 +54,7 @@ add_definitions (${CPP_FLAGS})
add_definitions (-DSTM32F4)
set (CMAKE_EXE_LINKER_FLAGS
"--static -nostartfiles -T${CMAKE_SOURCE_DIR}/libusbhost_stm32f4.ld -Wl,-Map=FIXME_ONE.map -Wl,--gc-sections -Wl,--start-group -lc -lgcc -lnosys -Wl,--end-group"
"--static -nostartfiles -L${CMAKE_SOURCE_DIR}/libopencm3/lib -T${CMAKE_SOURCE_DIR}/libusbhost_stm32f4.ld -Wl,-Map=FIXME_ONE.map -Wl,--gc-sections -Wl,--start-group -lc -lgcc -lnosys -Wl,--end-group"
)
include_directories (

View file

@ -16,6 +16,8 @@ from noise.exceptions import NoiseInvalidMessage
import keymap
from hexdump import hexdump
BINDING_INCANTATION_LENGTH = 4
class PacketType(enum.Enum):
_RESERVED = 0
INITIATE_HANDSHAKE = 1
@ -122,7 +124,7 @@ class KeyMapper:
class Magic:
@classmethod
def map_bytes_to_incantation(kls, data):
elems = [ f'{kls.ADJECTIVES[a]} {kls.NOUNS[b]}' for a, b in zip(data[0::2], data[1::2]) ]
elems = [ f'{kls.EVEN[a]} {kls.ODD[b]}' for a, b in zip(data[0::2], data[1::2]) ]
nfirst = ", ".join(elems[:-1])
return f'{nfirst} and {elems[-1]}'
@ -232,6 +234,8 @@ class NoiseEngine:
def perform_handshake(self):
self.packetizer.send_packet(PacketType.INITIATE_HANDSHAKE, b'')
self.debug_print('Handshake started')
import time
time.sleep(0.5) # FIXME
while True:
if self.proto.handshake_finished:
@ -262,7 +266,8 @@ class NoiseEngine:
def channel_binding_incantation(self):
hhash = self.proto.get_handshake_hash()
return '\n'.join(Magic.map_bytes_to_incantation(hhash[i:i+8]) for i in range(0, 16, 8))
#return '\n'.join(Magic.map_bytes_to_incantation(hhash[i:i+8]) for i in range(0, 16, 8))
return '\n'.join(Magic.map_bytes_to_incantation(hhash[i:min(BINDING_INCANTATION_LENGTH, i+8)]) for i in range(0, BINDING_INCANTATION_LENGTH, 8))
def receive_loop(self):
while True:
@ -368,7 +373,8 @@ if __name__ == '__main__':
ser = serial.Serial(args.serial, args.baudrate)
packetizer = Packetizer(ser, debug=args.debug, width=args.width)
noise = NoiseEngine(packetizer, debug=args.debug)
temp_priv_key = NoiseEngine.generate_private_key_x25519()
noise = NoiseEngine(temp_priv_key, packetizer, debug=args.debug)
noise.perform_handshake()
print('Handshake channel binding incantation:')

View file

@ -0,0 +1,23 @@
/* shim file for musl */
#ifndef __MUSL_SHIM_BITS_ALLTYPES_H__
#define __MUSL_SHIM_BITS_ALLTYPES_H__
#define _REDIR_TIME64 1
#define _Addr int
#define _Int64 long long
#define _Reg int
#define __BYTE_ORDER 1234
#define __LONG_MAX 0x7fffffffL
#ifndef __cplusplus
typedef unsigned wchar_t;
#endif
typedef float float_t;
typedef double double_t;
#endif /* __MUSL_SHIM_BITS_ALLTYPES_H__ */

81
fw/include/endian.h Normal file
View file

@ -0,0 +1,81 @@
#ifndef _ENDIAN_H
#define _ENDIAN_H
#include <features.h>
#include <unistd.h>
#define __NEED_uint16_t
#define __NEED_uint32_t
#define __NEED_uint64_t
#include <bits/alltypes.h>
#define __PDP_ENDIAN 3412
#define BIG_ENDIAN __BIG_ENDIAN
#define LITTLE_ENDIAN __LITTLE_ENDIAN
#define PDP_ENDIAN __PDP_ENDIAN
#define BYTE_ORDER __BYTE_ORDER
static __inline uint16_t __bswap16(uint16_t __x)
{
return __x<<8 | __x>>8;
}
static __inline uint32_t __bswap32(uint32_t __x)
{
return __x>>24 | __x>>8&0xff00 | __x<<8&0xff0000 | __x<<24;
}
static __inline uint64_t __bswap64(uint64_t __x)
{
return __bswap32(__x)+0ULL<<32 | __bswap32(__x>>32);
}
#if __BYTE_ORDER == __LITTLE_ENDIAN
#define htobe16(x) __bswap16(x)
#define be16toh(x) __bswap16(x)
#define htobe32(x) __bswap32(x)
#define be32toh(x) __bswap32(x)
#define htobe64(x) __bswap64(x)
#define be64toh(x) __bswap64(x)
#define htole16(x) (uint16_t)(x)
#define le16toh(x) (uint16_t)(x)
#define htole32(x) (uint32_t)(x)
#define le32toh(x) (uint32_t)(x)
#define htole64(x) (uint64_t)(x)
#define le64toh(x) (uint64_t)(x)
#else
#define htobe16(x) (uint16_t)(x)
#define be16toh(x) (uint16_t)(x)
#define htobe32(x) (uint32_t)(x)
#define be32toh(x) (uint32_t)(x)
#define htobe64(x) (uint64_t)(x)
#define be64toh(x) (uint64_t)(x)
#define htole16(x) __bswap16(x)
#define le16toh(x) __bswap16(x)
#define htole32(x) __bswap32(x)
#define le32toh(x) __bswap32(x)
#define htole64(x) __bswap64(x)
#define le64toh(x) __bswap64(x)
#endif
#if defined(_GNU_SOURCE) || defined(_BSD_SOURCE)
#if __BYTE_ORDER == __LITTLE_ENDIAN
#define betoh16(x) __bswap16(x)
#define betoh32(x) __bswap32(x)
#define betoh64(x) __bswap64(x)
#define letoh16(x) (uint16_t)(x)
#define letoh32(x) (uint32_t)(x)
#define letoh64(x) (uint64_t)(x)
#else
#define betoh16(x) (uint16_t)(x)
#define betoh32(x) (uint32_t)(x)
#define betoh64(x) (uint64_t)(x)
#define letoh16(x) __bswap16(x)
#define letoh32(x) __bswap32(x)
#define letoh64(x) __bswap64(x)
#endif
#endif
#endif

40
fw/include/features.h Normal file
View file

@ -0,0 +1,40 @@
#ifndef _FEATURES_H
#define _FEATURES_H
#if defined(_ALL_SOURCE) && !defined(_GNU_SOURCE)
#define _GNU_SOURCE 1
#endif
#if defined(_DEFAULT_SOURCE) && !defined(_BSD_SOURCE)
#define _BSD_SOURCE 1
#endif
#if !defined(_POSIX_SOURCE) && !defined(_POSIX_C_SOURCE) \
&& !defined(_XOPEN_SOURCE) && !defined(_GNU_SOURCE) \
&& !defined(_BSD_SOURCE) && !defined(__STRICT_ANSI__)
#define _BSD_SOURCE 1
#define _XOPEN_SOURCE 700
#endif
#if __STDC_VERSION__ >= 199901L
#define __restrict restrict
#elif !defined(__GNUC__)
#define __restrict
#endif
#if __STDC_VERSION__ >= 199901L || defined(__cplusplus)
#define __inline inline
#elif !defined(__GNUC__)
#define __inline
#endif
#if __STDC_VERSION__ >= 201112L
#elif defined(__GNUC__)
#define _Noreturn __attribute__((__noreturn__))
#else
#define _Noreturn
#endif
#define __REDIR(x,y) __typeof__(x) x __asm__(#y)
#endif

View file

@ -1,4 +1,4 @@
#!/bin/sh
git submodule init
git submodule update
make -C libopencm3 -j3 lib/stm32/f4
#git submodule init
#git submodule update
#make -C libopencm3 -j3 lib/stm32/f4

@ -1 +1 @@
Subproject commit 798c1edf4d11e8a40a7263dc465fa225a63fa7e9
Subproject commit 458250dc6147dc807eec9e4d5a6caf38a699ecb1

View file

@ -31,7 +31,7 @@ MEMORY
}
/* Include the common ld script. */
INCLUDE libopencm3_stm32f4.ld
INCLUDE cortex-m-generic.ld
/* Extra stuff */
SECTIONS

View file

@ -8,7 +8,7 @@ source [find interface/stlink-v2.cfg]
#transport select swd
#source /usr/share/openocd/scripts/target/stm32f0x.cfg
source [find target/stm32f4x_stlink.cfg]
source [find target/stm32f4x.cfg]
init
arm semihosting enable

1
fw/src/crypto/noise-c Submodule

@ -0,0 +1 @@
Subproject commit 604d48fc99b1ae349d4ceb01176a1adf83cb1b31

View file

@ -24,8 +24,8 @@
#include <libopencm3/stm32/gpio.h>
#include <libopencm3/stm32/usart.h>
#include <libopencm3/stm32/timer.h>
#include <libopencm3/stm32/otg_hs.h>
#include <libopencm3/stm32/otg_fs.h>
#include <libopencm3/usb/dwc/otg_hs.h>
#include <libopencm3/usb/dwc/otg_fs.h>
#include <libopencm3/stm32/pwr.h>
#include <libopencm3/stm32/dma.h>
#include <libopencm3/cm3/nvic.h>
@ -87,15 +87,16 @@ static inline void delay(uint32_t n) {
/* Set STM32 to 168 MHz. */
static void clock_setup(void) {
rcc_clock_setup_hse_3v3(&hse_8mhz_3v3[CLOCK_3V3_168MHZ]);
rcc_clock_setup_hse_3v3(&rcc_hse_8mhz_3v3[RCC_CLOCK_3V3_168MHZ]);
rcc_periph_clock_enable(RCC_GPIOA);
rcc_periph_clock_enable(RCC_GPIOB);
rcc_periph_clock_enable(RCC_GPIOC);
rcc_periph_clock_enable(RCC_GPIOD);
rcc_periph_clock_enable(RCC_GPIOE);
rcc_periph_clock_enable(RCC_USART1);
rcc_periph_clock_enable(RCC_USART2);
rcc_periph_clock_enable(RCC_UART4);
rcc_periph_clock_enable(RCC_OTGFS);
rcc_periph_clock_enable(RCC_TIM6);
rcc_periph_clock_enable(RCC_DMA2);
@ -139,7 +140,7 @@ static void finish_interrupted_scrub(void) {
/* setup 10kHz timer */
static void tim6_setup(void) {
timer_reset(TIM6);
rcc_periph_reset_pulse(RST_TIM6);
timer_set_prescaler(TIM6, 8400 - 1); // 84Mhz/10kHz - 1
timer_set_period(TIM6, 65535); // Overflow in ~6.5 seconds
timer_enable_irq(TIM6, TIM_DIER_UIE);
@ -180,13 +181,16 @@ static void gpio_setup(void)
//gpio_mode_setup(GPIOA, GPIO_MODE_OUTPUT, GPIO_PUPD_NONE, GPIO6 | GPIO7);
//gpio_set(GPIOA, GPIO6 | GPIO7);
/* Status LEDs (PE4-15) */
gpio_mode_setup(GPIOE, GPIO_MODE_INPUT, GPIO_PUPD_NONE, 0xfff0);
/* Alarm LEDs (PA6,7) */
gpio_mode_setup(GPIOA, GPIO_MODE_OUTPUT, GPIO_PUPD_NONE, GPIO6 | GPIO7);
gpio_set(GPIOA, GPIO6 | GPIO7);
/* Mode LEDs */
gpio_mode_setup(GPIOE, GPIO_MODE_OUTPUT, GPIO_PUPD_NONE, GPIO13 | GPIO14);
/* Mode button */
gpio_mode_setup(GPIOE, GPIO_MODE_INPUT, GPIO_PUPD_PULLUP, GPIO15);
/* Speaker */
gpio_mode_setup(GPIOB, GPIO_MODE_OUTPUT, GPIO_PUPD_NONE, GPIO10);
gpio_set(GPIOB, GPIO10);
@ -199,12 +203,9 @@ static void gpio_setup(void)
gpio_mode_setup(GPIOA, GPIO_MODE_AF, GPIO_PUPD_NONE, GPIO9 | GPIO10);
gpio_set_af(GPIOA, GPIO_AF7, GPIO9 | GPIO10);
/* USART2 (host link) */
gpio_mode_setup(GPIOA, GPIO_MODE_AF, GPIO_PUPD_NONE, GPIO2 | GPIO3);
gpio_set_af(GPIOA, GPIO_AF7, GPIO2 | GPIO3);
/* K0 (PE4)/K1 (PE3) buttons */
//gpio_mode_setup(GPIOE, GPIO_MODE_INPUT, GPIO_PUPD_PULLUP, GPIO3 | GPIO4);
/* UART4 (host link) */
gpio_mode_setup(GPIOC, GPIO_MODE_AF, GPIO_PUPD_NONE, GPIO10 | GPIO11);
gpio_set_af(GPIOC, GPIO_AF8, GPIO10 | GPIO11);
}
struct hid_report {
@ -221,7 +222,7 @@ void pairing_input(uint8_t modbyte, uint8_t keycode);
void pairing_parse_report(struct hid_report *buf, uint8_t len);
/* Minimum number of bytes of handshake hash to confirm during pairing */
#define MIN_PAIRING_SEQUENCE_LENGTH 8
#define MIN_PAIRING_SEQUENCE_LENGTH 4
int pairing_check(struct NoiseState *st, const char *buf) {
//LOG_PRINTF("Checking pairing\n");
@ -491,10 +492,10 @@ void DMA_ISR(DEBUG_USART_DMA_NUM, DEBUG_USART_DMA_STREAM_NUM)(void) {
/*@ 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);
requires \separated(st, st->rx_cipher, st->tx_cipher, st->handshake, (uint8_t *)pkt->payload, &uart4_out, &st->handshake_hash);
requires \valid(uart4_out);
assigns pairing_buf_pos, *usart2_out, *st;
assigns pairing_buf_pos, *uart4_out, *st;
assigns st->handshake, st->handshake_state, st->rx_cipher, st->tx_cipher;
@*/
@ -515,7 +516,7 @@ void handle_host_packet(struct NoiseState *st, const struct control_packet *pkt,
} else {
LOG_PRINTF("Too many failed handshake attempts, not starting another one\n");
struct control_packet out = { .type=HOST_TOO_MANY_FAILS };
send_packet(usart2_out, (uint8_t *)&out, sizeof(out));
send_packet(uart4_out, (uint8_t *)&out, sizeof(out));
}
} else if (pkt->type == HOST_HANDSHAKE) {
@ -525,7 +526,7 @@ void handle_host_packet(struct NoiseState *st, const struct control_packet *pkt,
TRACING_CLEAR(TR_NOISE_HANDSHAKE);
LOG_PRINTF("Reporting handshake error to host\n");
struct control_packet out = { .type=HOST_CRYPTO_ERROR };
send_packet(usart2_out, (uint8_t *)&out, sizeof(out));
send_packet(uart4_out, (uint8_t *)&out, sizeof(out));
} else TRACING_CLEAR(TR_NOISE_HANDSHAKE);
} else {
@ -555,10 +556,10 @@ int main(void)
/* end unsafe debug code */
#endif
usart_dma_init(usart2_out);
usart_enable_rx_interrupt(USART2);
nvic_enable_irq(NVIC_USART2_IRQ);
nvic_set_priority(NVIC_USART2_IRQ, 3<<4);
usart_dma_init(uart4_out);
usart_enable_rx_interrupt(UART4);
nvic_enable_irq(NVIC_UART4_IRQ);
nvic_set_priority(NVIC_UART4_IRQ, 3<<4);
nvic_set_priority(debug_out_s.irqn, 1<<4);
LOG_PRINTF("\n==================================\n");
@ -602,20 +603,52 @@ int main(void)
gpio_clear(GPIOA, GPIO6);
gpio_clear(GPIOA, GPIO7);
gpio_clear(GPIOB, GPIO10);
int last_btn_st = 0;
int debounce_ctr = 0;
int mode_debug = 0;
#define DEBOUNCE_IVL 1000
gpio_set(GPIOE, GPIO13);
gpio_clear(GPIOE, GPIO14);
while (23) {
delay(1);
if (debounce_ctr > 0) {
debounce_ctr -= 1;
} else {
if (gpio_get(GPIOE, GPIO15)) {
if (!last_btn_st) {
debounce_ctr = DEBOUNCE_IVL;
mode_debug = !mode_debug;
if (mode_debug) {
gpio_clear(GPIOE, GPIO13);
gpio_set(GPIOE, GPIO14);
} else {
gpio_set(GPIOE, GPIO13);
gpio_clear(GPIOE, GPIO14);
}
}
last_btn_st = 1;
} else {
last_btn_st = 0;
}
}
/*
led_ctr++;
if (led_ctr == 10) {
gpio_clear(GPIOA, GPIO6);
gpio_clear(GPIOA, GPIO7);
} else if (led_ctr == 300) {
gpio_mode_setup(GPIOE, GPIO_MODE_INPUT, GPIO_PUPD_NONE, 0xfff0);
} else if (led_ctr == 400) {
if (++led_idx == 12)
led_idx = 0;
gpio_mode_setup(GPIOE, GPIO_MODE_OUTPUT, GPIO_PUPD_NONE, 1<<(4+led_idx));
gpio_clear(GPIOE, 0xfff0);
if (led_idx & 1)
gpio_set(GPIOA, GPIO6);
else
@ -638,7 +671,7 @@ int main(void)
} else {
gpio_clear(GPIOB, GPIO10);
}
continue;
*/
if (++poll_ctr == 10) {
poll_ctr = 0;
@ -652,12 +685,13 @@ int main(void)
host_packet_length = 0; /* Acknowledge to USART ISR the buffer has been handled */
} else if (host_packet_length < 0) { /* USART error */
ssize_t err = host_packet_length;
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: %zd\n", err);
struct control_packet pkt = { .type=HOST_COMM_ERROR };
send_packet(usart2_out, (uint8_t *)&pkt, sizeof(pkt));
send_packet(uart4_out, (uint8_t *)&pkt, sizeof(pkt));
if (reset_protocol_handshake(&noise_state))
LOG_PRINTF("Error starting protocol handshake.\n");
@ -666,15 +700,17 @@ int main(void)
}
}
if (noise_state.handshake_state == HANDSHAKE_IN_PROGRESS) {
#if 0
if (noise_state.handshake_state == HANDSHAKE_PHASE1 || noise_state.handshake_state == HANDSHAKE_PHASE2) {
TRACING_SET(TR_NOISE_HANDSHAKE);
if (try_continue_noise_handshake(&noise_state, NULL, 0)) { /* handle outgoing messages */
TRACING_CLEAR(TR_NOISE_HANDSHAKE);
LOG_PRINTF("Reporting handshake error to host\n");
struct control_packet pkt = { .type=HOST_CRYPTO_ERROR };
send_packet(usart2_out, (uint8_t *)&pkt, sizeof(pkt));
send_packet(uart4_out, (uint8_t *)&pkt, sizeof(pkt));
} else TRACING_CLEAR(TR_NOISE_HANDSHAKE);
}
#endif
}
}

View file

@ -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:

View file

@ -12,54 +12,54 @@
volatile struct {
struct dma_buf dma;
uint8_t data[256];
} usart2_buf = { .dma = { .len = sizeof(usart2_buf.data) } };
} uart4_buf = { .dma = { .len = sizeof(uart4_buf.data) } };
struct dma_usart_file usart2_out_s = {
.usart = USART2,
struct dma_usart_file uart4_out_s = {
.usart = UART4,
.baudrate = 115200,
.dma = DMA1,
.stream = 6,
.stream = 4,
.channel = 4,
.irqn = NVIC_DMA_IRQ(1, 6),
.buf = &usart2_buf.dma
.irqn = NVIC_DMA_IRQ(1, 4),
.buf = &uart4_buf.dma
};
struct dma_usart_file *usart2_out = &usart2_out_s;
struct dma_usart_file *uart4_out = &uart4_out_s;
void dma1_stream6_isr(void) {
void dma1_stream4_isr(void) {
TRACING_SET(TR_HOST_IF_DMA_IRQ);
static unsigned int fifo_errors = 0; /* debug */
if (dma_get_interrupt_flag(usart2_out->dma, usart2_out->stream, DMA_FEIF)) {
if (dma_get_interrupt_flag(uart4_out->dma, uart4_out->stream, DMA_FEIF)) {
/* Ignore FIFO errors as they're 100% non-critical for UART applications */
dma_clear_interrupt_flags(usart2_out->dma, usart2_out->stream, DMA_FEIF);
dma_clear_interrupt_flags(uart4_out->dma, uart4_out->stream, DMA_FEIF);
fifo_errors++;
TRACING_CLEAR(TR_HOST_IF_DMA_IRQ);
return;
}
/* Transfer complete interrupt */
dma_clear_interrupt_flags(usart2_out->dma, usart2_out->stream, DMA_TCIF);
dma_clear_interrupt_flags(uart4_out->dma, uart4_out->stream, DMA_TCIF);
if (usart2_out->buf->wr_pos != usart2_out->buf->xfr_end) /* buffer not empty */
schedule_dma(usart2_out);
if (uart4_out->buf->wr_pos != uart4_out->buf->xfr_end) /* buffer not empty */
schedule_dma(uart4_out);
TRACING_CLEAR(TR_HOST_IF_DMA_IRQ);
}
void usart2_isr(void) {
void uart4_isr(void) {
TRACING_SET(TR_HOST_IF_USART_IRQ);
static struct cobs_decode_state host_cobs_state = {0};
if (USART2_SR & USART_SR_ORE) { /* Overrun handling */
LOG_PRINTF("USART2 data register overrun\n");
if (UART4_SR & USART_SR_ORE) { /* Overrun handling */
LOG_PRINTF("UART4 data register overrun\n");
/* Clear interrupt flag */
(void)USART2_DR; /* FIXME make sure this read is not optimized out */
(void)UART4_DR; /* FIXME make sure this read is not optimized out */
host_packet_length = -1;
TRACING_CLEAR(TR_HOST_IF_USART_IRQ);
return;
}
uint8_t data = USART2_DR; /* This automatically acknowledges the IRQ */
uint8_t data = UART4_DR; /* This automatically acknowledges the IRQ */
if (host_packet_length) {
LOG_PRINTF("USART2 COBS buffer overrun\n");
LOG_PRINTF("UART4 COBS buffer overrun\n");
host_packet_length = -1;
TRACING_CLEAR(TR_HOST_IF_USART_IRQ);
return;
@ -78,7 +78,7 @@ void usart2_isr(void) {
} else if (rv == -3) {
/* invalid empty frame */
LOG_PRINTF("Got double null byte from host\n");
host_packet_length = -1;
/* FIXME DEBUG host_packet_length = -1; */
} else if (rv == -4) {
/* frame too large */
LOG_PRINTF("Got too large frame from host\n");

View file

@ -4,7 +4,7 @@
#include "usart_helpers.h"
extern struct dma_usart_file *usart2_out;
extern struct dma_usart_file *uart4_out;
enum control_packet_types {
_HOST_RESERVED = 0,

View file

@ -38,6 +38,8 @@
#include <stdlib.h>
#include <string.h>
#include <usbh_core.h>
#include <libopencm3/stm32/f4/rng.h>
#include "usart_helpers.h"

View file

@ -26,8 +26,8 @@
#include <string.h>
#include <stdint.h>
#include <libopencm3/stm32/otg_hs.h>
#include <libopencm3/stm32/otg_fs.h>
#include <libopencm3/usb/dwc/otg_hs.h>
#include <libopencm3/usb/dwc/otg_fs.h>

View file

@ -261,261 +261,261 @@ const char * const even[256] = {
};
const char * const odd[256] = {
"aardvark", /* 00 */
"absurd", /* 01 */
"accrue", /* 02 */
"acme", /* 03 */
"adrift", /* 04 */
"adult", /* 05 */
"afflict", /* 06 */
"ahead", /* 07 */
"aimless", /* 08 */
"Algol", /* 09 */
"allow", /* 0A */
"alone", /* 0B */
"ammo", /* 0C */
"ancient", /* 0D */
"apple", /* 0E */
"artist", /* 0F */
"assume", /* 10 */
"Athens", /* 11 */
"atlas", /* 12 */
"Aztec", /* 13 */
"baboon", /* 14 */
"backfield", /* 15 */
"backward", /* 16 */
"banjo", /* 17 */
"beaming", /* 18 */
"bedlamp", /* 19 */
"beehive", /* 1A */
"beeswax", /* 1B */
"befriend", /* 1C */
"Belfast", /* 1D */
"berserk", /* 1E */
"billiard", /* 1F */
"bison", /* 20 */
"blackjack", /* 21 */
"blockade", /* 22 */
"blowtorch", /* 23 */
"bluebird", /* 24 */
"bombast", /* 25 */
"bookshelf", /* 26 */
"brackish", /* 27 */
"breadline", /* 28 */
"breakup", /* 29 */
"brickyard", /* 2A */
"briefcase", /* 2B */
"Burbank", /* 2C */
"button", /* 2D */
"buzzard", /* 2E */
"cement", /* 2F */
"chairlift", /* 30 */
"chatter", /* 31 */
"checkup", /* 32 */
"chisel", /* 33 */
"choking", /* 34 */
"chopper", /* 35 */
"Christmas", /* 36 */
"clamshell", /* 37 */
"classic", /* 38 */
"classroom", /* 39 */
"cleanup", /* 3A */
"clockwork", /* 3B */
"cobra", /* 3C */
"commence", /* 3D */
"concert", /* 3E */
"cowbell", /* 3F */
"crackdown", /* 40 */
"cranky", /* 41 */
"crowfoot", /* 42 */
"crucial", /* 43 */
"crumpled", /* 44 */
"crusade", /* 45 */
"cubic", /* 46 */
"dashboard", /* 47 */
"deadbolt", /* 48 */
"deckhand", /* 49 */
"dogsled", /* 4A */
"dragnet", /* 4B */
"drainage", /* 4C */
"dreadful", /* 4D */
"drifter", /* 4E */
"dropper", /* 4F */
"drumbeat", /* 50 */
"drunken", /* 51 */
"Dupont", /* 52 */
"dwelling", /* 53 */
"eating", /* 54 */
"edict", /* 55 */
"egghead", /* 56 */
"eightball", /* 57 */
"endorse", /* 58 */
"endow", /* 59 */
"enlist", /* 5A */
"erase", /* 5B */
"escape", /* 5C */
"exceed", /* 5D */
"eyeglass", /* 5E */
"eyetooth", /* 5F */
"facial", /* 60 */
"fallout", /* 61 */
"flagpole", /* 62 */
"flatfoot", /* 63 */
"flytrap", /* 64 */
"fracture", /* 65 */
"framework", /* 66 */
"freedom", /* 67 */
"frighten", /* 68 */
"gazelle", /* 69 */
"Geiger", /* 6A */
"glitter", /* 6B */
"glucose", /* 6C */
"goggles", /* 6D */
"goldfish", /* 6E */
"gremlin", /* 6F */
"guidance", /* 70 */
"hamlet", /* 71 */
"highchair", /* 72 */
"hockey", /* 73 */
"indoors", /* 74 */
"indulge", /* 75 */
"inverse", /* 76 */
"involve", /* 77 */
"island", /* 78 */
"jawbone", /* 79 */
"keyboard", /* 7A */
"kickoff", /* 7B */
"kiwi", /* 7C */
"klaxon", /* 7D */
"locale", /* 7E */
"lockup", /* 7F */
"merit", /* 80 */
"minnow", /* 81 */
"miser", /* 82 */
"Mohawk", /* 83 */
"mural", /* 84 */
"music", /* 85 */
"necklace", /* 86 */
"Neptune", /* 87 */
"newborn", /* 88 */
"nightbird", /* 89 */
"Oakland", /* 8A */
"obtuse", /* 8B */
"offload", /* 8C */
"optic", /* 8D */
"orca", /* 8E */
"payday", /* 8F */
"peachy", /* 90 */
"pheasant", /* 91 */
"physique", /* 92 */
"playhouse", /* 93 */
"Pluto", /* 94 */
"preclude", /* 95 */
"prefer", /* 96 */
"preshrunk", /* 97 */
"printer", /* 98 */
"prowler", /* 99 */
"pupil", /* 9A */
"puppy", /* 9B */
"python", /* 9C */
"quadrant", /* 9D */
"quiver", /* 9E */
"quota", /* 9F */
"ragtime", /* A0 */
"ratchet", /* A1 */
"rebirth", /* A2 */
"reform", /* A3 */
"regain", /* A4 */
"reindeer", /* A5 */
"rematch", /* A6 */
"repay", /* A7 */
"retouch", /* A8 */
"revenge", /* A9 */
"reward", /* AA */
"rhythm", /* AB */
"ribcage", /* AC */
"ringbolt", /* AD */
"robust", /* AE */
"rocker", /* AF */
"ruffled", /* B0 */
"sailboat", /* B1 */
"sawdust", /* B2 */
"scallion", /* B3 */
"scenic", /* B4 */
"scorecard", /* B5 */
"Scotland", /* B6 */
"seabird", /* B7 */
"select", /* B8 */
"sentence", /* B9 */
"shadow", /* BA */
"shamrock", /* BB */
"showgirl", /* BC */
"skullcap", /* BD */
"skydive", /* BE */
"slingshot", /* BF */
"slowdown", /* C0 */
"snapline", /* C1 */
"snapshot", /* C2 */
"snowcap", /* C3 */
"snowslide", /* C4 */
"solo", /* C5 */
"southward", /* C6 */
"soybean", /* C7 */
"spaniel", /* C8 */
"spearhead", /* C9 */
"spellbind", /* CA */
"spheroid", /* CB */
"spigot", /* CC */
"spindle", /* CD */
"spyglass", /* CE */
"stagehand", /* CF */
"stagnate", /* D0 */
"stairway", /* D1 */
"standard", /* D2 */
"stapler", /* D3 */
"steamship", /* D4 */
"sterling", /* D5 */
"stockman", /* D6 */
"stopwatch", /* D7 */
"stormy", /* D8 */
"sugar", /* D9 */
"surmount", /* DA */
"suspense", /* DB */
"sweatband", /* DC */
"swelter", /* DD */
"tactics", /* DE */
"talon", /* DF */
"tapeworm", /* E0 */
"tempest", /* E1 */
"tiger", /* E2 */
"tissue", /* E3 */
"tonic", /* E4 */
"topmost", /* E5 */
"tracker", /* E6 */
"transit", /* E7 */
"trauma", /* E8 */
"treadmill", /* E9 */
"Trojan", /* EA */
"trouble", /* EB */
"tumor", /* EC */
"tunnel", /* ED */
"tycoon", /* EE */
"uncut", /* EF */
"unearth", /* F0 */
"unwind", /* F1 */
"uproot", /* F2 */
"upset", /* F3 */
"upshot", /* F4 */
"vapor", /* F5 */
"village", /* F6 */
"virus", /* F7 */
"Vulcan", /* F8 */
"waffle", /* F9 */
"wallet", /* FA */
"watchword", /* FB */
"wayside", /* FC */
"willow", /* FD */
"woodlark", /* FE */
"Zulu", /* FF */
"adroitness", /* 00 */
"adviser", /* 01 */
"aftermath", /* 02 */
"aggregate", /* 03 */
"alkali", /* 04 */
"almighty", /* 05 */
"amulet", /* 06 */
"amusement", /* 07 */
"antenna", /* 08 */
"applicant", /* 09 */
"Apollo", /* 0A */
"armistice", /* 0B */
"article", /* 0C */
"asteroid", /* 0D */
"Atlantic", /* 0E */
"atmosphere", /* 0F */
"autopsy", /* 10 */
"Babylon", /* 11 */
"backwater", /* 12 */
"barbecue", /* 13 */
"belowground", /* 14 */
"bifocals", /* 15 */
"bodyguard", /* 16 */
"bookseller", /* 17 */
"borderline", /* 18 */
"bottomless", /* 19 */
"Bradbury", /* 1A */
"bravado", /* 1B */
"Brazilian", /* 1C */
"breakaway", /* 1D */
"Burlington", /* 1E */
"businessman", /* 1F */
"butterfat", /* 20 */
"Camelot", /* 21 */
"candidate", /* 22 */
"cannonball", /* 23 */
"Capricorn", /* 24 */
"caravan", /* 25 */
"caretaker", /* 26 */
"celebrate", /* 27 */
"cellulose", /* 28 */
"certify", /* 29 */
"chambermaid", /* 2A */
"Cherokee", /* 2B */
"Chicago", /* 2C */
"clergyman", /* 2D */
"coherence", /* 2E */
"combustion", /* 2F */
"commando", /* 30 */
"company", /* 31 */
"component", /* 32 */
"concurrent", /* 33 */
"confidence", /* 34 */
"conformist", /* 35 */
"congregate", /* 36 */
"consensus", /* 37 */
"consulting", /* 38 */
"corporate", /* 39 */
"corrosion", /* 3A */
"councilman", /* 3B */
"crossover", /* 3C */
"crucifix", /* 3D */
"cumbersome", /* 3E */
"customer", /* 3F */
"Dakota", /* 40 */
"decadence", /* 41 */
"December", /* 42 */
"decimal", /* 43 */
"designing", /* 44 */
"detector", /* 45 */
"detergent", /* 46 */
"determine", /* 47 */
"dictator", /* 48 */
"dinosaur", /* 49 */
"direction", /* 4A */
"disable", /* 4B */
"disbelief", /* 4C */
"disruptive", /* 4D */
"distortion", /* 4E */
"document", /* 4F */
"embezzle", /* 50 */
"enchanting", /* 51 */
"enrollment", /* 52 */
"enterprise", /* 53 */
"equation", /* 54 */
"equipment", /* 55 */
"escapade", /* 56 */
"Eskimo", /* 57 */
"everyday", /* 58 */
"examine", /* 59 */
"existence", /* 5A */
"exodus", /* 5B */
"fascinate", /* 5C */
"filament", /* 5D */
"finicky", /* 5E */
"forever", /* 5F */
"fortitude", /* 60 */
"frequency", /* 61 */
"gadgetry", /* 62 */
"Galveston", /* 63 */
"getaway", /* 64 */
"glossary", /* 65 */
"gossamer", /* 66 */
"graduate", /* 67 */
"gravity", /* 68 */
"guitarist", /* 69 */
"hamburger", /* 6A */
"Hamilton", /* 6B */
"handiwork", /* 6C */
"hazardous", /* 6D */
"headwaters", /* 6E */
"hemisphere", /* 6F */
"hesitate", /* 70 */
"hideaway", /* 71 */
"holiness", /* 72 */
"hurricane", /* 73 */
"hydraulic", /* 74 */
"impartial", /* 75 */
"impetus", /* 76 */
"inception", /* 77 */
"indigo", /* 78 */
"inertia", /* 79 */
"infancy", /* 7A */
"inferno", /* 7B */
"informant", /* 7C */
"insincere", /* 7D */
"insurgent", /* 7E */
"integrate", /* 7F */
"intention", /* 80 */
"inventive", /* 81 */
"Istanbul", /* 82 */
"Jamaica", /* 83 */
"Jupiter", /* 84 */
"leprosy", /* 85 */
"letterhead", /* 86 */
"liberty", /* 87 */
"maritime", /* 88 */
"matchmaker", /* 89 */
"maverick", /* 8A */
"Medusa", /* 8B */
"megaton", /* 8C */
"microscope", /* 8D */
"microwave", /* 8E */
"midsummer", /* 8F */
"millionaire", /* 90 */
"miracle", /* 91 */
"misnomer", /* 92 */
"molasses", /* 93 */
"molecule", /* 94 */
"Montana", /* 95 */
"monument", /* 96 */
"mosquito", /* 97 */
"narrative", /* 98 */
"nebula", /* 99 */
"newsletter", /* 9A */
"Norwegian", /* 9B */
"October", /* 9C */
"Ohio", /* 9D */
"onlooker", /* 9E */
"opulent", /* 9F */
"Orlando", /* A0 */
"outfielder", /* A1 */
"Pacific", /* A2 */
"pandemic", /* A3 */
"Pandora", /* A4 */
"paperweight", /* A5 */
"paragon", /* A6 */
"paragraph", /* A7 */
"paramount", /* A8 */
"passenger", /* A9 */
"pedigree", /* AA */
"Pegasus", /* AB */
"penetrate", /* AC */
"perceptive", /* AD */
"performance", /* AE */
"pharmacy", /* AF */
"phonetic", /* B0 */
"photograph", /* B1 */
"pioneer", /* B2 */
"pocketful", /* B3 */
"politeness", /* B4 */
"positive", /* B5 */
"potato", /* B6 */
"processor", /* B7 */
"provincial", /* B8 */
"proximate", /* B9 */
"puberty", /* BA */
"publisher", /* BB */
"pyramid", /* BC */
"quantity", /* BD */
"racketeer", /* BE */
"rebellion", /* BF */
"recipe", /* C0 */
"recover", /* C1 */
"repellent", /* C2 */
"replica", /* C3 */
"reproduce", /* C4 */
"resistor", /* C5 */
"responsive", /* C6 */
"retraction", /* C7 */
"retrieval", /* C8 */
"retrospect", /* C9 */
"revenue", /* CA */
"revival", /* CB */
"revolver", /* CC */
"sandalwood", /* CD */
"sardonic", /* CE */
"Saturday", /* CF */
"savagery", /* D0 */
"scavenger", /* D1 */
"sensation", /* D2 */
"sociable", /* D3 */
"souvenir", /* D4 */
"specialist", /* D5 */
"speculate", /* D6 */
"stethoscope", /* D7 */
"stupendous", /* D8 */
"supportive", /* D9 */
"surrender", /* DA */
"suspicious", /* DB */
"sympathy", /* DC */
"tambourine", /* DD */
"telephone", /* DE */
"therapist", /* DF */
"tobacco", /* E0 */
"tolerance", /* E1 */
"tomorrow", /* E2 */
"torpedo", /* E3 */
"tradition", /* E4 */
"travesty", /* E5 */
"trombonist", /* E6 */
"truncated", /* E7 */
"typewriter", /* E8 */
"ultimate", /* E9 */
"undaunted", /* EA */
"underfoot", /* EB */
"unicorn", /* EC */
"unify", /* ED */
"universe", /* EE */
"unravel", /* EF */
"upcoming", /* F0 */
"vacancy", /* F1 */
"vagabond", /* F2 */
"vertigo", /* F3 */
"Virginia", /* F4 */
"visitor", /* F5 */
"vocalist", /* F6 */
"voyager", /* F7 */
"warranty", /* F8 */
"Waterloo", /* F9 */
"whimsical", /* FA */
"Wichita", /* FB */
"Wilmington", /* FC */
"Wyoming", /* FD */
"yesteryear", /* FE */
"Yucatan" /* FF */
};

@ -0,0 +1 @@
Subproject commit 72134885be981628d8c224aa6ddced508cae715a

@ -0,0 +1 @@
Subproject commit 81bd97f26ed9f73555e8f6bb9220f316c9860ed8