Skip to content
19 changes: 17 additions & 2 deletions dcrec/secp256k1/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,8 @@ structures and functions for working with public and private secp256k1 keys.

In addition, subpackages are provided to produce, verify, parse, and serialize
ECDSA signatures and EC-Schnorr-DCRv0 (a custom Schnorr-based signature scheme
specific to Decred) signatures. See the README.md files in the relevant sub
packages for more details about those aspects.
specific to Decred) signatures. See the README.md files in the relevant
subpackages for more details about those aspects.

## Features

Expand Down Expand Up @@ -95,6 +95,21 @@ secp256k1 elliptic curve cryptography.

The secp256k1 domain parameters are specified in [SEC 2: Recommended Elliptic Curve Domain Parameters](https://www.secg.org/sec2-v2.pdf).

## Caveats

Constant time implementations are designed to eliminate data dependent timing
variation at the algorithmic level. This property depends on the Go compiler
continuing to compile the relevant operations into constant-time machine
instructions.

This package also consistently uses temporary stack allocated buffers which it
attempts to clear in order to reduce the likelihood of sensitive data lingering
in memory, but Go does not guarantee such writes are never optimized away.

Significant effort has been made to ensure correctness including careful review
of the generated assembly, but it is impossible to guarantee exact behavior of
future versions of the Go compiler.

## secp256k1 use in Decred

At the time of this writing, the primary public key cryptography in widespread
Expand Down
7 changes: 4 additions & 3 deletions dcrec/secp256k1/common.go
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,10 @@ func constantTimeEq64(a, b uint64) uint32 {
return uint32(((t | -t) >> 63) ^ 1)
}

// constantTimeNotEq returns 1 if a != b or 0 otherwise in constant time.
func constantTimeNotEq(a, b uint32) uint32 {
return ^uint32((uint64(a^b)-1)>>63) & 1
// constantTimeNotEq64 returns 1 if a != b or 0 otherwise in constant time.
func constantTimeNotEq64(a, b uint64) uint32 {
t := a ^ b
return uint32(((t | -t) >> 63))
}

// constantTimeLess returns 1 if a < b or 0 otherwise in constant time.
Expand Down
54 changes: 20 additions & 34 deletions dcrec/secp256k1/curve.go
Original file line number Diff line number Diff line change
Expand Up @@ -720,16 +720,6 @@ func mulAdd64Carry(digit1, digit2, m, c uint64) (hi, lo uint64) {
// because it is used for replacing division with multiplication and thus the
// intermediate results must be done via a field extension to a larger field.
func mul512Rsh320Round(n1, n2 *ModNScalar) ModNScalar {
// Convert n1 and n2 to base 2^64 digits.
n1Digit0 := uint64(n1.n[0]) | uint64(n1.n[1])<<32
n1Digit1 := uint64(n1.n[2]) | uint64(n1.n[3])<<32
n1Digit2 := uint64(n1.n[4]) | uint64(n1.n[5])<<32
n1Digit3 := uint64(n1.n[6]) | uint64(n1.n[7])<<32
n2Digit0 := uint64(n2.n[0]) | uint64(n2.n[1])<<32
n2Digit1 := uint64(n2.n[2]) | uint64(n2.n[3])<<32
n2Digit2 := uint64(n2.n[4]) | uint64(n2.n[5])<<32
n2Digit3 := uint64(n2.n[6]) | uint64(n2.n[7])<<32

// Compute the full 512-bit product n1*n2.
var r0, r1, r2, r3, r4, r5, r6, r7, c uint64

Expand All @@ -738,40 +728,40 @@ func mul512Rsh320Round(n1, n2 *ModNScalar) ModNScalar {
//
// Note that r0 is ignored because it is not needed to compute the higher
// terms and it is shifted out below anyway.
c, _ = bits.Mul64(n2Digit0, n1Digit0)
c, r1 = mulAdd64(n2Digit0, n1Digit1, c)
c, r2 = mulAdd64(n2Digit0, n1Digit2, c)
r4, r3 = mulAdd64(n2Digit0, n1Digit3, c)
c, _ = bits.Mul64(n2.n[0], n1.n[0])
c, r1 = mulAdd64(n2.n[0], n1.n[1], c)
c, r2 = mulAdd64(n2.n[0], n1.n[2], c)
r4, r3 = mulAdd64(n2.n[0], n1.n[3], c)

// Terms resulting from the product of the second digit of the second number
// by all digits of the first number.
//
// Note that r1 is ignored because it is no longer needed to compute the
// higher terms and it is shifted out below anyway.
c, _ = mulAdd64(n2Digit1, n1Digit0, r1)
c, r2 = mulAdd64Carry(n2Digit1, n1Digit1, r2, c)
c, r3 = mulAdd64Carry(n2Digit1, n1Digit2, r3, c)
r5, r4 = mulAdd64Carry(n2Digit1, n1Digit3, r4, c)
c, _ = mulAdd64(n2.n[1], n1.n[0], r1)
c, r2 = mulAdd64Carry(n2.n[1], n1.n[1], r2, c)
c, r3 = mulAdd64Carry(n2.n[1], n1.n[2], r3, c)
r5, r4 = mulAdd64Carry(n2.n[1], n1.n[3], r4, c)

// Terms resulting from the product of the third digit of the second number
// by all digits of the first number.
//
// Note that r2 is ignored because it is no longer needed to compute the
// higher terms and it is shifted out below anyway.
c, _ = mulAdd64(n2Digit2, n1Digit0, r2)
c, r3 = mulAdd64Carry(n2Digit2, n1Digit1, r3, c)
c, r4 = mulAdd64Carry(n2Digit2, n1Digit2, r4, c)
r6, r5 = mulAdd64Carry(n2Digit2, n1Digit3, r5, c)
c, _ = mulAdd64(n2.n[2], n1.n[0], r2)
c, r3 = mulAdd64Carry(n2.n[2], n1.n[1], r3, c)
c, r4 = mulAdd64Carry(n2.n[2], n1.n[2], r4, c)
r6, r5 = mulAdd64Carry(n2.n[2], n1.n[3], r5, c)

// Terms resulting from the product of the fourth digit of the second number
// by all digits of the first number.
//
// Note that r3 is ignored because it is no longer needed to compute the
// higher terms and it is shifted out below anyway.
c, _ = mulAdd64(n2Digit3, n1Digit0, r3)
c, r4 = mulAdd64Carry(n2Digit3, n1Digit1, r4, c)
c, r5 = mulAdd64Carry(n2Digit3, n1Digit2, r5, c)
r7, r6 = mulAdd64Carry(n2Digit3, n1Digit3, r6, c)
c, _ = mulAdd64(n2.n[3], n1.n[0], r3)
c, r4 = mulAdd64Carry(n2.n[3], n1.n[1], r4, c)
c, r5 = mulAdd64Carry(n2.n[3], n1.n[2], r5, c)
r7, r6 = mulAdd64Carry(n2.n[3], n1.n[3], r6, c)

// At this point the upper 256 bits of the full 512-bit product n1*n2 are in
// r4..r7 (recall the low order results were discarded as noted above).
Expand All @@ -796,14 +786,10 @@ func mul512Rsh320Round(n1, n2 *ModNScalar) ModNScalar {
// less than the group order given the group order is > 2^255 and the
// maximum possible value of the result is 2^192.
var result ModNScalar
result.n[0] = uint32(r0)
result.n[1] = uint32(r0 >> 32)
result.n[2] = uint32(r1)
result.n[3] = uint32(r1 >> 32)
result.n[4] = uint32(r2)
result.n[5] = uint32(r2 >> 32)
result.n[6] = uint32(r3)
result.n[7] = uint32(r3 >> 32)
result.n[0] = r0
result.n[1] = r1
result.n[2] = r2
result.n[3] = r3
return result
}

Expand Down
20 changes: 4 additions & 16 deletions dcrec/secp256k1/curve_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -877,28 +877,16 @@ func TestScalarBaseMultJacobian(t *testing.T) {
// modNBitLen returns the minimum number of bits required to represent the mod n
// scalar. The result is 0 when the value is 0.
func modNBitLen(s *ModNScalar) uint16 {
if w := s.n[7]; w > 0 {
return uint16(bits.Len32(w)) + 224
}
if w := s.n[6]; w > 0 {
return uint16(bits.Len32(w)) + 192
}
if w := s.n[5]; w > 0 {
return uint16(bits.Len32(w)) + 160
}
if w := s.n[4]; w > 0 {
return uint16(bits.Len32(w)) + 128
}
if w := s.n[3]; w > 0 {
return uint16(bits.Len32(w)) + 96
return uint16(bits.Len64(w)) + 192
}
if w := s.n[2]; w > 0 {
return uint16(bits.Len32(w)) + 64
return uint16(bits.Len64(w)) + 128
}
if w := s.n[1]; w > 0 {
return uint16(bits.Len32(w)) + 32
return uint16(bits.Len64(w)) + 64
}
return uint16(bits.Len32(s.n[0]))
return uint16(bits.Len64(s.n[0]))
}

// checkLambdaDecomposition returns an error if the provided decomposed scalars
Expand Down
15 changes: 15 additions & 0 deletions dcrec/secp256k1/doc.go
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,21 @@ use optimized secp256k1 elliptic curve cryptography.
Finally, a comprehensive suite of tests is provided to provide a high level of
quality assurance.

## Caveats

Constant time implementations are designed to eliminate data dependent timing
variation at the algorithmic level. This property depends on the Go compiler
continuing to compile the relevant operations into constant time machine
instructions.

This package also consistently uses temporary stack allocated buffers which it
attempts to clear in order to reduce the likelihood of sensitive data lingering
in memory, but Go does not guarantee such writes are never optimized away.

Significant effort has been made to ensure correctness, including careful review
of the generated assembly, but it is impossible to guarantee exact behavior of
future versions of the Go compiler.

# Use of secp256k1 in Decred

At the time of this writing, the primary public key cryptography in widespread
Expand Down
18 changes: 10 additions & 8 deletions dcrec/secp256k1/field64.go
Original file line number Diff line number Diff line change
Expand Up @@ -799,9 +799,10 @@ func field64Square512(t *[8]uint64, a *[4]uint64) {
// The p5 carry is safe to discard because p5 + h13 + c ≤ 2^64 - 1 (where c
// is the carry from p4 + l13).
//
// A full proof involves case work that is omitted here, but the key point
// is that the only way the final add could have a carry is if all 3 of the
// following conditions were simultaneously true:
// A full proof involves case analysis that is omitted here since the
// impossibility of the carry is formally proven in internal/proofs, but the
// key point is that the only way the final add could have a carry is if all
// 3 of the following conditions were simultaneously true:
//
// 1) p5_old = 1 (the carry from the earlier chain, so ≤ 1)
// 2) h13 = 2^64 - 2 (h13 ≤ 2^64 - 2 as proven previously)
Expand Down Expand Up @@ -891,14 +892,15 @@ func field64Reduce512(r *[4]uint64, x *[8]uint64) {

h, t0 = bits.Mul64(x[4], field64PrimeComplement)

// Note that since hi is the upper 64 bits of the product of two uint64s:
// h3 ≤ floor((2^64-1)^2 / 2^64) = 2^64 - 2
// Note that since hi is the upper 64 bits of the product of a uint64 with
// c and c < 2^33:
// hi ≤ floor((2^64-1)(2^33 - 1) / 2^64) = 2^33 - 2
//
// Then, because c ≤ 1, a loose bound is:
// p4h3 + 1 = 2^64 - 1 < 2^64
// Then, because carry ≤ 1, a loose bound for h is:
// hhi + 1 = 2^33 - 1 < 2^64
//
// Therefore, it is safe to discard the carry and the same applies to the
// next two limbs.
// next two limbs (second h and first t4).
hi, lo = bits.Mul64(x[5], field64PrimeComplement)
t1, carry = bits.Add64(lo, h, 0)
h, _ = bits.Add64(hi, 0, carry)
Expand Down
4 changes: 2 additions & 2 deletions dcrec/secp256k1/field_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -1307,7 +1307,7 @@ func TestFieldMulInt(t *testing.T) {
in2: 5,
expected: "6cf4eb20f2447c77657fccb172d38c0aa91ea4ac446dc641fa463a6b5091fba7",
}, {
name: "random sampling #3",
name: "random sampling #4",
in1: "fb4529be3e027a3d1587d8a500b72f2d312e3577340ef5175f96d113be4c2ceb",
in2: 8,
expected: "da294df1f013d1e8ac3ec52805b979698971abb9a077a8bafcb688a4f261820f",
Expand Down Expand Up @@ -1369,7 +1369,7 @@ func TestFieldMul(t *testing.T) {
in2: "3",
expected: "0",
}, {
name: "secp256k1 prime * 3",
name: "secp256k1 prime * 8",
in1: "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e",
in2: "8",
expected: "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc27",
Expand Down
9 changes: 7 additions & 2 deletions dcrec/secp256k1/internal/proofs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,9 @@ proofs
This consists of formal verification artifacts used to help establish the
correctness of the security-critical arithmetic implementations.

The current proofs formally verify properties of the optimized field arithmetic
implementations using [z3](https://github.com/Z3Prover/z3):
The current proofs formally verify properties of the optimized scalar and field
arithmetic implementations using the [Z3 Theorem
Prover](https://github.com/Z3Prover/z3):

- Correctness of multi-precision multiplication
- Bounds on intermediate values
Expand Down Expand Up @@ -45,3 +46,7 @@ optimized implementations preserve the required arithmetic invariants.
- [Field Modular Reduction](field_4x64_reduce_prover.py)
Provides formal verification of the reduction of a 512-bit value represented
using saturated 64-bit limbs modulo the secp256k1 prime.

- [Scalar Modular Reduction](modnscalar_4x64_reduce_prover.py)
Provides formal verification of the reduction of a 512-bit value represented
using saturated 64-bit limbs modulo the secp256k1 group order.
Loading