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
|
diff --git a/tests/sidetrail/working/s2n-cbc/tls/s2n_cbc.c b/tests/sidetrail/working/s2n-cbc/tls/s2n_cbc.c
index 401ab760..f39cc7e2 100644
--- a/tests/sidetrail/working/s2n-cbc/tls/s2n_cbc.c
+++ b/tests/sidetrail/working/s2n-cbc/tls/s2n_cbc.c
@@ -26,6 +26,28 @@
#include "tls/s2n_connection.h"
#include "tls/s2n_record.h"
+#include <smack.h>
+#include <smack-contracts.h>
+#include "ct-verif.h"
+#include "sidetrail.h"
+
+/* Because of a bug in SMACK, when we try to specify the invarients for this loop in the main function,
+ * SMACK crashes. Moving the code (unmodified) to this function sidesteps the bug. Michael Emmi has promissed
+ * a fix soon
+ */
+int double_loop(int old_mismatches, struct s2n_blob *decrypted, int check, int cutoff, int padding_length) {
+ __VERIFIER_assert(decrypted->size >= 0);
+ __VERIFIER_assert(decrypted->size <= MAX_SIZE);
+ int mismatches = old_mismatches;
+ for (uint32_t i = 0, j = decrypted->size - 1 - check; i < check && j < decrypted->size; i++, j++) {
+ invariant(i <= check);
+ invariant(j == i + decrypted->size - check - 1);
+ uint8_t mask = ~(0xff << ((i >= cutoff) * 8));
+ mismatches |= (decrypted->data[j] ^ padding_length) & mask;
+ }
+ return mismatches;
+}
+
/* A TLS CBC record looks like ..
*
* [ Payload data ] [ HMAC ] [ Padding ] [ Padding length byte ]
@@ -48,23 +70,28 @@
*/
int s2n_verify_cbc(struct s2n_connection *conn, struct s2n_hmac_state *hmac, struct s2n_blob *decrypted)
{
- uint8_t mac_digest_size = 0;
- POSIX_GUARD(s2n_hmac_digest_size(hmac->alg, &mac_digest_size));
+ uint8_t mac_digest_size = DIGEST_SIZE;
+ //POSIX_GUARD(s2n_hmac_digest_size(hmac->alg, &mac_digest_size));
/* The record has to be at least big enough to contain the MAC,
* plus the padding length byte */
POSIX_ENSURE_GT(decrypted->size, mac_digest_size);
int payload_and_padding_size = decrypted->size - mac_digest_size;
+ __VERIFIER_assert(payload_and_padding_size <= MAX_SIZE - 20);
/* Determine what the padding length is */
uint8_t padding_length = decrypted->data[decrypted->size - 1];
+ __VERIFIER_assume(padding_length >= 0);
+ __VERIFIER_assume(padding_length < 256);
int payload_length = MAX(payload_and_padding_size - padding_length - 1, 0);
/* Update the MAC */
POSIX_GUARD(s2n_hmac_update(hmac, decrypted->data, payload_length));
int currently_in_hash_block = hmac->currently_in_hash_block;
+ __VERIFIER_assume(currently_in_hash_block >= 0);
+ __VERIFIER_assume(currently_in_hash_block < BLOCK_SIZE);
/* Check the MAC */
uint8_t check_digest[S2N_MAX_DIGEST_LEN];
@@ -81,18 +108,19 @@ int s2n_verify_cbc(struct s2n_connection *conn, struct s2n_hmac_state *hmac, str
POSIX_GUARD(s2n_hmac_update(hmac, decrypted->data + payload_length + mac_digest_size, decrypted->size - payload_length - mac_digest_size - 1));
/* SSLv3 doesn't specify what the padding should actually be */
- if (conn->actual_protocol_version == S2N_SSLv3) {
- return 0 - mismatches;
- }
+ //if (conn->actual_protocol_version == S2N_SSLv3) {
+ // return 0 - mismatches;
+ //}
/* Check the maximum amount that could theoretically be padding */
uint32_t check = MIN(255, (payload_and_padding_size - 1));
POSIX_ENSURE_GTE(check, padding_length);
uint32_t cutoff = check - padding_length;
- for (size_t i = 0, j = decrypted->size - 1 - check; i < check && j < decrypted->size; i++, j++) {
- uint8_t mask = ~(0xff << ((i >= cutoff) * 8));
- mismatches |= (decrypted->data[j] ^ padding_length) & mask;
- }
+ mismatches = double_loop(mismatches, decrypted, check, cutoff, padding_length);
+ //for (size_t i = 0, j = decrypted->size - 1 - check; i < check && j < decrypted->size; i++, j++) {
+ // uint8_t mask = ~(0xff << ((i >= cutoff) * 8));
+ // mismatches |= (decrypted->data[j] ^ padding_length) & mask;
+ //}
S2N_ERROR_IF(mismatches, S2N_ERR_CBC_VERIFY);
|
