> The EverCrypt primitives are formally proven, whereas ring has no such formal proofs.

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.

Thanks for the correction!

> 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.

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?

This is an important point. The C standard does not define the time it takes for an operation to complete as "observable behavior", so compilers are *always* free to change timings, even with optimization disabled. It is fundamentally impossible to guarantee constant-time execution in Standard portable C. It's possible to use non-standard intrinsics and compiler directives to get such a guarantee, but that's not portable.

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.)

Rust doesn't guarantee timing, but there are crates that carefully construct constant-time primitives that should work with current Rust, such as https://crates.io/crates/subtle-ng .

Personally, I would love to see enhancements to Rust and LLVM that would make it possible to provide such guarantees in pure Rust.

Word on the block is that there is a RFC to add support for secret types in LLVM, and Rust is waiting for them to also provide it in Rust [0].

[0]: https://github.com/rust-lang/rfcs/pull/2859

It doesn't seem to stop people from trying though: https://www.bearssl.org/constanttime.html

(This sort of thing is not my area of expertise, but has always made me uneasy...)

Yeah. That sort of thing works, right up until some compiler gets released that optimizes it out. It's "portable C", but the behavior it's trying to produce is non-portable.

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.

I don't think Intel/AMD make any guarantees about instructions being constant time either.

Correct, and don't provide any guarantees about electromagnetic side channel emissions or power side channels or…

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...

Normally, rather than counting on two different codepaths to take the same number of cycles, assembly code written for constant execution time will always run all the same instructions unconditionally.

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.

This is only possible with resource aware types, it would be nice to import a function with resource constraints such as constant time, etc.

> It should be possible to create constant-time C code, if the code avoids branching (if, case, goto), and all loops have a constant number of operations.

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.

Sad! It's as if we might need some kind of simple portable assembly, one which straightforwardly translates simple constructs and formulas to the target machine code. Like, well, C used to be in 1975.

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.

In fairness assembly isn't what it was in 1975 either - with superscalar architectures and the dominance of caches these days even assembly is not as constant-time as you might expect.

And assembly makes the code harder to audit: https://cryptologie.net/article/520/cryptography-and-assembl...

But assembly is unavoidable.

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).

You might be interested in https://www.microsoft.com/en-us/research/publication/coq-wor... if you've not seen it already.

MiTLS is written in FStar, not F#. FStar has some tools (like Kremlin [1]) for extracting C code from the verified FStar, so in theory it wouldn’t be too hard to also extract Rust code too.

[1] https://github.com/FStarLang/kremlin

Straight from https://mitls.org/

> The stable version of miTLS including the new 0.9 release are written in F#

With F# being a link to https://fsharp.org/

The original code was written in F#, then re-written later in F7 then F* (FStar).

Doesn't .net have pretty good C FFI support, what would make it harder than a Rust lib?