Notes from a deep dive into BoringSSL's Curve25519 code on June 19, 2020, with an eye for finding the path to a fully verified high-level crypto operation using bedrock2, fiat-crypto, and rupicola. # Crypto operations These are the top-level operations, and depend on *scalar* (function names usually include `sc`), *group* (`ge`), and *field* (`fe`) operations. Note that "scalar" here does not actually mean scalar in the usual sense; the "scalars" are members of a field modulo a parameter called _l_, which is simply a prime field with a different modulus than the one used for "field" elements. There are two top-level schemes provided in BoringSSL for Curve25519: Ed25519 and X25519 ([more on Curve25519 naming](https://mailarchive.ietf.org/arch/msg/cfrg/-9LEdnzVrE5RORux3Oo_oDDRksU/)). Ed25519 is the signature system using Edwards coordinates, and X25519 is the scheme using Montgomery X-coordinates and Diffie-Hellman. Both operations use the same underlying curve. These functions also depend on some SHA512 operations which are mentioned here in parentheses but not expanded. `x25519_NEON` is also omitted (it is only used if `BORINGSSL_X25519_NEON` is defined). ## Implementation links [ED25519_keypair](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1879) [ED25519_sign](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1885) [ED25519_verify](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1924) [X25519_keypair](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#2100) ## Callees ### Ed25519 - Scalar : `x25519_sc_reduce` `scmuladd` - Group : `x25519_ge_scalarmult_base` `x25519_ge_frombytes_vartime` `ge_double_scalarmult_vartime` `x25519_ge_tobytes` `ge_p3_tobytes` - Field : `fe_neg` `fe_carry` ### X25519 - Group : `x25519_ge_scalarmult_base` `x25519_scalar_mult` - Field : `fe_add` `fe_sub` `fe_loose_invert` `fe_mul_tlt` `fe_tobytes` ## Code graph Here, and elsewhere, a `*` indicates a function that is low-level enough to generate in fiat-crypto's AST but is currently not generated, and `+` indicates a function that is already implemented with fiat-crypto's generated code. ``` ED25519_keypair | (RAND_bytes) | ED25519_keypair_from_seed | (SHA512, OPENSSL_memcpy) | x25519_ge_scalarmult_base | ge_p3_tobytes ED25519_sign | (SHA512, SHA512_Init, SHA512_Update, SHA512_Final) | * x25519_sc_reduce | x25519_ge_scalarmult_base | * sc_muladd ED25519_verify | (OPENSSL_memcpy, SHA512_Init, SHA512_Update, SHA512_Final, CRYPTO_memcmp) | x25519_ge_frombytes_vartime | + fe_neg | + fe_carry | * x25519_sc_reduce | ge_double_scalarmult_vartime | x25519_ge_tobytes X25519_keypair | (RAND_bytes) | X25519_public_from_private | (OPENSSL_memcpy) | x25519_ge_scalarmult_base | + fe_add | + fe_sub | + fe_loose_invert | + fe_mul_tlt | + fe_tobytes X25519 | (CRYPTO_memcmp) | x25519_scalar_mult ``` # Scalar Operations The top-level functions rely on just two scalar operations: `x25519_sc_reduce` and `sc_muladd`. Both are low-level enough to be generated by fiat-crypto, in theory, and could probably reuse parts of the field arithmetic infrastructure. However, they might also include low-level optimizations at a similar level of complexity to field arithmetic. (See [https://github.com/mit-plv/fiat-crypto/issues/805](https://github.com/mit-plv/fiat-crypto/issues/805) for some discussion). `x25519_sc_reduce` implements full modular reduction (like `freeze`). `sc_muladd(a, b, c)` produces `(ab + c) mod l`. Also full modular reduction, although implementation looks like Solinas. ## Implementation links [x25519_sc_reduce](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1057) [sc_muladd](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#1398) ## Callees None # Group Operations These operations manipulate curve points (members of the curve algebraic group). They depend on field operations mostly, but also a few uncategorized helpers (here listed as "misc"). The function `x25519_scalar_mult` corresponds to `montladder` in the fiat-crypto repository and a bedrock2 version exists in rupicola, but has not at the time of writing been integrated to BoringSSL or proven to connect to the specifications of the field operations. Note" `x25519_ge_scalarmult` is also defined and used in the SPAKE2 protocol, but not for the core Ed25519. ## Implementation links [x25519_ge_tobytes](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#479) [ge_p3_tobytes](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#491) [x25519_ge_frombytes_vartime](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#503) [ge_p3_0](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#555) [ge_cached_0](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#569) [ge_p3_to_p2](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#576) [x25519_ge_p3_to_cached](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#583) [x25519_ge_p1p1_to_p2](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#591) [x25519_ge_p1p1_to_p3](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#598) [ge_p2_dbl](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#613) [ge_p3_dbl](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#632) [ge_madd](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#639) [ge_msub](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#656) [x25519_ge_add](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#673) [x25519_ge_sub](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#691) [cmov](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#718) [x25519_ge_scalarmult_small_precomp](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#724) [x25519_ge_scalarmult_base (if OPENSSL_SMALL defined)](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#780) [table_select](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#792) [x25519_ge_scalarmult_base (if OPENSSL_SMALL undefined)](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#823) [ge_double_scalarmult_vartime](https://boringssl.googlesource.com/boringssl/+/cbac9c3a2d20a05d5c634eaab8f8b07589838d57/crypto/curve25519/curve25519.c#972) ## Callees - Field: `fe_frombytes` `fe_0` `fe_1` `fe_cswap` `fe_add` `fe_sub` `fe_mul_impl` `fe_sq_tl` `fe_mul121666` `fe_invert` `fe_tobytes` `fe_frombytes_strict` `fe_cmov` `fe_copy_ll` `fe_carry` `fe_neg` `fe_copy_lt` `fe_copy` `fe_sq_tt` `fe_sq2_tt` `fe_isnonzero` `fe_isnegative` `fe_invert` `fe_loose_0` `fe_loose_1` `fe_pow22523` - Misc: `equal` `negative` `slide` Note: `fe_mul_impl` is called through various wrappers: `fe_mul_ltt` `fe_mul_llt` `fe_mul_ttt` `fe_mul_tlt` `fe_mul_ttl` `fe_mul_tll`. ## Code graph Starting from callees of crypto operations. ``` x25519_scalar_mult | x25519_scalar_mult_generic | + fe_frombytes | * fe_1 | * fe_0 | * fe_copy | * fe_cswap | + fe_sub | + fe_add | + fe_mul_tll | + fe_sq_tl | + fe_mul121666 | + fe_mul_ttt | fe_invert | + fe_tobytes x25519_ge_scalarmult_base (if OPENSSSL_SMALL defined) | x25519_ge_scalarmult_small_precomp | + fe_frombytes_strict | + fe_add | + fe_sub | + fe_mul_ltt | ge_p3_0 | * fe_0 | * fe_1 | * equal | cmov | * fe_cmov | * fe_copy_ll | + fe_carry | + fe_neg | x25519_ge_p3_to_cached | + fe_add | + fe_sub | * fe_copy_lt | + fe_mul_llt | x25519_ge_add | + fe_add | + fe_sub | + fe_mul_tll | + fe_carry | x25519_ge_p1p1_to_p3 | + fe_mul_tll x25519_ge_scalarmult_base (if OPENSSL_SMALL undefined) | ge_p3_0 | * fe_0 | * fe_1 | table_select | ge_precomp_0 | * fe_loose_1 | * fe_loose_0 | * negative | * equal | cmov | * fe_cmov | * fe_copy_ll | + fe_carry | + fe_neg | * fe_copy_ll | + fe_carry | + fe_neg | ge_madd | + fe_add | + fe_sub | + fe_mul_tll | + fe_carry | x25519_ge_p1p1_to_p3 | + fe_mul_tll | ge_p3_dbl | ge_p3_to_p2 | * fe_copy | ge_p2_dbl | + fe_sq_tt | fe_sq2_tt | + fe_add | + fe_sq_tl | + fe_sub | + fe_carry | + fe_sub | x25519_ge_p1p1_to_p2 | + fe_mul_tll x25519_ge_frombytes_vartime | + fe_frombytes | * fe_1 | + fe_sq_tt | + fe_mul_ttt | + fe_sub | + fe_carry | + fe_add | + fe_sq_tl | + fe_mul_ttl | * fe_pow22523 | fe_isnonzero | fe_isnegative ge_double_scalarmult_vartime | * slide | x25519_ge_p3_to_cached | + fe_add | + fe_sub | * fe_copy_lt | + fe_mul_llt | ge_p3_dbl | ge_p3_to_p2 | * fe_copy | ge_p2_dbl | + fe_sq_tt | fe_sq2_tt | + fe_add | + fe_sq_tl | + fe_sub | + fe_carry | + fe_sub | x25519_ge_p1p1_to_p3 | + fe_mul_tll | x25519_ge_add | + fe_add | + fe_sub | + fe_mul_tll | + fe_mul_tlt | + fe_mul_ttl | + fe_carry | x25519_ge_sub | + fe_add | + fe_sub | + fe_mul_tll | + fe_mul_tlt | + fe_mul_ttl | + fe_carry | ge_p2_dbl | + fe_sq_tt | fe_sq2_tt | + fe_add | + fe_sq_tl | + fe_sub | + fe_carry | + fe_sub | ge_madd | + fe_add | + fe_sub | + fe_mul_tll | + fe_carry | ge_msub | + fe_add | + fe_sub | + fe_mul_tll | + fe_mul_tlt | + fe_carry x25519_ge_tobytes | fe_invert | + fe_mul_ttt | + fe_tobytes | fe_isnegative ge_p3_tobytes | fe_invert | + fe_mul_ttt | + fe_tobytes | fe_isnegative ``` # Field Operations Mostly, these are complete. However, there are a couple that aren't and seem easy to verify given our existing proven operations. The functions that are just wrappers (with bounds assertions) for calls to fiat-crypto generated code are: `fe_frombytes_strict` `fe_tobytes` `fe_add` `fe_sub` `fe_carry` `fe_mul_impl` `fe_sq_tl` `fe_sq_tt` `fe_mul_121666` `fe_neg` Additionally, the following functions are fairly trivial wrappers for the ones listed above: `fe_frombytes` `fe_mul_ltt` `fe_mul_llt` `fe_mul_ttt` `fe_mul_tlt` `fe_mul_ttl` `fe_mul_tll` There's a bit of a special case with`fe_cmov`; it should use fiat-crypto's `selectznz`, but there's a TODO in the codebase to make the calling conventions match up. That leaves the following field operations: - `fe_0` `fe_loose_0` `fe_1` `fe_loose_1` : literal 0s and 1s - `fe_cswap`: conditional swap of field elements - `fe_copy` `fe_copy_lt` `fe_copy_ll`: copying content of field elements - `fe_loose_invert` : inversion (there's a PR on fiat-crypto that does inversion -- is it the same algorithm?) - `fe_invert` : inversion (wrapper for `fe_loose_invert`) - `fe_isnonzero` : converts to bytes and checks if the bytes are 0 - `fe_isnegative` : converts to bytes and checks if odd - `fe_sq2_tt` : calls `fe_sq_tt` and adds result to itself - `fe_pow22523`: sequence of squares and multiplications All of these should be very reasonable to write in bedrock2 and prove correct against existing field operations (with the exception of inversion, if the PR is a different algorithm). In terms of value added by verification, `fe_pow22523` is probably the best, while `fe_sq2_tt`, `fe_isnonzero`, and `fe_isnegative` would be reasonable. ### Code graph Operations not listed here have no callees at the field level or above. ``` fe_sq2_tt | + fe_sq_tt | + fe_add | + fe_carry fe_invert | * fe_copy_lt | fe_loose_invert | + fe_sq_tl | + fe_sq_tt | + fe_mul_tlt | + fe_mul_ttt fe_isnonzero | + fe_carry | + fe_tobytes fe_isnegative | + fe_tobytes fe_pow22523 | + fe_sq_tt | + fe_mul_ttt ``` # Misc Operations The group level relies on a few self-contained helper functions: - `slide` is probably something to do with "sliding window"; it transforms an array of bytes with low-level computations. Unclear what the specification should be, but otherwise reasonable to write up in bedrock2. - `negative` computes whether a signed byte is negative (not suitable for bedrock2, probably, because it involves typecasting to larger integers) - `equal` computes whether two signed bytes are equal (not suitable for bedrock2, probably, because it involves typecasting to larger integers)