4 ms·

It's worrying that for some cases you have to put a lot of effort into "obscuring" code and destroy readability to comply with the rules just because the C's se

It's worrying that for some cases you have to put a lot of effort into "obscuring" code and destroy readability to comply with the rules just because the C's semantics is not obvious and its type system weak and dated. A good language for cryptography engineering should at least somehow allow the programmer to annotate/type variables containing secret data and functions as constant-time so that the programmer can concentrate on implementing the cryptography logic while the compiler warns on correctness issues or security violations.

nickpsecurity 7y ago
Yup: https://www.cryptol.net/ https://www.cryptol.net/ https://cseweb.ucsd.edu/~dstefan/pubs/cauligi:2017:fact.pdf https://cseweb.ucsd.edu/~dstefan/pubs/cauligi:2017:fact.pdf There's also program analysis work in this area: https://michael-emmi.github.io/papers/conf-uss-AlmeidaBBDE16.pdf https://michael-emmi.github.io/papers/conf-uss-AlmeidaBBDE16...
- ReidZB 7y ago
  I admit I've only ever taken cursory glances at Cryptol, but it's never seemed like a replacement for the sort of low-level programming described in the article. If anything, it goes the opposite way - its Haskell base inherits one of Haskell's flaws, namely that it can be difficult to understand the runtime/performance implications of Haskell code without careful analysis. Cryptol's README describes it as a sort of standardization/prototyping language. That said, I don't know these things for sure, and I'd love to be corrected if I'm wrong.
  - nickpsecurity 7y ago
    It's a higher-level language that generates or compiles to the lower-level forms, including C and hardware languages, so you don't have to worry about that stuff. The expert can specify the algorithm, mathematically verify it, synthesize it to code, another tool like Galois' SAW can verify that, and they usually do a certifying compiler (esp CompCert) at the end. Rockwell-Collins and Galois both use the tools in high-security projects. I can't remember if it addresses constant-time programming. So, I went looking arount, found the other language, and maybe someone will merge them.
    - ReidZB 7y ago
      Well, it doesn't matter if Cryptol is compiled down to "safe" machine code, like FaCT, right? But that's not something I've seen explicitly stated in the Cryptol docs, so I would not make that assumption myself. Are SAW or CompCert able to do formal verification around things like ensuring no branching on secrets, ensuring that memory is cleared after use, ...? Or does Cryptol make guarantees about the machine code it generates? I see that SAW is able to do things like prove that hand-written, optimized code is equivalent to the Cryptol specification, which is certainly very neat - but that does not preclude potential side-channel vulnerabilities in the hand-written, optimized variant. After all, much of the scariness of side-channel attacks is that they're explicitly not targeting the (highly analyzed) mathematics of a construction, but rather its implementation.
      - nickpsecurity 7y ago
        "Well, it doesn't matter if Cryptol is compiled down to "safe" machine code, like FaCT, right?" It does. It gets you the correct implementation of crypto. Most failures are implementation errors. From there, before the buzz about constant-time, high-assurance security was just mitigating that stuff by using fixed-size, fixed-timing transmission of messages. As in, they couldn't tell anything about the inside of the black box because all they saw was the same behavior on the outside. Designers sacrificed some performance and plenty of bandwidth to do that. Tightly-coupled designed with no covert channel analysis or mitigation later showed up that leaked all sorts of stuff with them changing coding styles instead of bad architecture. That's when we need stuff like OP article and FaCT. "Are SAW or CompCert able to do formal verification" (you) "I can't remember if it addresses constant-time programming. So, I went looking arount, found the other language, and maybe someone will merge them. " (me) I already answered that. I collected papers like FaCT specifically in case anyone wants to integrate them with Cryptol to address that gap if it exists. Also, other analysis and testing for information-flow security to make sure it is working on top of human review. This is a tiny part of my research given covert channel detection is mostly a solved problem with public, free methods such as Kemmerer's Shared Resource Matrix and Wray's for timing channels that most people just don't apply. Most of my research is on stuff that blocks code injection.
- bjoh 7y ago
  A follow-up to the FaCT paper can be found here: https://github.com/PLSysSec/FaCT/blob/master/FaCT_extended.pdf https://github.com/PLSysSec/FaCT/blob/master/FaCT_extended.p.... The source for the compiler is in the same repo. (Full disclosure: I’m a co-author.) There were a few interesting issues we ran into when implementing the compiler that we did not anticipate when writing the paper you linked (e.g., there are cases where making code constant-time can inadvertently introduce memory errors). You can try out the language here (based on Compiler Explorer): https://fact.sysnet.ucsd.edu/ https://fact.sysnet.ucsd.edu/
alltakendamned 7y ago
Cryptography is hard to implement correctly. What you consider to be obscure and destroying readability is not necessarily there because of semantics, but in order to avoid particular vulnerability categories, such as timing side channel attacks, due to using particular coding patterns or the compiler optimizing things in a certain way. The good language you talk about exists in crypto libraries that are meant to be used by us mere mortals. This document discusses some of the problems and solutions that are important if you are building those very same crypto libraries instead. On that note, veorq is an absolute authority in the field so I trust his writing on the matter.
floodyberry- 7y ago
A useful high language for cryptography would likely have to: * Not compile to C because you'd be left with the same doubts that the generated machine code is constant time * Not use gcc / clang internally to generate machine code for the same reason.. * ..but still optimize as well as either * ..while also implementing SIMD for all the useful platforms * ..and knowing which approach is most efficient for the target platform (SIMD vs scalar vs SIMD+scalar, instruction selection, instruction ordering, data alignment, etc) otherwise it's easier to just use C, or if you're a masochist, qhasm. There is also not a readability issue with constant time code as long as it's in properly named functions (which will get inlined away if necessary).

nickpsecurity 7y ago

Yup: https://www.cryptol.net/ https://www.cryptol.net/ https://cseweb.ucsd.edu/~dstefan/pubs/cauligi:2017:fact.pdf https://cseweb.ucsd.edu/~dstefan/pubs/cauligi:2017:fact.pdf There's also program analysis work in this area: https://michael-emmi.github.io/papers/conf-uss-AlmeidaBBDE16.pdf https://michael-emmi.github.io/papers/conf-uss-AlmeidaBBDE16...

ReidZB 7y ago
I admit I've only ever taken cursory glances at Cryptol, but it's never seemed like a replacement for the sort of low-level programming described in the article. If anything, it goes the opposite way - its Haskell base inherits one of Haskell's flaws, namely that it can be difficult to understand the runtime/performance implications of Haskell code without careful analysis. Cryptol's README describes it as a sort of standardization/prototyping language. That said, I don't know these things for sure, and I'd love to be corrected if I'm wrong.
- nickpsecurity 7y ago
  It's a higher-level language that generates or compiles to the lower-level forms, including C and hardware languages, so you don't have to worry about that stuff. The expert can specify the algorithm, mathematically verify it, synthesize it to code, another tool like Galois' SAW can verify that, and they usually do a certifying compiler (esp CompCert) at the end. Rockwell-Collins and Galois both use the tools in high-security projects. I can't remember if it addresses constant-time programming. So, I went looking arount, found the other language, and maybe someone will merge them.
  - ReidZB 7y ago
    Well, it doesn't matter if Cryptol is compiled down to "safe" machine code, like FaCT, right? But that's not something I've seen explicitly stated in the Cryptol docs, so I would not make that assumption myself. Are SAW or CompCert able to do formal verification around things like ensuring no branching on secrets, ensuring that memory is cleared after use, ...? Or does Cryptol make guarantees about the machine code it generates? I see that SAW is able to do things like prove that hand-written, optimized code is equivalent to the Cryptol specification, which is certainly very neat - but that does not preclude potential side-channel vulnerabilities in the hand-written, optimized variant. After all, much of the scariness of side-channel attacks is that they're explicitly not targeting the (highly analyzed) mathematics of a construction, but rather its implementation.
    - nickpsecurity 7y ago
      "Well, it doesn't matter if Cryptol is compiled down to "safe" machine code, like FaCT, right?" It does. It gets you the correct implementation of crypto. Most failures are implementation errors. From there, before the buzz about constant-time, high-assurance security was just mitigating that stuff by using fixed-size, fixed-timing transmission of messages. As in, they couldn't tell anything about the inside of the black box because all they saw was the same behavior on the outside. Designers sacrificed some performance and plenty of bandwidth to do that. Tightly-coupled designed with no covert channel analysis or mitigation later showed up that leaked all sorts of stuff with them changing coding styles instead of bad architecture. That's when we need stuff like OP article and FaCT. "Are SAW or CompCert able to do formal verification" (you) "I can't remember if it addresses constant-time programming. So, I went looking arount, found the other language, and maybe someone will merge them. " (me) I already answered that. I collected papers like FaCT specifically in case anyone wants to integrate them with Cryptol to address that gap if it exists. Also, other analysis and testing for information-flow security to make sure it is working on top of human review. This is a tiny part of my research given covert channel detection is mostly a solved problem with public, free methods such as Kemmerer's Shared Resource Matrix and Wray's for timing channels that most people just don't apply. Most of my research is on stuff that blocks code injection.
bjoh 7y ago
A follow-up to the FaCT paper can be found here: https://github.com/PLSysSec/FaCT/blob/master/FaCT_extended.pdf https://github.com/PLSysSec/FaCT/blob/master/FaCT_extended.p.... The source for the compiler is in the same repo. (Full disclosure: I’m a co-author.) There were a few interesting issues we ran into when implementing the compiler that we did not anticipate when writing the paper you linked (e.g., there are cases where making code constant-time can inadvertently introduce memory errors). You can try out the language here (based on Compiler Explorer): https://fact.sysnet.ucsd.edu/ https://fact.sysnet.ucsd.edu/

alltakendamned 7y ago

Cryptography is hard to implement correctly. What you consider to be obscure and destroying readability is not necessarily there because of semantics, but in order to avoid particular vulnerability categories, such as timing side channel attacks, due to using particular coding patterns or the compiler optimizing things in a certain way. The good language you talk about exists in crypto libraries that are meant to be used by us mere mortals. This document discusses some of the problems and solutions that are important if you are building those very same crypto libraries instead. On that note, veorq is an absolute authority in the field so I trust his writing on the matter.

floodyberry- 7y ago

A useful high language for cryptography would likely have to: * Not compile to C because you'd be left with the same doubts that the generated machine code is constant time * Not use gcc / clang internally to generate machine code for the same reason.. * ..but still optimize as well as either * ..while also implementing SIMD for all the useful platforms * ..and knowing which approach is most efficient for the target platform (SIMD vs scalar vs SIMD+scalar, instruction selection, instruction ordering, data alignment, etc) otherwise it's easier to just use C, or if you're a masochist, qhasm. There is also not a readability issue with constant time code as long as it's in properly named functions (which will get inlined away if necessary).