5 ms·

Are we finally approaching consensus in the field of systems programming that security is more important than performance (thanks to heartbleed)? Or put differ

by hoggle 12y ago

Are we finally approaching consensus in the field of systems programming that security is more important than performance (thanks to heartbleed)? Or put differently: have we reached the point where computers are fast enough so that we can move on and sacrifice some of those abundant MIPS and extra RAM for much improved clarity in our critical infrastructure code? OCaml could actually be a great choice for maintaining a solid TLS layer.

pdpi 12y ago
For the sake of moving things forward: every time we have this discussion, someone always points out that functional languages would make it easier to get correct behaviour from a crypto library, and someone always replies that garbage collection opens you up to side-channel (timing, in this case) attacks.
- lomnakkus 12y ago
  Isn't even C pretty vulnerable to timing attacks? (I'm thinking primarily through things like L1/L2 cache effects, etc.)
- hoggle 12y ago
  Interesting, I didn't know that. I always wondered why (non "functional") Ada doesn't get mentioned more often in these kinds of discussions: http://www.adaic.org/advantages/ http://www.adaic.org/advantages/ http://www.seas.gwu.edu/~mfeldman/ada-project-summary.html http://www.seas.gwu.edu/~mfeldman/ada-project-summary.html
  - pgeorgi 12y ago
    And it's "cousin" SPARK, which adds proof capabilities: http://git.codelabs.ch/?p=spark-crypto.git http://git.codelabs.ch/?p=spark-crypto.git
  - e12e 12y ago
    Last time it was brought up, there appeared to be some lingering confusion and issues with how the compiler and runtime was and is licensed. The latest version of Ada is available for a (large) fee from Adacore and for free under the GPL. There is also a version published as part of gcc, that trails the upstream version a little in terms of features -- but like the rest of gcc, the relevant parts are under LGPL, so not all binaries distributed to third parties need be distributed under the GPL, but can be under any licence one choose[1] -- without the need for a commercial licence from Adacore. It would appear the lack of an up-to-date, gratis, version of Ada was a real problem for adoption at some point -- and the impression of Ada being difficult to get access to outside of large contractors put a damper on its popularity (justified or not). [1] The "problem" with a compiler under GPL is that most compilers will have some kind of library code or language runtime that needs to be distributed with resulting binaries, thus forcing all projects to adopt GPL, rather than just the projects that build directly on the compiler.
    - pjmlp 12y ago
      More than price, what really hindered Ada was lack of adoption by popular OS vendors and hardware requirements for the early compilers. Back in the day everyone was paying for compilers, the prices were the normal ones for the target audience. Rational Software first product was an advanced Ada Machine, providing an early 80's InteliJ experience. Which followed the same fate as all special purpose computers. UNIX, mainframe and other enterprise OS vendors that eventually provided an Ada compiler, treated it as second class citizen in regard to their main systems programming language. Home computers lacked the required hardware to implement a proprer Ada compiler. A systems programming language really needs to be "the language" an OS vendor SDK requires, otherwise it becomes just another application language that can also go low level. Besides Ada Core, there are a few embedded and real time OS vendors providing Ada compilers.
      - e12e 12y ago
        > Home computers lacked the required hardware to implement a proprer Ada compiler. Could you elaborate? Are you thinking 80s home computers like the Amiga 1000, or more classical PCs?
- edwintorok 12y ago
  The actual crypto primitives are still implemented in C, do those timing attack apply to the high-level part implemented in OCaml too?
  - pqwy 12y ago
    That is exactly the question we have. And yes, the primitives are in C largely due to timing concerns.
- chriswarbo 12y ago
  Interesting. Maybe an area where linear types can shine? Rust is probably the most trendy language offering linear types at the moment, although I'd say it much closer to being "a safer C" than "a linear OCaml", so it wouldn't really make things more functional (although it would be safer!). ATS is descended from DependentML, but for some reason most ATS code I've seen is written in a "safer C" style too. Maybe that's just pragmatism, since ATS has very few native libraries, so it's usually easier to call out to C. Linear Lisp might be a nice choice, but its dynamic typing may be a problem for security-critical code.
  - steveklabnik 12y ago
    Fun bit of trivia: Rust was originally implemented _in_ OCaml, and takes a lot of cues from it.
    - klibertp 12y ago
      I saw a bit of OCaml code in Rust code-base recently, can you say what it's used for? I know that Rust is self-hosting now, but I swear I saw some .ml files there...
      - dbaupp 12y ago
        ~/rust $ find -name '*.ml' | wc -l 72 ~/rust $ find -name '*.ml' | grep -v ./src/llvm | wc -l 0 i.e. there are some OCaml files in a Rust checkout, but they're all part of LLVM, mostly part of the "OCaml Kaleidoscope": http://llvm.org/docs/tutorial/OCamlLangImpl1.html http://llvm.org/docs/tutorial/OCamlLangImpl1.html
- colanderman 12y ago
  I know nothing about crypto, but I know a bit about languages. I don't really get this. Say you're coding in a language with no garbage collection like C. If your code is not "symmetric" (more below), you still have timing attacks due to cache usage patterns, correct? After all, C hasn't been a very good model of any CPU designed since 1985. Coming from the outside, I would think the way to tackle this would be to simple ensure your code is "symmetric"; that every legal code path through an algorithm perform the same operations, regardless of what data it is presented with, even if this means operating on fake data. That way the timing of any operation is always identical (barring uncorrelated noise). It seems to me that this technique would apply equally to languages with and without garbage collection. Why is this not so?
duaneb 12y ago
> OCaml could actually be a great choice for maintaining a solid TLS layer. Maybe; it uses GC and it's difficult to embed. I would much prefer something that compiles without a runtime (or with a minimal one for resource allocation).
- avsm 12y ago
  The OCaml runtime is very easy to embed, as runtimes go. We've got it compiling in Mirage as a standalone kernel, as a FreeBSD kernel module, and others have had it running on 8-bit PIC microcontrollers: http://www.algo-prog.info/ocaml_for_pic/web/index.php?id=ocapic http://www.algo-prog.info/ocaml_for_pic/web/index.php?id=oca... A fun project that I discussed with the Rust devs at last year's OSCON would be to rewrite the OCaml GC in Rust. Get in touch with me if you're interested and want some guidance on how to go about this.
  - duaneb 12y ago
    Consider me interested.
pjmlp 12y ago
I hope so. We already had safer systems programming languages around the time UNIX spread outside AT&T. There is a quote from Hoare how engineers asked him to not allow to disable bounds checking in Algol, for example[0]. Also the rise in security exploits has helped Ada/SPARK to move outside their original niche into areas where human lifes are at risk, like medical equipments and train control systems. At least from the FOSDEM talks. I am looking forward to the days when we can recover the systems programming security C took away. [0] later compiler versions allowed it.

by hoggle 12y ago

pdpi 12y ago

For the sake of moving things forward: every time we have this discussion, someone always points out that functional languages would make it easier to get correct behaviour from a crypto library, and someone always replies that garbage collection opens you up to side-channel (timing, in this case) attacks.

lomnakkus 12y ago
Isn't even C pretty vulnerable to timing attacks? (I'm thinking primarily through things like L1/L2 cache effects, etc.)
hoggle 12y ago
Interesting, I didn't know that. I always wondered why (non "functional") Ada doesn't get mentioned more often in these kinds of discussions: http://www.adaic.org/advantages/ http://www.adaic.org/advantages/ http://www.seas.gwu.edu/~mfeldman/ada-project-summary.html http://www.seas.gwu.edu/~mfeldman/ada-project-summary.html
- pgeorgi 12y ago
  And it's "cousin" SPARK, which adds proof capabilities: http://git.codelabs.ch/?p=spark-crypto.git http://git.codelabs.ch/?p=spark-crypto.git
- e12e 12y ago
  Last time it was brought up, there appeared to be some lingering confusion and issues with how the compiler and runtime was and is licensed. The latest version of Ada is available for a (large) fee from Adacore and for free under the GPL. There is also a version published as part of gcc, that trails the upstream version a little in terms of features -- but like the rest of gcc, the relevant parts are under LGPL, so not all binaries distributed to third parties need be distributed under the GPL, but can be under any licence one choose[1] -- without the need for a commercial licence from Adacore. It would appear the lack of an up-to-date, gratis, version of Ada was a real problem for adoption at some point -- and the impression of Ada being difficult to get access to outside of large contractors put a damper on its popularity (justified or not). [1] The "problem" with a compiler under GPL is that most compilers will have some kind of library code or language runtime that needs to be distributed with resulting binaries, thus forcing all projects to adopt GPL, rather than just the projects that build directly on the compiler.
  - pjmlp 12y ago
    More than price, what really hindered Ada was lack of adoption by popular OS vendors and hardware requirements for the early compilers. Back in the day everyone was paying for compilers, the prices were the normal ones for the target audience. Rational Software first product was an advanced Ada Machine, providing an early 80's InteliJ experience. Which followed the same fate as all special purpose computers. UNIX, mainframe and other enterprise OS vendors that eventually provided an Ada compiler, treated it as second class citizen in regard to their main systems programming language. Home computers lacked the required hardware to implement a proprer Ada compiler. A systems programming language really needs to be "the language" an OS vendor SDK requires, otherwise it becomes just another application language that can also go low level. Besides Ada Core, there are a few embedded and real time OS vendors providing Ada compilers.
    - e12e 12y ago
      > Home computers lacked the required hardware to implement a proprer Ada compiler. Could you elaborate? Are you thinking 80s home computers like the Amiga 1000, or more classical PCs?
edwintorok 12y ago
The actual crypto primitives are still implemented in C, do those timing attack apply to the high-level part implemented in OCaml too?
- pqwy 12y ago
  That is exactly the question we have. And yes, the primitives are in C largely due to timing concerns.
chriswarbo 12y ago
Interesting. Maybe an area where linear types can shine? Rust is probably the most trendy language offering linear types at the moment, although I'd say it much closer to being "a safer C" than "a linear OCaml", so it wouldn't really make things more functional (although it would be safer!). ATS is descended from DependentML, but for some reason most ATS code I've seen is written in a "safer C" style too. Maybe that's just pragmatism, since ATS has very few native libraries, so it's usually easier to call out to C. Linear Lisp might be a nice choice, but its dynamic typing may be a problem for security-critical code.
- steveklabnik 12y ago
  Fun bit of trivia: Rust was originally implemented _in_ OCaml, and takes a lot of cues from it.
  - klibertp 12y ago
    I saw a bit of OCaml code in Rust code-base recently, can you say what it's used for? I know that Rust is self-hosting now, but I swear I saw some .ml files there...
    - dbaupp 12y ago
      ~/rust $ find -name '*.ml' | wc -l 72 ~/rust $ find -name '*.ml' | grep -v ./src/llvm | wc -l 0 i.e. there are some OCaml files in a Rust checkout, but they're all part of LLVM, mostly part of the "OCaml Kaleidoscope": http://llvm.org/docs/tutorial/OCamlLangImpl1.html http://llvm.org/docs/tutorial/OCamlLangImpl1.html
colanderman 12y ago
I know nothing about crypto, but I know a bit about languages. I don't really get this. Say you're coding in a language with no garbage collection like C. If your code is not "symmetric" (more below), you still have timing attacks due to cache usage patterns, correct? After all, C hasn't been a very good model of any CPU designed since 1985. Coming from the outside, I would think the way to tackle this would be to simple ensure your code is "symmetric"; that every legal code path through an algorithm perform the same operations, regardless of what data it is presented with, even if this means operating on fake data. That way the timing of any operation is always identical (barring uncorrelated noise). It seems to me that this technique would apply equally to languages with and without garbage collection. Why is this not so?

duaneb 12y ago

> OCaml could actually be a great choice for maintaining a solid TLS layer. Maybe; it uses GC and it's difficult to embed. I would much prefer something that compiles without a runtime (or with a minimal one for resource allocation).

avsm 12y ago
The OCaml runtime is very easy to embed, as runtimes go. We've got it compiling in Mirage as a standalone kernel, as a FreeBSD kernel module, and others have had it running on 8-bit PIC microcontrollers: http://www.algo-prog.info/ocaml_for_pic/web/index.php?id=ocapic http://www.algo-prog.info/ocaml_for_pic/web/index.php?id=oca... A fun project that I discussed with the Rust devs at last year's OSCON would be to rewrite the OCaml GC in Rust. Get in touch with me if you're interested and want some guidance on how to go about this.
- duaneb 12y ago
  Consider me interested.

pjmlp 12y ago

I hope so. We already had safer systems programming languages around the time UNIX spread outside AT&T. There is a quote from Hoare how engineers asked him to not allow to disable bounds checking in Algol, for example[0]. Also the rise in security exploits has helped Ada/SPARK to move outside their original niche into areas where human lifes are at risk, like medical equipments and train control systems. At least from the FOSDEM talks. I am looking forward to the days when we can recover the systems programming security C took away. [0] later compiler versions allowed it.