4 ms·

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

by spoiler 13y ago

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/

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

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

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/