Ideas for a New Elliptic Curve Library

It's a lot easier to produce properties like constant-time execution by construction than to have to shoehorn things into them after the fact.

One project that tries to do something like this is Nadeko: https://www.reddit.com/r/rust/comments/3696wt/checking_that_...

The idea is that the DSL compiler would be responsible for ensuring constant-timeness. Note that C, C++, and Rust offer no guarantee of constant-timeness. Even processors don't offer constant-timeness guarantees and some instructions (often division) are not constant-time. See also http://blog.erratasec.com/2015/03/x86-is-high-level-language....

I wrote the paper mostly in the context of implementing signature verification, which doesn't require side-channel protection since there are no secrets in verification. But, I think the DSL approach is even more important for ECDH and signing, where side-channel protection is important.

Finally, given that processors don't even promise us that any instruction is constant-time, and given that other types of attacks are possible where constant-timesness doesn't help so much (e.g. power analysis), I think it is worth considering other approaches to side-channel protection (e.g. blinding). For many applications, constant-timeness isn't sufficient and I'd love to learn that it isn't necessary.

I see I didn't do a good job of explaining why that doesn't work so well. See, papers on high-performance elliptic curve cryptography tend to give formulas for implementing calculations using the three-operand style I mentioned. One reason for having a DSL is to make it so that we can copy/paste, with minimal changes, those formulas into our programs so that we can easily see that we're implementing the formula from the paper exactly. If you C++-ify or Rust-ify them, then you lose that obvious "this is the same" comparison ability. Also, for the kinds of code where such a DSL would be relevant, you really don't want a C++ or Rust compiler's optimizer to be involved at all. And, if you want to prove the correctness of your ECC code, you don't really want to have to first (1) Define a formal semantics for C++ or Rust, (2) Prove that your C++ or Rust compiler is correct with respect to that formal semantics, and (3) Prove that your transliterations of the original formulas are equivalent to the original formulas.

I've already written a prototype that compiles that DSL into C, which requires a leap of faith that the C compiler won't ruin things for us. That prototype convinced me that it would likely be much less work to go the DSL route than the C++/Rust library route. Note that I prefer writing C++ and Rust libraries to creating DSLs, so this was a disappointing conclusion for me.

Well, best response I've seen to a post like this. The audience you refer to might be best served with a SPARK, Frama-C, etc. implementation decomposed as much as possible with experts doing the DbC annotations or VCC's.

More likely an informal method. In the distant past, my method was to use a language with compile-time macro's to decompose the overall algorithm into simplest functions. In dev mode, I could manually run checks to hopefully ensure my assumptions were correct. Each module was simple enough to extensively test and spot coding defects. If necessary, I could do it at ASM level while wrapping low-level stuff in HLL calls w/ checks. In production mode, it compiled to straight-forward, high-performance, low-level code.

So, two routes with different levels of formality and optimization. The 2nd method is more likely to get adopted. Just not sure how many weird corner cases can be prevented that way.