https://github.com/mit-plv/fiat-crypto
Tip revision: b64e689afd0e77f2802a07c0c3c4e95e650ff89a authored by Andres Erbsen on 14 December 2020, 19:06:44 UTC
do not use a precomputed table in ed25519 sign
do not use a precomputed table in ed25519 sign
Tip revision: b64e689
boringssl_notes.md
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)