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
|
/*
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Licensed under the Apache License, Version 2.0 (the "License").
* You may not use this file except in compliance with the License.
* A copy of the License is located at
*
* http://aws.amazon.com/apache2.0
*
* or in the "license" file accompanying this file. This file is distributed
* on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
* express or implied. See the License for the specific language governing
* permissions and limitations under the License.
*/
#include <sys/param.h>
#include <stdint.h>
#include "crypto/s2n_hmac.h"
#include "tls/s2n_record.h"
#include "tls/s2n_prf.h"
#include "tls/s2n_connection.h"
#include <smack.h>
#include <smack-contracts.h>
#include "ct-verif.h"
#include "sidetrail.h"
int simple_cbc_wrapper(int currently_in_hash_block, int size, int *xor_pad, int * digest_pad)
{
/* Even after code balancing, there is a small remaining leakage, because s2n forces an extra hash-compression
* round by copying an extra hash block's worth of data into the hash. This has extra cost of memcopy one
* hash block (of data already in cache). This could potentially be reduced by finding a better way to trigger
* the extra hash-compression round.
* Note that the 68 here is in LLVM time model units, which roughly correspond to cycles
*/
__VERIFIER_ASSERT_MAX_LEAKAGE(68);
public_in(__SMACK_value(currently_in_hash_block));
__VERIFIER_assume(currently_in_hash_block >= 0);
__VERIFIER_assume(currently_in_hash_block < BLOCK_SIZE);
struct s2n_hmac_state hmac = {
.alg = S2N_HMAC_SHA1,
.hash_block_size = BLOCK_SIZE,
.currently_in_hash_block = 0,
.digest_size = SHA_DIGEST_LENGTH,
.xor_pad_size = BLOCK_SIZE,
.inner.alg = S2N_HASH_SHA1,
.inner.currently_in_hash_block = 0,
.inner_just_key.alg = S2N_HASH_SHA1,
.inner_just_key.currently_in_hash_block = 0,
.outer.alg = S2N_HASH_SHA1,
.outer.currently_in_hash_block = 0,
.outer_just_key.alg = S2N_HASH_SHA1,
.outer_just_key.currently_in_hash_block = 0,
.xor_pad = *xor_pad,
//xor_pad is an array
.digest_pad = *digest_pad
};
struct s2n_crypto_parameters client;
struct s2n_connection conn = {
.client = &client,
.mode = S2N_SERVER
};
/* Data represents the decrypted data handed to the process.
* Intentionally left non-deterministic so that the proof can handle all possible values in the buffer
*/
//cppcheck-suppress unassignedVariable
int data[MAX_SIZE];
public_in(__SMACK_value(size));
__VERIFIER_assume(size >= 0);
__VERIFIER_assume(size <= MAX_SIZE);
struct s2n_blob decrypted = {
.data = data,
.size = size,
.allocated = 1,
};
return s2n_verify_cbc(&conn, &hmac, &decrypted);
}
|
