/src/nss/lib/freebl/verified/Hacl_Chacha20.c
Line | Count | Source (jump to first uncovered line) |
1 | | /* MIT License |
2 | | * |
3 | | * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation |
4 | | * Copyright (c) 2022-2023 HACL* Contributors |
5 | | * |
6 | | * Permission is hereby granted, free of charge, to any person obtaining a copy |
7 | | * of this software and associated documentation files (the "Software"), to deal |
8 | | * in the Software without restriction, including without limitation the rights |
9 | | * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell |
10 | | * copies of the Software, and to permit persons to whom the Software is |
11 | | * furnished to do so, subject to the following conditions: |
12 | | * |
13 | | * The above copyright notice and this permission notice shall be included in all |
14 | | * copies or substantial portions of the Software. |
15 | | * |
16 | | * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR |
17 | | * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, |
18 | | * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE |
19 | | * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER |
20 | | * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, |
21 | | * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE |
22 | | * SOFTWARE. |
23 | | */ |
24 | | |
25 | | #include "internal/Hacl_Chacha20.h" |
26 | | |
27 | | const uint32_t |
28 | | Hacl_Impl_Chacha20_Vec_chacha20_constants[4U] = { (uint32_t)0x61707865U, (uint32_t)0x3320646eU, (uint32_t)0x79622d32U, (uint32_t)0x6b206574U }; |
29 | | |
30 | | static inline void |
31 | | quarter_round(uint32_t *st, uint32_t a, uint32_t b, uint32_t c, uint32_t d) |
32 | 24.9M | { |
33 | 24.9M | uint32_t sta = st[a]; |
34 | 24.9M | uint32_t stb0 = st[b]; |
35 | 24.9M | uint32_t std0 = st[d]; |
36 | 24.9M | uint32_t sta10 = sta + stb0; |
37 | 24.9M | uint32_t std10 = std0 ^ sta10; |
38 | 24.9M | uint32_t std2 = std10 << (uint32_t)16U | std10 >> (uint32_t)16U; |
39 | 24.9M | st[a] = sta10; |
40 | 24.9M | st[d] = std2; |
41 | 24.9M | uint32_t sta0 = st[c]; |
42 | 24.9M | uint32_t stb1 = st[d]; |
43 | 24.9M | uint32_t std3 = st[b]; |
44 | 24.9M | uint32_t sta11 = sta0 + stb1; |
45 | 24.9M | uint32_t std11 = std3 ^ sta11; |
46 | 24.9M | uint32_t std20 = std11 << (uint32_t)12U | std11 >> (uint32_t)20U; |
47 | 24.9M | st[c] = sta11; |
48 | 24.9M | st[b] = std20; |
49 | 24.9M | uint32_t sta2 = st[a]; |
50 | 24.9M | uint32_t stb2 = st[b]; |
51 | 24.9M | uint32_t std4 = st[d]; |
52 | 24.9M | uint32_t sta12 = sta2 + stb2; |
53 | 24.9M | uint32_t std12 = std4 ^ sta12; |
54 | 24.9M | uint32_t std21 = std12 << (uint32_t)8U | std12 >> (uint32_t)24U; |
55 | 24.9M | st[a] = sta12; |
56 | 24.9M | st[d] = std21; |
57 | 24.9M | uint32_t sta3 = st[c]; |
58 | 24.9M | uint32_t stb = st[d]; |
59 | 24.9M | uint32_t std = st[b]; |
60 | 24.9M | uint32_t sta1 = sta3 + stb; |
61 | 24.9M | uint32_t std1 = std ^ sta1; |
62 | 24.9M | uint32_t std22 = std1 << (uint32_t)7U | std1 >> (uint32_t)25U; |
63 | 24.9M | st[c] = sta1; |
64 | 24.9M | st[b] = std22; |
65 | 24.9M | } |
66 | | |
67 | | static inline void |
68 | | double_round(uint32_t *st) |
69 | 3.12M | { |
70 | 3.12M | quarter_round(st, (uint32_t)0U, (uint32_t)4U, (uint32_t)8U, (uint32_t)12U); |
71 | 3.12M | quarter_round(st, (uint32_t)1U, (uint32_t)5U, (uint32_t)9U, (uint32_t)13U); |
72 | 3.12M | quarter_round(st, (uint32_t)2U, (uint32_t)6U, (uint32_t)10U, (uint32_t)14U); |
73 | 3.12M | quarter_round(st, (uint32_t)3U, (uint32_t)7U, (uint32_t)11U, (uint32_t)15U); |
74 | 3.12M | quarter_round(st, (uint32_t)0U, (uint32_t)5U, (uint32_t)10U, (uint32_t)15U); |
75 | 3.12M | quarter_round(st, (uint32_t)1U, (uint32_t)6U, (uint32_t)11U, (uint32_t)12U); |
76 | 3.12M | quarter_round(st, (uint32_t)2U, (uint32_t)7U, (uint32_t)8U, (uint32_t)13U); |
77 | 3.12M | quarter_round(st, (uint32_t)3U, (uint32_t)4U, (uint32_t)9U, (uint32_t)14U); |
78 | 3.12M | } |
79 | | |
80 | | static inline void |
81 | | rounds(uint32_t *st) |
82 | 312k | { |
83 | 312k | double_round(st); |
84 | 312k | double_round(st); |
85 | 312k | double_round(st); |
86 | 312k | double_round(st); |
87 | 312k | double_round(st); |
88 | 312k | double_round(st); |
89 | 312k | double_round(st); |
90 | 312k | double_round(st); |
91 | 312k | double_round(st); |
92 | 312k | double_round(st); |
93 | 312k | } |
94 | | |
95 | | static inline void |
96 | | chacha20_core(uint32_t *k, uint32_t *ctx, uint32_t ctr) |
97 | 312k | { |
98 | 312k | memcpy(k, ctx, (uint32_t)16U * sizeof(uint32_t)); |
99 | 312k | uint32_t ctr_u32 = ctr; |
100 | 312k | k[12U] = k[12U] + ctr_u32; |
101 | 312k | rounds(k); |
102 | 312k | KRML_MAYBE_FOR16(i, |
103 | 312k | (uint32_t)0U, |
104 | 312k | (uint32_t)16U, |
105 | 312k | (uint32_t)1U, |
106 | 312k | uint32_t *os = k; |
107 | 312k | uint32_t x = k[i] + ctx[i]; |
108 | 312k | os[i] = x;); |
109 | 312k | k[12U] = k[12U] + ctr_u32; |
110 | 312k | } |
111 | | |
112 | | static const uint32_t |
113 | | chacha20_constants[4U] = { (uint32_t)0x61707865U, (uint32_t)0x3320646eU, (uint32_t)0x79622d32U, (uint32_t)0x6b206574U }; |
114 | | |
115 | | void |
116 | | Hacl_Impl_Chacha20_chacha20_init(uint32_t *ctx, uint8_t *k, uint8_t *n, uint32_t ctr) |
117 | 304k | { |
118 | 304k | KRML_MAYBE_FOR4(i, |
119 | 304k | (uint32_t)0U, |
120 | 304k | (uint32_t)4U, |
121 | 304k | (uint32_t)1U, |
122 | 304k | uint32_t *os = ctx; |
123 | 304k | uint32_t x = chacha20_constants[i]; |
124 | 304k | os[i] = x;); |
125 | 304k | KRML_MAYBE_FOR8(i, |
126 | 304k | (uint32_t)0U, |
127 | 304k | (uint32_t)8U, |
128 | 304k | (uint32_t)1U, |
129 | 304k | uint32_t *os = ctx + (uint32_t)4U; |
130 | 304k | uint8_t *bj = k + i * (uint32_t)4U; |
131 | 304k | uint32_t u = load32_le(bj); |
132 | 304k | uint32_t r = u; |
133 | 304k | uint32_t x = r; |
134 | 304k | os[i] = x;); |
135 | 304k | ctx[12U] = ctr; |
136 | 304k | KRML_MAYBE_FOR3(i, |
137 | 304k | (uint32_t)0U, |
138 | 304k | (uint32_t)3U, |
139 | 304k | (uint32_t)1U, |
140 | 304k | uint32_t *os = ctx + (uint32_t)13U; |
141 | 304k | uint8_t *bj = n + i * (uint32_t)4U; |
142 | 304k | uint32_t u = load32_le(bj); |
143 | 304k | uint32_t r = u; |
144 | 304k | uint32_t x = r; |
145 | 304k | os[i] = x;); |
146 | 304k | } |
147 | | |
148 | | static void |
149 | | chacha20_encrypt_block(uint32_t *ctx, uint8_t *out, uint32_t incr, uint8_t *text) |
150 | 312k | { |
151 | 312k | uint32_t k[16U] = { 0U }; |
152 | 312k | chacha20_core(k, ctx, incr); |
153 | 312k | uint32_t bl[16U] = { 0U }; |
154 | 312k | KRML_MAYBE_FOR16(i, |
155 | 312k | (uint32_t)0U, |
156 | 312k | (uint32_t)16U, |
157 | 312k | (uint32_t)1U, |
158 | 312k | uint32_t *os = bl; |
159 | 312k | uint8_t *bj = text + i * (uint32_t)4U; |
160 | 312k | uint32_t u = load32_le(bj); |
161 | 312k | uint32_t r = u; |
162 | 312k | uint32_t x = r; |
163 | 312k | os[i] = x;); |
164 | 312k | KRML_MAYBE_FOR16(i, |
165 | 312k | (uint32_t)0U, |
166 | 312k | (uint32_t)16U, |
167 | 312k | (uint32_t)1U, |
168 | 312k | uint32_t *os = bl; |
169 | 312k | uint32_t x = bl[i] ^ k[i]; |
170 | 312k | os[i] = x;); |
171 | 312k | KRML_MAYBE_FOR16(i, |
172 | 312k | (uint32_t)0U, |
173 | 312k | (uint32_t)16U, |
174 | 312k | (uint32_t)1U, |
175 | 312k | store32_le(out + i * (uint32_t)4U, bl[i]);); |
176 | 312k | } |
177 | | |
178 | | static inline void |
179 | | chacha20_encrypt_last(uint32_t *ctx, uint32_t len, uint8_t *out, uint32_t incr, uint8_t *text) |
180 | 303k | { |
181 | 303k | uint8_t plain[64U] = { 0U }; |
182 | 303k | memcpy(plain, text, len * sizeof(uint8_t)); |
183 | 303k | chacha20_encrypt_block(ctx, plain, incr, plain); |
184 | 303k | memcpy(out, plain, len * sizeof(uint8_t)); |
185 | 303k | } |
186 | | |
187 | | void |
188 | | Hacl_Impl_Chacha20_chacha20_update(uint32_t *ctx, uint32_t len, uint8_t *out, uint8_t *text) |
189 | 304k | { |
190 | 304k | uint32_t rem = len % (uint32_t)64U; |
191 | 304k | uint32_t nb = len / (uint32_t)64U; |
192 | 304k | uint32_t rem1 = len % (uint32_t)64U; |
193 | 313k | for (uint32_t i = (uint32_t)0U; i < nb; i++) { |
194 | 9.13k | chacha20_encrypt_block(ctx, out + i * (uint32_t)64U, i, text + i * (uint32_t)64U); |
195 | 9.13k | } |
196 | 304k | if (rem1 > (uint32_t)0U) { |
197 | 303k | chacha20_encrypt_last(ctx, rem, out + nb * (uint32_t)64U, nb, text + nb * (uint32_t)64U); |
198 | 303k | } |
199 | 304k | } |
200 | | |
201 | | void |
202 | | Hacl_Chacha20_chacha20_encrypt( |
203 | | uint32_t len, |
204 | | uint8_t *out, |
205 | | uint8_t *text, |
206 | | uint8_t *key, |
207 | | uint8_t *n, |
208 | | uint32_t ctr) |
209 | 304k | { |
210 | 304k | uint32_t ctx[16U] = { 0U }; |
211 | 304k | Hacl_Impl_Chacha20_chacha20_init(ctx, key, n, ctr); |
212 | 304k | Hacl_Impl_Chacha20_chacha20_update(ctx, len, out, text); |
213 | 304k | } |
214 | | |
215 | | void |
216 | | Hacl_Chacha20_chacha20_decrypt( |
217 | | uint32_t len, |
218 | | uint8_t *out, |
219 | | uint8_t *cipher, |
220 | | uint8_t *key, |
221 | | uint8_t *n, |
222 | | uint32_t ctr) |
223 | 0 | { |
224 | 0 | uint32_t ctx[16U] = { 0U }; |
225 | 0 | Hacl_Impl_Chacha20_chacha20_init(ctx, key, n, ctr); |
226 | 0 | Hacl_Impl_Chacha20_chacha20_update(ctx, len, out, cipher); |
227 | 0 | } |