8c7c6356e6
- In base.h, if BORINGSSL_PREFIX is defined, include boringssl_prefix_symbols.h - In all .S files, if BORINGSSL_PREFIX is defined, include boringssl_prefix_symbols_asm.h - In base.h, BSSL_NAMESPACE_BEGIN and BSSL_NAMESPACE_END are defined with appropriate values depending on whether BORINGSSL_PREFIX is defined; these macros are used in place of 'namespace bssl {' and '}' - Add util/make_prefix_headers.go, which takes a list of symbols and auto-generates the header files mentioned above - In CMakeLists.txt, if BORINGSSL_PREFIX and BORINGSSL_PREFIX_SYMBOLS are defined, run util/make_prefix_headers.go to generate header files - In various CMakeLists.txt files, add "global_target" that all targets depend on to give us a place to hook logic that must run before all other targets (in particular, the header file generation logic) - Document this in BUILDING.md, including the fact that it is the caller's responsibility to provide the symbol list and keep it up to date - Note that this scheme has not been tested on Windows, and likely does not work on it; Windows support will need to be added in a future commit Change-Id: If66a7157f46b5b66230ef91e15826b910cf979a2 Reviewed-on: https://boringssl-review.googlesource.com/31364 Commit-Queue: David Benjamin <davidben@google.com> CQ-Verified: CQ bot account: commit-bot@chromium.org <commit-bot@chromium.org> Reviewed-by: David Benjamin <davidben@google.com> |
||
---|---|---|
.. | ||
BUILD.gn | ||
curve25519_tables.h | ||
curve25519.c | ||
internal.h | ||
LICENSE | ||
make_curve25519_tables.py | ||
METADATA | ||
p256.c | ||
README.chromium | ||
README.md |
Fiat
Some of the code in this directory is generated by Fiat and thus these files are licensed under the MIT license. (See LICENSE file.)
Curve25519
To generate the field arithmetic procedures in curve25519.c
from a fiat-crypto
checkout (as of 7892c66d5e0e5770c79463ce551193ceef870641
), run
make src/Specific/solinas32_2e255m19_10limbs/femul.c
(replacing femul
with
the desired field operation). The "source" file specifying the finite field and
referencing the desired implementation strategy is
src/Specific/solinas32_2e255m19_10limbs/CurveParameters.v
, specifying roughly
"unsaturated arithmetic modulo 2^255-19 using 10 limbs of radix 2^25.5 in 32-bit
unsigned integers with a single carry chain and two wraparound carries" where
only the prime is considered normative and everything else is treated as
"compiler hints".
The 64-bit implementation uses 5 limbs of radix 2^51 with instruction scheduling
taken from curve25519-donna-c64. It is found in
src/Specific/solinas64_2e255m19_5limbs_donna
.
P256
To generate the field arithmetic procedures in p256.c
from a fiat-crypto
checkout, run
make src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/femul.c
.
The corresponding "source" file is
src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/CurveParameters.v
,
specifying roughly "64-bit saturated word-by-word Montgomery reduction modulo
2^256 - 2^224 + 2^192 + 2^96 - 1". Again, everything except for the prime is
untrusted. There is currently a known issue where fesub.c
for p256 does not
manage to complete the build (specialization) within a week on Coq 8.7.0.
https://github.com/JasonGross/fiat-crypto/tree/3e6851ddecaac70d0feb484a75360d57f6e41244/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs
does manage to build that file, but the work on that branch was never finished
(the correctness proofs of implementation templates still apply, but the
now abandoned prototype specialization facilities there are unverified).
Working With Fiat Crypto Field Arithmetic
The fiat-crypto readme https://github.com/mit-plv/fiat-crypto#arithmetic-core contains an overview of the implementation templates followed by a tour of the specialization machinery. It may be helpful to first read about the less messy parts of the system from chapter 3 of http://adam.chlipala.net/theses/andreser.pdf. There is work ongoing to replace the entire specialization mechanism with something much more principled https://github.com/mit-plv/fiat-crypto/projects/4.