Skip to content

Commit 705dfb3

Browse files
utzigutzig
committed
Add third_party/fiat from boringssl
This adds the boringssl version of fiat-crypto. The version bundled here had most if its non-used code removed, like signing, X25519 curve operations not required by verification, etc. Under boringssl tree, fiat can be found in third_party/fiat. The version included here comes from a boringssl tree where the last commit is f109f2087349712d3ac717d15fab48e130618110. Signed-off-by: Fabio Utzig <[email protected]>
1 parent 8101d1f commit 705dfb3

File tree

7 files changed

+2167
-0
lines changed

7 files changed

+2167
-0
lines changed

‎ext/fiat/LICENSE‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
The MIT License (MIT)
2+
3+
Copyright (c) 2015-2016 the fiat-crypto authors (see
4+
https://github.com/mit-plv/fiat-crypto/blob/master/AUTHORS).
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.

‎ext/fiat/METADATA‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
name: "fiat"
2+
description: "Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives."
3+
4+
third_party {
5+
url {
6+
type: GIT
7+
value: "https://github.com/mit-plv/fiat-crypto"
8+
}
9+
version: "4441785fb44b88bb6943ddbf639d872c8c903281"
10+
last_upgrade_date { year: 2019 month: 1 day: 16 }
11+
12+
local_modifications: "Fiat-generated code has been integrated into existing BoringSSL code"
13+
}

‎ext/fiat/README.chromium‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
Name: Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives
2+
Short Name: fiat-crypto
3+
URL: https://github.com/mit-plv/fiat-crypto
4+
Version: git (see METADATA)
5+
License: MIT
6+
License File: LICENSE
7+
Security Critical: yes
8+
9+
Description:
10+
See README.md and METADATA.

‎ext/fiat/README.md‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
# Fiat
2+
3+
Some of the code in this directory is generated by
4+
[Fiat](https://github.com/mit-plv/fiat-crypto) and thus these files are
5+
licensed under the MIT license. (See LICENSE file.)
6+
7+
## Curve25519
8+
9+
To generate the field arithmetic procedures in `curve25519.c` from a fiat-crypto
10+
checkout (as of `7892c66d5e0e5770c79463ce551193ceef870641`), run
11+
`make src/Specific/solinas32_2e255m19_10limbs/femul.c` (replacing `femul` with
12+
the desired field operation). The "source" file specifying the finite field and
13+
referencing the desired implementation strategy is
14+
`src/Specific/solinas32_2e255m19_10limbs/CurveParameters.v`, specifying roughly
15+
"unsaturated arithmetic modulo 2^255-19 using 10 limbs of radix 2^25.5 in 32-bit
16+
unsigned integers with a single carry chain and two wraparound carries" where
17+
only the prime is considered normative and everything else is treated as
18+
"compiler hints".
19+
20+
The 64-bit implementation uses 5 limbs of radix 2^51 with instruction scheduling
21+
taken from curve25519-donna-c64. It is found in
22+
`src/Specific/solinas64_2e255m19_5limbs_donna`.
23+
24+
## P256
25+
26+
To generate the field arithmetic procedures in `p256.c` from a fiat-crypto
27+
checkout, run
28+
`make src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/femul.c`.
29+
The corresponding "source" file is
30+
`src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/CurveParameters.v`,
31+
specifying roughly "64-bit saturated word-by-word Montgomery reduction modulo
32+
2^256 - 2^224 + 2^192 + 2^96 - 1". Again, everything except for the prime is
33+
untrusted. There is currently a known issue where `fesub.c` for p256 does not
34+
manage to complete the build (specialization) within a week on Coq 8.7.0.
35+
<https://github.com/JasonGross/fiat-crypto/tree/3e6851ddecaac70d0feb484a75360d57f6e41244/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs>
36+
does manage to build that file, but the work on that branch was never finished
37+
(the correctness proofs of implementation templates still apply, but the
38+
now abandoned prototype specialization facilities there are unverified).
39+
40+
## Working With Fiat Crypto Field Arithmetic
41+
42+
The fiat-crypto readme <https://github.com/mit-plv/fiat-crypto#arithmetic-core>
43+
contains an overview of the implementation templates followed by a tour of the
44+
specialization machinery. It may be helpful to first read about the less messy
45+
parts of the system from chapter 3 of <http://adam.chlipala.net/theses/andreser.pdf>.
46+
There is work ongoing to replace the entire specialization mechanism with
47+
something much more principled <https://github.com/mit-plv/fiat-crypto/projects/4>.

0 commit comments

Comments
 (0)