Home | History | Annotate | only in /external/boringssl/src/third_party/fiat
Up to higher level directory
NameDateSize
BUILD.gn21-Aug-2018216
CMakeLists.txt21-Aug-201884
curve25519.c21-Aug-201896.1K
curve25519_tables.h21-Aug-2018270K
internal.h21-Aug-20184.7K
LICENSE21-Aug-20181.1K
make_curve25519_tables.py21-Aug-20186.9K
METADATA21-Aug-2018413
p256.c21-Aug-201878.1K
README.chromium21-Aug-2018286
README.md21-Aug-20182.5K

README.chromium

      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.
     11

README.md

      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>.
     48