7 ms·

In the age where "most" web-servers are idling at 10% load and yaaaawning most of the hours away, it makes no sense that security-critical network-code should b

In the age where "most" web-servers are idling at 10% load and yaaaawning most of the hours away, it makes no sense that security-critical network-code should be written in unsafe languages which can leak memory, such as C. Due to improved hardware, we've now reached the point where we can have reasonable security and performance at the same time. We no longer need to sacrifice security by using unsafe languages. So why are we using them? Yes some companies like Google and Facebook has busy servers, but for the rest of us, for the rest of the entire internet having to redo all our keys and certs and passwords due to a archetypical C-style bug in OpenSSL, the cost using C compared to the potential performance-benefits is absolutely not worth it. Not even close. TLDR: Stop writing network-code in C unless you bloody well need to

spoiler 13y ago
With just a little bit of brain power and abstraction C can be made "safe" (assuming you don't cock up the API).
- alkonaut 13y ago
  Certainly. But abstract it enough and the abstractions and syntax extensions required become another language. Abstract it to the point where you don't have any pointer arithmetic, a good type checker and so on, and the C code has turned into something else. Just adding wrappers around buffers to prevent overflows etc. doesn't come near the type of safety you can get in languages where you can prove formally what is going to happen when the program executes. Before you have the kind of security you can reason about like http://www.mitls.org http://www.mitls.org (rather than just abstractions for buffers etc.) it can't look like C any more.
  - jude- 13y ago
    While miTLS is a step in the right direction (as are proofs of logical correctness as a general development strategy), one must keep in mind that miTLS in particular is implemented in F#, meaning that runs on top of the CLI. The CLI is written in an "unsafe" language and is not formally verified for correctness, but to use miTLS you must trust the CLI fully. I'm not saying that the CLI is inherently insecure. I'm just saying that you can't ignore the security implications of the layers beneath your TLS implementation.
    - alkonaut 13y ago
      I see what you are saying, any language that has a runtime has its security dependent on that runtime. F# can compile and run on a variety of platforms (not sure which mitls are compatible with) not necessarily the ms CLI only. Normally I'd argue that running safe programs on top of a runtime/VM would make everything safer since you would only have to prove ONE system (the VM) to be safe, but with the Java debacle of recent years I think that argument isn't really as good as it used to be. I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal. Not sure how difficult this is for good "safe" languages such as e.g. Haskell.
      - Dewie 13y ago
        > I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal. Not sure how difficult this is for good "safe" languages such as e.g. Haskell. I wonder if optimizations affect the area of code that would need to be verified? Haskell is pure, and this fact is exploited in a lot optimizations and code generation - I guess one would have to prove that all of these transformations preserve the integrity of the Haskell semantics. I guess you could have a small (compared to GHC) implementation of Haskell which is formally verified, which is small because you don't bother with hardly any optimizations?
        jude- 13y ago
        Side-channel attacks are my primary concern with writing secure code. For example, if Haskell optimizes and makes some decryption functions run faster than others for an attacker-chosen ciphertext, the attacker could use the runtime differences perform a timing attack [1], and potentially learn your secrets. [1] https://en.wikipedia.org/wiki/Timing_attack https://en.wikipedia.org/wiki/Timing_attack
      - jude- 13y ago
        "I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal." Proving all layers logically correct would be a great start :) We could probably have avoided this whole Heartbleed debacle. If you'll allow me to elaborate on the security properties, it's worth pointing out that even if your TLS implementation ran on top of a formally-proven correct VM and used formally-proven correct libraries, and ran on a formally-proven correct kernel and processor, you still have to prove that it resists side-channel attacks before it can be said to be secure. Doing so is open-ended, and likely impossible, since side-channel attacks come in all shapes and sizes, and some are outside the scope of software engineering. For example, how do we prove that a logically-correct TLS implementation is secure against acoustic analysis? [1] How would we have done this before it was known that acoustic analysis was possible? This is the essence of what makes writing secure code hard. [1] https://www.cs.tau.ac.il/~tromer/acoustic/ https://www.cs.tau.ac.il/~tromer/acoustic/
hackerboos 13y ago
I think the point of TFA is that we can write this code and it will run as efficiently as C in a language which is safer than C.
- pjmlp 13y ago
  It was already possible in the 70's with PL/I, Mesa and Modula-2, but alas they though it would be better not to offer bounds checking in the language, instead of a way to disable them if required, like the other languages.
ris 13y ago
Is electrical power free for you, then?

spoiler 13y ago

With just a little bit of brain power and abstraction C can be made "safe" (assuming you don't cock up the API).

alkonaut 13y ago
Certainly. But abstract it enough and the abstractions and syntax extensions required become another language. Abstract it to the point where you don't have any pointer arithmetic, a good type checker and so on, and the C code has turned into something else. Just adding wrappers around buffers to prevent overflows etc. doesn't come near the type of safety you can get in languages where you can prove formally what is going to happen when the program executes. Before you have the kind of security you can reason about like http://www.mitls.org http://www.mitls.org (rather than just abstractions for buffers etc.) it can't look like C any more.
- jude- 13y ago
  While miTLS is a step in the right direction (as are proofs of logical correctness as a general development strategy), one must keep in mind that miTLS in particular is implemented in F#, meaning that runs on top of the CLI. The CLI is written in an "unsafe" language and is not formally verified for correctness, but to use miTLS you must trust the CLI fully. I'm not saying that the CLI is inherently insecure. I'm just saying that you can't ignore the security implications of the layers beneath your TLS implementation.
  - alkonaut 13y ago
    I see what you are saying, any language that has a runtime has its security dependent on that runtime. F# can compile and run on a variety of platforms (not sure which mitls are compatible with) not necessarily the ms CLI only. Normally I'd argue that running safe programs on top of a runtime/VM would make everything safer since you would only have to prove ONE system (the VM) to be safe, but with the Java debacle of recent years I think that argument isn't really as good as it used to be. I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal. Not sure how difficult this is for good "safe" languages such as e.g. Haskell.
    - Dewie 13y ago
      > I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal. Not sure how difficult this is for good "safe" languages such as e.g. Haskell. I wonder if optimizations affect the area of code that would need to be verified? Haskell is pure, and this fact is exploited in a lot optimizations and code generation - I guess one would have to prove that all of these transformations preserve the integrity of the Haskell semantics. I guess you could have a small (compared to GHC) implementation of Haskell which is formally verified, which is small because you don't bother with hardly any optimizations?
      - jude- 13y ago
        Side-channel attacks are my primary concern with writing secure code. For example, if Haskell optimizes and makes some decryption functions run faster than others for an attacker-chosen ciphertext, the attacker could use the runtime differences perform a timing attack [1], and potentially learn your secrets. [1] https://en.wikipedia.org/wiki/Timing_attack https://en.wikipedia.org/wiki/Timing_attack
    - jude- 13y ago
      "I agree with what you are saying: for proven security you need to prove properties of all the layers down to the metal." Proving all layers logically correct would be a great start :) We could probably have avoided this whole Heartbleed debacle. If you'll allow me to elaborate on the security properties, it's worth pointing out that even if your TLS implementation ran on top of a formally-proven correct VM and used formally-proven correct libraries, and ran on a formally-proven correct kernel and processor, you still have to prove that it resists side-channel attacks before it can be said to be secure. Doing so is open-ended, and likely impossible, since side-channel attacks come in all shapes and sizes, and some are outside the scope of software engineering. For example, how do we prove that a logically-correct TLS implementation is secure against acoustic analysis? [1] How would we have done this before it was known that acoustic analysis was possible? This is the essence of what makes writing secure code hard. [1] https://www.cs.tau.ac.il/~tromer/acoustic/ https://www.cs.tau.ac.il/~tromer/acoustic/

hackerboos 13y ago

I think the point of TFA is that we can write this code and it will run as efficiently as C in a language which is safer than C.

pjmlp 13y ago
It was already possible in the 70's with PL/I, Mesa and Modula-2, but alas they though it would be better not to offer bounds checking in the language, instead of a way to disable them if required, like the other languages.

ris 13y ago

Is electrical power free for you, then?