Skip to content

Latest commit

 

History

History
404 lines (341 loc) · 13.3 KB

boringssl_notes.md

File metadata and controls

404 lines (341 loc) · 13.3 KB
Raw

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). 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 ED25519_sign ED25519_verify X25519_keypair

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 mit-plv#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 sc_muladd

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 ge_p3_tobytes x25519_ge_frombytes_vartime ge_p3_0 ge_cached_0 ge_p3_to_p2 x25519_ge_p3_to_cached x25519_ge_p1p1_to_p2 x25519_ge_p1p1_to_p3 ge_p2_dbl ge_p3_dbl ge_madd ge_msub x25519_ge_add x25519_ge_sub cmov x25519_ge_scalarmult_small_precomp x25519_ge_scalarmult_base (if OPENSSL_SMALL defined) table_select x25519_ge_scalarmult_base (if OPENSSL_SMALL undefined) ge_double_scalarmult_vartime

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 withfe_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)