forked from awslabs/aws-lc-verification
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathHKDF.saw
111 lines (90 loc) · 3.37 KB
/
HKDF.saw
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
/*
* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
* SPDX-License-Identifier: Apache-2.0
*/
enable_experimental;
let digestOut_64_pre = do {
out_ptr <- llvm_alloc (llvm_array SHA_DIGEST_LENGTH i8);
out_len_ptr <- llvm_alloc i64;
return (out_ptr, out_len_ptr);
};
let digestOut_64_post out_ptr out_len_ptr out_value = do {
crucible_points_to out_ptr out_value;
crucible_points_to out_len_ptr (crucible_term {{`SHA_DIGEST_LENGTH : [64]}} );
};
// HKDF_extract
let HKDF_extract_spec = do {
global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_md_globals;
alloc_hmac_globals;
points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX));
secret_len <- crucible_fresh_var "secret_len" i64;
(secret, secret_ptr) <- ptr_to_fresh_array_readonly "secret" secret_len;
salt_len <- crucible_fresh_var "salt_len" i64;
(salt, salt_ptr) <- ptr_to_fresh_array_readonly "salt" salt_len;
(out_ptr, out_len_ptr) <- digestOut_64_pre;
crucible_execute_func
[ out_ptr
, out_len_ptr
, (crucible_global (md_storage HMAC_MD_INDEX))
, secret_ptr
, (crucible_term secret_len)
, salt_ptr
, (crucible_term salt_len)
];
global_points_to "OPENSSL_ia32cap_P" {{ ia32cap }};
points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX));
digestOut_64_post out_ptr out_len_ptr (crucible_term {{ HKDF_extract salt salt_len secret secret_len }});
crucible_return (crucible_term {{ 1 : [32] }});
};
// HKDF_expand specification
let HKDF_out = "HKDF.out";
let HKDF_expand_spec outLen = do {
global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_md_globals;
alloc_hmac_globals;
points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX));
out_ptr <- llvm_alloc (llvm_array outLen i8);
(prk, prk_ptr) <- ptr_to_fresh_readonly "prk" (llvm_array SHA_DIGEST_LENGTH i8);
info_len <- crucible_fresh_var "info_len" i64;
(info, info_ptr) <- ptr_to_fresh_array_readonly "info" info_len;
crucible_execute_func
[ out_ptr
, (crucible_term {{ `outLen : [64] }} )
, (crucible_global (md_storage HMAC_MD_INDEX))
, prk_ptr
, (crucible_term {{ `SHA_DIGEST_LENGTH : [64]}} )
, info_ptr
, (crucible_term info_len)
];
llvm_setup_with_tag HKDF_out
(crucible_points_to out_ptr (crucible_term {{ HKDF_expand`{l = outLen} prk info info_len }}));
crucible_return (crucible_term {{ 1 : [32] }});
};
// HKDF specification
let HKDF_spec outLen = do {
global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
alloc_md_globals;
alloc_hmac_globals;
points_to_env_md_st (crucible_global (md_storage HMAC_MD_INDEX));
out_ptr <- llvm_alloc (llvm_array outLen i8);
secret_len <- crucible_fresh_var "secret_len" i64;
(secret, secret_ptr) <- ptr_to_fresh_array_readonly "secret" secret_len;
salt_len <- crucible_fresh_var "salt_len" i64;
(salt, salt_ptr) <- ptr_to_fresh_array_readonly "salt" salt_len;
info_len <- crucible_fresh_var "info_len" i64;
(info, info_ptr) <- ptr_to_fresh_array_readonly "info" info_len;
crucible_execute_func
[ out_ptr
, (crucible_term {{ `outLen : [64] }} )
, (crucible_global (md_storage HMAC_MD_INDEX))
, secret_ptr
, (crucible_term secret_len)
, salt_ptr
, (crucible_term salt_len)
, info_ptr
, (crucible_term info_len)
];
crucible_points_to out_ptr (crucible_term {{ HKDF`{l = outLen} secret secret_len salt salt_len info info_len }});
crucible_return (crucible_term {{ 1 : [32] }});
};