summaryrefslogtreecommitdiff
path: root/src/noise.c
blob: 949a68d16044c7749f667f921d9db584754b9c15 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
#include <string.h>

#include "noise.h"
#include "packet_interface.h"
#include "rand_stm32.h"

#include "crypto/noise-c/src/crypto/blake2/blake2s.h"


#ifdef VERIFICATION
#define HANDLE_NOISE_ERROR(x, msg) if (x) { goto errout; }
#else
#define HANDLE_NOISE_ERROR(x, msg) do { \
        err = x; \
        if (err != NOISE_ERROR_NONE) { \
            char errbuf[256]; \
            noise_strerror(err, errbuf, sizeof(errbuf)); \
            LOG_PRINTF("Error " msg ": %s\n", errbuf); \
            goto errout; \
        } \
    } while(0);
#endif

#ifdef VERIFICATION

/*@ requires \valid(s + (0..n-1));
  @ assigns s[0..n-1] \from c;
  @ assigns \result \from s;
  @ ensures result_ptr: \result == s;
  @*/
uint8_t *fc_memset_uint8(uint8_t *s, int c, size_t n);

/*@ requires \valid(dest + (0..n-1));
  @ requires \valid_read(src + (0..n-1));
  @ assigns dest[0..n-1] \from src[0..n-1];
  @ assigns \result \from dest;
  @ ensures result_ptr: \result == dest;
  @ ensures equals: \forall integer i; 0 <= i <= n-1 ==> dest[i] == src[i];
  @*/
uint8_t *fc_memcpy_uint8(uint8_t *dest, const uint8_t *src, size_t n);

#else
#define fc_memset_uint8 memset
#define fc_memcpy_uint8 memcpy
#endif


volatile uint8_t host_packet_buf[MAX_HOST_PACKET_SIZE];
volatile int host_packet_length = 0;


/*@
    requires \valid(st);

    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) {
    st->handshake_state = HANDSHAKE_UNINITIALIZED;
    st->handshake = NULL;
    st->tx_cipher = NULL;
    st->rx_cipher = NULL;
    fc_memset_uint8(st->handshake_hash, 0, sizeof(st->handshake_hash));
    st->remote_key_reference = remote_key_reference;
    st->local_key = local_key;
    st->failed_handshakes = 0;
}

/*@
    requires \valid(st);
    requires \valid(st->handshake_hash + (0..31));
    requires \separated(st, st->rx_cipher, st->tx_cipher, st->handshake);

    ensures \result == 0 ==> (
        \valid(st->handshake) &&
        (st->handshake_state == HANDSHAKE_IN_PROGRESS));

    ensures \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;
 */
int reset_protocol_handshake(struct NoiseState *st) {
    uninit_handshake(st, HANDSHAKE_UNINITIALIZED);
    disarm_key_scrubber();
    noise_cipherstate_free(st->tx_cipher);
    noise_cipherstate_free(st->rx_cipher);
    st->tx_cipher = NULL;
    st->rx_cipher = NULL;
    st->handshake = NULL;
    memset(st->handshake_hash, 0, sizeof(st->handshake_hash));
    return start_protocol_handshake(st);
}

/*@ requires \valid(st) && \valid_read(st->local_key + (0..31));
  
    ensures \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};

    assigns st->handshake, st->handshake_state;
 */
int start_protocol_handshake(struct NoiseState *st) {
    /* TODO Noise-C is nice for prototyping, but we should really get rid of it for mostly three reasons:
     *   * We don't need cipher/protocol agility, and by baking the final protocol into the firmware we can save a lot
     *     of flash space by not including all the primitives we don't need as well as noise's dynamic protocol
     *     abstraction layer.
     *   * Noise-c is not very embedded-friendly, in particular it uses malloc and free. We should be able to run
     *     everything with statically allocated buffers instead.
     *   * Parts of it are not written that well
     */
    NoiseHandshakeState *handshake;
    int err;
    
    HANDLE_NOISE_ERROR(noise_init(), "initializing noise");

    HANDLE_NOISE_ERROR(noise_handshakestate_new_by_name(&handshake, "Noise_XX_25519_ChaChaPoly_BLAKE2s", NOISE_ROLE_RESPONDER), "instantiating handshake pattern");

    NoiseDHState *dh = noise_handshakestate_get_local_keypair_dh(handshake);
    HANDLE_NOISE_ERROR(noise_dhstate_set_keypair_private(dh, st->local_key, CURVE25519_KEY_LEN), "loading local private keys");

    HANDLE_NOISE_ERROR(noise_handshakestate_start(handshake), "starting handshake");

    st->handshake = handshake;
    st->handshake_state = HANDSHAKE_IN_PROGRESS;
    return 0;

errout:
    noise_handshakestate_free(handshake);
    return -1;
}

/*@ requires \valid(st);
    requires \valid(st->local_key + (0..31));
    requires \separated(st, st->local_key + (0..31));
    assigns st->local_key[0..31];
 */
int generate_identity_key(struct NoiseState *st) {
    NoiseDHState *dh;
    int err;

    HANDLE_NOISE_ERROR(noise_dhstate_new_by_name(&dh, "25519"), "creating dhstate for key generation"); 
    HANDLE_NOISE_ERROR(noise_dhstate_generate_keypair(dh), "generating key pair");

    uint8_t unused[CURVE25519_KEY_LEN]; /* the noise api is a bit bad here. */
    fc_memset_uint8(st->local_key, 0, CURVE25519_KEY_LEN);

    HANDLE_NOISE_ERROR(noise_dhstate_get_keypair(dh, st->local_key, CURVE25519_KEY_LEN, unused, sizeof(unused)), "saving key pair");

    noise_dhstate_free(dh);
    return 0;
errout:
    if (dh)
        noise_dhstate_free(dh);
    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;

   assigns st->handshake, st->handshake_state;
 @*/
void uninit_handshake(struct NoiseState *st, enum handshake_state new_state) {
    if (st->handshake)
        noise_handshakestate_free(st->handshake);
    st->handshake_state = new_state;
    st->handshake = NULL;
    arm_key_scrubber();
}

//@ ghost int key_checked_trace;
//@ ghost int key_match_trace;
/*@ 
    requires \valid(st);
    requires \valid(usart2_out);
    requires \valid(st->handshake);

    requires \valid(st->remote_key + (0..sizeof(st->remote_key)-1));
    requires \valid(st->handshake_hash + (0..sizeof(st->handshake_hash)-1));

    requires \separated(&usart2_out, st, buf, st->handshake, &st->handshake_hash);

    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;
        uint8_t payload[MAX_HOST_PACKET_SIZE];
    } pkt;
    NoiseBuffer noise_msg;

    if (!st->handshake || st->handshake_state != HANDSHAKE_IN_PROGRESS) {
        LOG_PRINTF("Error: Invalid handshake state\n");
        goto errout;
    }

    /* 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;

    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;

    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");

        //@ 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");
        }

        
        //@ 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;
        }

        HANDLE_NOISE_ERROR(noise_dhstate_get_public_key(remote_dh, st->remote_key, sizeof(st->remote_key)), "getting remote pubkey");

        /* 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 (!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");

            uninit_handshake(st, HANDSHAKE_DONE_KNOWN_HOST);
            st->failed_handshakes = 0;

        } 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");

            uninit_handshake(st, HANDSHAKE_DONE_UNKNOWN_HOST);
            st->failed_handshakes++;
        }
        break;

    default:
        goto errout;
    }

    return 0;
errout:
    uninit_handshake(st, HANDSHAKE_UNINITIALIZED);
    st->failed_handshakes++;
    LOG_PRINTF("Noise protocol handshake failed, %d failed attempts\n", st->failed_handshakes);
    return -1;
}

/*@
    requires \valid(st);
    requires \valid_read(st->remote_key + (0..sizeof(st->remote_key)-1));
    requires \valid(st->remote_key_reference + (0..31));

    ensures st->handshake_state == HANDSHAKE_DONE_KNOWN_HOST;
    assigns st->remote_key_reference[0..31], st->handshake_state;
 */
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_finish(&bc, st->remote_key_reference);
    st->handshake_state = HANDSHAKE_DONE_KNOWN_HOST;
}

/*@
  requires \valid(st);
  requires \valid(usart2_out);
  requires \valid(st->tx_cipher);
  requires \valid_read(msg + (0..len-1));
  requires 0 <= len <= 65536;

  ensures \result \in {0, -1, -2, -3};
  assigns *st->tx_cipher;
 */
int send_encrypted_message(struct NoiseState *st, const uint8_t *msg, size_t len) {
    int err;
    NoiseBuffer noise_buf;
    struct {
        struct control_packet header;
        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;
    }

    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));

    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));

    return 0;
errout:
    return -2;
}