How does this compare to the verified TLS implementation from Project Everest?
1. The EverCrypt primitives are formally proven, whereas ring has no such formal proofs. Also it seems that all the EverCrypt primitives have portable (non-assembly) fallbacks, while ring has several primitives that are assembly only and have no portable fallback.
2. MiTLS is written in F#, which is harder to integrate with other languages than Rust.
We do use some of the Fiat Crypto stuff for elliptic curve computations. I am not opposed to switching some stuff to use EverCrypt or other things that might be better, as long as the performance is the same or better, and as long as there's a clear path towards that code being in Rust.
> ring has several primitives that are assembly only and have no portable fallback.
Either in the latest release (0.16.20) or the upcoming release, there is a portable non-assembly implementation of everything in ring.
Ring uses assembly to make sure it can do constant-time operations, to avoid leaking information through computation time. What does EverCrypt use for constant-time operations?
AFAIK Rust also doesn't guarantee timing. That's part of why Ring uses assembly for the constant-time bits (really Ring uses code from BoringSSL for that, and BoringSSL uses assembly for that reason and for performance.)
Personally, I would love to see enhancements to Rust and LLVM that would make it possible to provide such guarantees in pure Rust.
(This sort of thing is not my area of expertise, but has always made me uneasy...)
Especially note his guideline to look at the assembly output. The best guarantee is to simply check that the compiler did what you wanted.
There are also some aspects that a compiler is unlikely to alter. EG if you write code with no secret-dependent branches, no normal compiler will insert any secret-dependent branches during optimization. It's generally safe to rely on the compiler not being actively malicious or de-optimizing code.
The lack of a guarantee in assembly is less of a concern than the lack of a guarantee in C, since the CPU behavior is less likely to change unexpectedly than a C compiler.
Though Intel at least does provide a list of instruction latencies and throughputs, in their "Intel 64 and IA-32 Architectures Optimization Reference Manual"[1].
[1] https://www.intel.com/content/dam/www/public/us/en/documents...
So, you don't have to know how many cycles every instruction takes; you just have to make sure you use instructions that don't take a data-dependent number of cycles.
Expressing most algorithms this way is not impossible, but does nor feel natural for many.
It fundamentally isn't, because there is no way (in standard C) to prevent the compiler from introducing performance differences. Even if you avoid control flow constructions, what if the compiler e.g. generates a separate codepath for when one particular variable is 0 (perhaps as part of arithmetic optimizations)? There's just no (standard) way to stop that happening, no matter how cleverly you write your code.
Jokes aside, I wonder if some kind of -Ox option could be standardized to switch off all optimizations, like -O0, and also guarantee no code rewriting for whatever other purposes.
Hand-crafting constant-time algorithms in assembly is even more error-prone.
for the guaranteeing const execution time aspects. More or less any language compiled by LLVM, GCC or similar optimizing compilers can't do so. (And even wrt. assembly the cpus could do optimizations which also brake this but it's less likely).
Same is true for any language using a JIT with optimizations like e.g. Java, JavaScript, C#, etc.
Practically the degree of how much compilers could mess up const execution time guarantes is language dependent but for many languages especially including such using compilers created for C/C++ basically you have no useful guarantees.
At best you can create some code which just with the current version happen to not be optimized in a bad way. But this means you will have to review the produced assemply code and do it again and again every time the compiler (or just surrounding code) changes... To make it worse the high level code is force to use all kind of tricks to prevent the compiler from doing certain optimizations, which often obfuscate the intent of the code.
So all in all having a small very well reviewed set of assembly snippets for the core primitives the the easier to review and more reliable way in many cases. (Note that "a small set" means that just a few primitives are assembly only, not all the crypto, which normally is good enough).
Through best would be to have some language which focuses on both making it reasonable to implement such primitives in a more high level language and has tooling for proving code correctness and also code-to-assembly transformation correctness (e.g. see what SeL4 did wrt. proving assembly).
> The stable version of miTLS including the new 0.9 release are written in F#
With F# being a link to https://fsharp.org/