Crap, now I have to update my manual¹, and advise the paranoid to verify the signature they just generated. Perhaps even provide a helper function for it?
(I still think letting the user control `r` is too dangerous.)
(I still think letting the user control `r` is too dangerous.)
Monocypher can "only" produce 7000 signatures per seconds on a single thread on my laptop (i5 Skylake Intel). With the verification, I would waste a whooping 0.3ms on each signature, reducing the throughput to 2000 signatures per seconds.
Unless you're running a signing intensive application on the scale of Let's Encrypt, you won't really care about the slow-down. If you don't fully trust your hardware however, faults might be a real problem.
2. If you can induce faults on Lets Encrypt's signing infrastructure you have better attacks to deploy.
3. Lets Encrypt doesn't use Elliptic Curve in the first place.
If the algorithm is immune to faults, the worst thing that can happen is that you produce an invalid signature, which will then be rejected. This turns the security concern into a more mundane performance concern.
The truly paranoid would never believe any algorithm is immune to faults.
Even if full mathematical code analysis shows it to be so, can you prove that the proving analysis algorithm itself is immune to faults? It is potentially faulty turtles all the way down!
The proof checker can be ran several times to account for faults. Then you don't need to run it at all (it's proven). And you can use another proof checker (or that proof checker itself) to prove that the proof checker works. Etc.
Now there's the problem of the compiler, which gives a upper bound on the confidence you can have: if there's a bug in it, you're screwed even with a correct algorithm.
> Even if full mathematical code analysis shows it to be so
Come to think of it, that may not be possible for lots and lots of algorithms —whose mathematical security is only conjectured to begin with. Thanks for pointing that out.
This is what SEL4 people are doing.
The remaining part is verifying if your machine model is correct. Not trivial for some CPU and memory controller as complex as x86. (Even though just a subset of operations are used.)
Doing this also allows you a proof against fault attacks and timing attacks.
A better question would be whether, in a theoretical sense, fault-free algorithms even exist. There are similar questions, like whether one-way functions exist, where we have lots of evidence to suggest that the answer is "yes" but we have yet to prove it.
But you can prove many things. Many programs we care about can be proven correct (for whatever definition of "correct" we manage to formally specify), and those we can't prove correct can probably be transformed into provable versions —assuming they're short enough.