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.