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.
"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.
You can only prove it secure against known side-channel attacks. In a language with a good type system you would probably use types that support only constant-time operations.
Protecting against everything including side-channel attacks that are unknown at the time of implementation will likely never be possible, regardless of language. Thus for language choice this is a non-issue. Still: if you can avoid the stupid bug-holes and just leave the exotic side-channels that would be a big win.
> 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?
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.
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.