mirage-crypto-ec: implementation of SECP256K1

[ansiwen]

This change implements the SECP256K1 curve (also known as the Bitcoin curve).

• field primitives are generated by the fiat-crypto project[1]
• point primitives are generated by the ECCKiila project[2]
• Ocaml point operations are taken from NIST implementation, adapted to ECCKiila point primitives and optimized for a=0.
• testvectors for ECDH and ECDSA verification from wycheproof[3]

Closes: #187

[1] https://github.com/mit-plv/fiat-crypto
[2] https://gitlab.com/nisec/ecckiila
[3] https://github.com/C2SP/wycheproof

[ansiwen]

CI failures seem to be unrelated.

[ansiwen]

As an alternative I can also migrate the NIST curves to ECCKiila code, which is about 10% faster and would make the code simpler and more unified.

On my Mac (M3, arm64)
old:

P256:  21248.700 ops per second (225225 iters in 10.599)

ecckiila:

P256:  24023.883 ops per second (250000 iters in 10.406)

[ansiwen]

FWIW: I will also implement Brainpool curves. Please let me know, if you are interested in these as well.

[hannesm]

Thank you for your PR. Now, I have some questions:

• what license is ECCkiila, is it fine to embed the code?
• could you follow the other curve implementations and have the code generated by fiat added to the ec/native/GNUmakefile, so we can at any point when fiat updates generate these C files?
• where are the unit tests taken from? if from a RFC or elsewhere, could you add a remark in the file?
• the changes to mirage_crypto_ec.ml are substantial, could you please minimize the diff (i.e. changing the constructor of field_element, renaming b_uts to out_fe_to_fe, rename Foreign to Foreign_field etc. -- this can be done in a separate PR, but please keep these things separate)

As an alternative I can also migrate the NIST curves to ECCKiila code, which is about 10% faster and would make the code simpler and more unified.

Is this true across CPU architectures, or only on your Apple silicon? As you may have noticed, the other EC code is taken from projects with verification in mind, how much review and formal verification did ECCkiila get?

FWIW: I will also implement Brainpool curves. Please let me know, if you are interested in these as well.

Sure, in the end it all depends on code clarity and binary size (we dropped P224 for the binary size reason).

[ansiwen]

• what license is ECCkiila, is it fine to embed the code?

The license (MIT) is included in the generated file:

mirage-crypto/ec/native/secp256k1.h

Lines 1 to 24 in 1a4e3f2

	/* Autogenerated: ECCKiila https://gitlab.com/nisec/ecckiila */
	/*-
	* MIT License
	* -
	* Copyright (c) 2020 Luis Rivera-Zamarripa, Jesús-Javier Chi-Domínguez, Billy Bob Brumley
	* -
	* Permission is hereby granted, free of charge, to any person obtaining a copy
	* of this software and associated documentation files (the "Software"), to deal
	* in the Software without restriction, including without limitation the rights
	* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
	* copies of the Software, and to permit persons to whom the Software is
	* furnished to do so, subject to the following conditions:
	* -
	* The above copyright notice and this permission notice shall be included in all
	* copies or substantial portions of the Software.
	* -
	* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
	* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
	* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
	* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
	* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
	* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
	* SOFTWARE.
	*/

• could you follow the other curve implementations and have the code generated by fiat added to the ec/native/GNUmakefile, so we can at any point when fiat updates generate these C files?

The fiat code is automatically embedded in the file generated by ECCKiila. So, you want me to create the fiat files separately and remove them from the generated ECCKiila file? I sure can do that, just want to make sure we are on one page.

• where are the unit tests taken from? if from a RFC or elsewhere, could you add a remark in the file?

Unfortunately there doesn't seem to be any official or common test vectors for ECDSA signing and secp256k1, so I frankensteined them from some single test vectors I found at different places. (One of them is from Bouncy Castle IIRC)

• the changes to mirage_crypto_ec.ml are substantial, could you please minimize the diff (i.e. changing the constructor of field_element, renaming b_uts to out_fe_to_fe, rename Foreign to Foreign_field etc. -- this can be done in a separate PR, but please keep these things separate)

Ok, but some code I had to change in order to make it reusable. Or would you prefer code duplication and untouched old code?

As an alternative I can also migrate the NIST curves to ECCKiila code, which is about 10% faster and would make the code simpler and more unified.

Is this true across CPU architectures, or only on your Apple silicon?

I just tested it on x86_64, there it is also around 10%.

As you may have noticed, the other EC code is taken from projects with verification in mind, how much review and formal verification did ECCkiila get?

You mean other projects than fiat-crypto? They don't have any formal verification beyond fiat. From their paper:

It is important to note [Fiat] is the formal verification boundary for ECCKiila—all other code on top of Fiat, while computer generated through templating and automatic formula generation for ECC arithmetic, has no formal verification guarantees.

If the current EC arithmetic in mirage-crypto has stronger guarantees, that is of course an argument to keep the implementation, despite the slight performance difference.

I don't know how much review it received, I only know that the fiat project referred you to it, which can be interpreted as a slight endorsement.

Let me know what you prefer, and I will proceed accordingly.

[ansiwen]

I reduced the diff as much as possible without creating too much duplicate code, and split it up in two commits. The first is a pure restructuring without functional difference. The second is the addition of the new curve. Hope that helps to digest it.

I added makefile targets for the fiat code generator (took ages to compile it), and replaced the embedded ones in the ECCKiila generated ones with #includes of the generated fiat files. I had to add the --inline option to the fiat generator, otherwise it complained about unused functions. (File size didn't change.)

[ansiwen]

As you may have noticed, the other EC code is taken from projects with verification in mind, how much review and formal verification did ECCkiila get?

You mean other projects than fiat-crypto? They don't have any formal verification beyond fiat. From their paper:

It is important to note [Fiat] is the formal verification boundary for ECCKiila—all other code on top of Fiat, while computer generated through templating and automatic formula generation for ECC arithmetic, has no formal verification guarantees.

If the current EC arithmetic in mirage-crypto has stronger guarantees, that is of course an argument to keep the implementation, despite the slight performance difference.

I looked a bit more into the point add and double formulas ECCKiila is using for code generation. They are taken from this paper (which is also referenced in the comments of the generated code) that provides at least Magma code which provides "verification of the complete addition and exception-free doubling formulas". So there seems to be indeed some verification of the algorithm itself, and I guess if the tooling has no bugs, this is also true for the generated C code? Unfortunately I can't really tell how that compares to the guarantees of the implementations in point_operations.h.

[ansiwen]

FWIW: I did more comparisons of the ECCKiila implementation with the current implementation on x86_64 and arm64:

x86_64 (Intel Core i7, 2.6GHz)

	current	ECCKiila	%	ECCKiila u-sol	%
P256 DSA sign	5504	6023	109 %
P256 DSA verify	1004	1645	164 %
P256 DH share	1261	2344	186 %
P256 DH secret	7964	9156	115 %
P521 DSA sign	773	796	103 %	2519	326 %
P521 DSA verify	108	191	177 %	1010	935 %
P521 DH share	137	252	184 %	1751	1278 %
P521 DH secret	883	918	104 %	4302	487 %

arm64 (MacBook M3)

	current	ECCKiila	%	ECCKiila u-sol	%
P256 DSA sign	15718	17330	110 %
P256 DSA verify	2990	5335	178 %
P256 DH share	3834	7534	197 %
P256 DH secret	24241	28464	117 %
P521 DSA sign	2901	2926	101 %	4957	171 %
P521 DSA verify	429	754	176 %	1529	356 %
P521 DH share	542	1044	193 %	2243	414 %
P521 DH secret	2822	2835	100 %	4659	165 %

The "u-sol" column is a ECCKiila with unsaturated-solinas fiat code for field arithmetic. (scalar arithmetic is still montgomery, couldn't create unsaturated-solinas for the order of P-521, probably wouldn't be that efficient anyway.)

As you can see, there are some vast improvements for P-521, but the unsaturated-solinas could probably also be used independently of ECCKiila, I guess.

[hannesm]

Briefly coming back to your PR. Thanks a lot. I wonder what are the benefits to include it into mirage-crypto-ec? Would a separate opam package (secp256k1) contain a lot of code duplication? (and given the amount of updates to mirage-crypto-ec, would that be a bad idea to maintain?)

[ansiwen]

Briefly coming back to your PR. Thanks a lot. I wonder what are the benefits to include it into mirage-crypto-ec? Would a separate opam package (secp256k1) contain a lot of code duplication? (and given the amount of updates to mirage-crypto-ec, would that be a bad idea to maintain?)

Since the package also includes Ed/X25519, which is a completely separate implementation, and it is an EC, it was just natural for me to include it in the mirage-crypto-ec package. Even more so, because P256k1 uses the same ECDSA implementation as the NIST curves, so it is just an obvious extension. Also the Brainpool curves in the follow-up PR use that same ECDSA implementation and otherwise the same code as P256k1 in general. Of course we could reorganise the code, so that the implementations are more separate but use the same ECDSA module. But a separate package? I'm not sure, if that makes sense. I would ask back: what is the advantage of having a separate package? And if we would use ECCKiila code also for the NIST curves, it basically becomes all the same implementation again anyway.

In general I guess I have less issues with code duplication than the average developer. But in this specific case, where we would duplicate sensitive code like EC point arithmetic and transformations, I would rather swing to the reuseable-code side.

BTW: I also implemented the BIP-340 Schnorr signature, which - like Secp256k1 - is important for Bitcoin applications. If you are interested, please have a look at my fork, which is completely ECCKiila based. I'm happy to bring upstream whatever is of interest.

[hannesm]

what is the advantage of having a separate package?

Code size. Maintenance. Since OCaml doesn't have a way to avoid unused modules in a binary (see ocaml/ocaml#608), every user of mirage-crypto-ec would inhibit this code (+ brainpool curves) -- where apart from "crypto" (Bitcoin, other blockchains) I see not much usage (i.e. in security protocols - ssh, tls, ...).

Maintenance: if we merge this PR, suddenly someone needs to maintain the ~30_000 lines of code (plus another ~300_000 for the brainpool curves). Since some is generated, this may be simple (nevertheless, needs an eye on upstream to update the generated code when they change it [which may be due to security issues, performance, ...]) - but nevertheless it is something that needs to be done. I don't have that much time and energy to say "yes, of course, I want to maintain these curves". This is different for more widely used and useful curves (Ed448 comes to mind).

This is why I thought, maybe you want to create a separate opam package that you maintain, and contribute it to the opam-repository?

[ansiwen]

what is the advantage of having a separate package?

Code size. Maintenance. Since OCaml doesn't have a way to avoid unused modules in a binary (see ocaml/ocaml#608), every user of mirage-crypto-ec would inhibit this code (+ brainpool curves) -- where apart from "crypto" (Bitcoin, other blockchains) I see not much usage (i.e. in security protocols - ssh, tls, ...).

Binary size is indeed a good reason. I didn't think about that, because in our case we always need all of them, but of course for other users that should only be compiled and included if desired.

Maintenance: if we merge this PR, suddenly someone needs to maintain the ~30_000 lines of code (plus another ~300_000 for the brainpool curves). Since some is generated, this may be simple (nevertheless, needs an eye on upstream to update the generated code when they change it [which may be due to security issues, performance, ...]) - but nevertheless it is something that needs to be done. I don't have that much time and energy to say "yes, of course, I want to maintain these curves". This is different for more widely used and useful curves (Ed448 comes to mind).

That is understandable. We need these curves anyway and we plan to be more "up-to-date" with latest mirage versions, if it is feasible. So we can certainly probably cover the maintenance.

This is why I thought, maybe you want to create a separate opam package that you maintain, and contribute it to the opam-repository?

Ok, so to make sure I understand correctly: you are suggesting to use a separate repository for that, and not including these opam packages in the mirage-crypto repo?

Since I have no experience maintaining an opam package: how would you recommend to organise the code? Thinking out loud: Certainly a separate opam package for each group of curves (secp256k1, brainpool, ...) to avoid binary bloat, but I would like to depend on mirage-crypto then as much as possible. OTOH I will also be using ECCKiila for the other curves, so there is indeed not much overlap left then, if you prefer to stay with the current implementation. Mainly just the ECDSA implementation. So I guess it's not worth the hassle to make the Make_dsa available and I just copy everything?

[ansiwen]

I reorganized the code and created a bunch of new packages, which allow to selectively include only the curves that are required. See my branch here: https://github.com/Nitrokey/nethsm-mirage-crypto/tree/nethsm-crypto

Unfortunately, after all that work I realized, that we don't use Mirage_crypto_ec directly, but through the X509 package, which seems to be highly entangled with Mirage_crypto. To make X509 to support other curves from third party libraries as a kind of plugin looks like lot of work, and I even don't know if this would be something that upstream would be interested in. WDYT? Is that something the upstream projects would like to go? (I mean it is certainly useful, if Mirage_crypto and X509 would be more modular with per-curve-packages, but I don't really know how much work that would be.)

Otherwise at the moment it looks like a lot more feasible to me to just extend Mirage_crypto and X509, as a kind of "extended fork", which would be quite straight forward.