5 ms·

How does this compare to the verified TLS implementation from Project Everest? https://project-everest.github.io/ https://project-everest.github.io/ https://m

How does this compare to the verified TLS implementation from Project Everest? https://project-everest.github.io/ https://project-everest.github.io/ https://mitls.org/ https://mitls.org/

CameronNemo 6y ago
From a layman's perspective: 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.
- JoshTriplett 6y ago
  > 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?
  - SAI_Peregrinus 6y ago
    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.)
    - steveklabnik 6y ago
      It doesn't seem to stop people from trying though: https://www.bearssl.org/constanttime.html https://www.bearssl.org/constanttime.html (This sort of thing is not my area of expertise, but has always made me uneasy...)
      - SAI_Peregrinus 6y ago
        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.
    - CodesInChaos 6y ago
      I don't think Intel/AMD make any guarantees about instructions being constant time either.
      - SAI_Peregrinus 6y ago
        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/manuals/64-ia-32-architectures-optimization-manual.pdf https://www.intel.com/content/dam/www/public/us/en/documents...
        JoshTriplett 6y ago
        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.
  - baby 6y ago
    And assembly makes the code harder to audit: https://cryptologie.net/article/520/cryptography-and-assembly-code/ https://cryptologie.net/article/520/cryptography-and-assembl...
    - dathinab 6y ago
      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).
      - lmm 6y ago
        You might be interested in https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/ https://www.microsoft.com/en-us/research/publication/coq-wor... if you've not seen it already.
- briansmith 6y ago
  > 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.
  - CameronNemo 6y ago
    Thanks for the correction!
- fulafel 6y ago
  Doesn't .net have pretty good C FFI support, what would make it harder than a Rust lib?
- deleted 6y ago
  [deleted]
- profquail 6y ago
  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 https://github.com/FStarLang/kremlin
  - lights0123 6y ago
    Straight from https://mitls.org/ 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/ https://fsharp.org/
    - profquail 6y ago
      The original code was written in F#, then re-written later in F7 then F* (FStar).

How does this compare to the verified TLS implementation from Project Everest? https://project-everest.github.io/ https://project-everest.github.io/ https://mitls.org/ https://mitls.org/

CameronNemo 6y ago

From a layman's perspective: 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.

JoshTriplett 6y ago
> 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?
- SAI_Peregrinus 6y ago
  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.)
  - steveklabnik 6y ago
    It doesn't seem to stop people from trying though: https://www.bearssl.org/constanttime.html https://www.bearssl.org/constanttime.html (This sort of thing is not my area of expertise, but has always made me uneasy...)
    - SAI_Peregrinus 6y ago
      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.
  - CodesInChaos 6y ago
    I don't think Intel/AMD make any guarantees about instructions being constant time either.
    - SAI_Peregrinus 6y ago
      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/manuals/64-ia-32-architectures-optimization-manual.pdf https://www.intel.com/content/dam/www/public/us/en/documents...
      - JoshTriplett 6y ago
        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.
- baby 6y ago
  And assembly makes the code harder to audit: https://cryptologie.net/article/520/cryptography-and-assembly-code/ https://cryptologie.net/article/520/cryptography-and-assembl...
  - dathinab 6y ago
    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).
    - lmm 6y ago
      You might be interested in https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/ https://www.microsoft.com/en-us/research/publication/coq-wor... if you've not seen it already.
briansmith 6y ago
> 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.
- CameronNemo 6y ago
  Thanks for the correction!
fulafel 6y ago
Doesn't .net have pretty good C FFI support, what would make it harder than a Rust lib?
deleted 6y ago
[deleted]
profquail 6y ago
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 https://github.com/FStarLang/kremlin
- lights0123 6y ago
  Straight from https://mitls.org/ 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/ https://fsharp.org/
  - profquail 6y ago
    The original code was written in F#, then re-written later in F7 then F* (FStar).