ECDSA sample code

[hannesm]

Hi,

thanks for your very nice work on fiat. We are using it (https://github.com/mirage/fiat) - with (not verfied) inversion, point_double and point_add function to compute ECDH P256. Now I've a question for developing ECDSA (P256) support, where I miss some functionality (or: are you aware of third-part C code implementing them - I was not able to sufficiently understand boringssl?):

• constant time inversion (modulo n) -- as far as I can tell the inv is modulo the prime p?
• constant time multiplication (modulo n) - again, it is modulo p

Thanks again for your time.

[andres-erbsen]

Hi, and thanks for your interest. If I understand correctly, you are asking about multiplication and inversion modulo the order of the P256 group -- please correct me if I am wrong. We do not have pregenerated code for this, and we haven't tried out this field before (I think), but it may still work out anyway:

• I think you should be able to follow these instructions to generate multiplication for the desired modulus. The code generation will likely only work with Montgomery strategy, which I think is not optimal for usage in ECDSA, but I think this operation makes up a small enough fraction of the total running time that even the suboptimal code would be workable.
• For inversion, I think the best way to use fiat-crypto would be to try out the freshly-merged constant-time Euclidian inversion template. I have not looked into it personally, but I hear it can generate C code. We'd be happy to work with you to figure out any rough edges. @JasonGross what would be a good way to get started? I think we also have Gallina code for Fermat's inversion, but it does not go down to C and it relies on multiplication, so I would expect it to be actually slow in the current situation.

[JasonGross]

@JasonGross what would be a good way to get started?

You will now automatically get divstep code when you invoke the montgomery binary. Examples of turning divstep into inversion via a loop are at, e.g.,

fiat-crypto/inversion-c/p224_64.c

Lines 1 to 9 in 84eba63

	#include "../fiat-c/src/p224_64.c"
	#define LIMBS 4 /* amount of limbs pr. large integer in montgomery domain, see montgomery_inversion */
	#define WORD uint64_t
	#define WORDSIZE 64 /* wordsize */
	#define LEN_PRIME 224 /* length of the prime in bits */
	#define CURVE_DESCRIPTION fiat_p224
	#include "inversion_template.c"

[hannesm]

Thanks for your replies, I'll look into that later this week. A brief note on performance: this is not critical, I'm more interested in the extraction with a constant time behavior (better constant time and safe than fast and sorry).

[andres-erbsen]

The C code our tools generate is intended to be straightforwardly compilable to constant-time machinecode for machines with constant-time multiplication and cmov. As it's C, there is always some chance (and precedent) that a compiler change might optimize our bit manipulation into a branch, so it's best to check.

[spitters]

Constant time inversion is now available:
#670

[hannesm]

thanks for your kind comments and fixes (e31a36d), I managed to generate code for n, the order of g, with word_by_word_montgomery, and implemented the remaining bits necessary in OCaml (see mirage/mirage-crypto#101 -- this passes an initial test vector).