4 ms·

Really not the end. The existence of issues that cannot be addressed via 'langsec' does not imply that we should give up on 'langsec'. There will be more securi

Really not the end. The existence of issues that cannot be addressed via 'langsec' does not imply that we should give up on 'langsec'. There will be more security issues due to buffer overflows than there will be CPU bugs this year. More importantly, there will be orders of magnitudes more users with data compromised via buffer overflows, compared to CPU bugs.

deleted 9y ago
[deleted]
alxlaz 9y ago
The author does not seem to mean "the end of langsec" as in "everyone will give up on it", but rather the end of a period characterized, and not incorrectly, by the opinion that a safe programming language guarantees the absence of unintentional unsafe behaviour. In short, that things which, within this "langsec framework", one could prove to be impossible, turn out to be possible in practice; in the author's own words: "The basis of language security is starting from a programming language with a well-defined, easy-to-understand semantics. From there you can prove (formally or informally) interesting security properties about particular programs. [..] But the Spectre and Meltdown attacks have seriously set back this endeavor. One manifestation of the Spectre vulnerability is that code running in a process can now read the entirety of its address space, bypassing invariants of the language in which it is written, even if it is written in a "safe" language. [...] Mathematically, in terms of the semantics of e.g. JavaScript, these attacks should not be possible. But practically, they work. " This is not really news. The limits of formal methods were, in my opinion, well-understood, if often exaggerated by naysayers, brogrammers or simply programmers without much familiarity with them. Intuitively, it is not too difficult to grasp the idea that formal proofs are exactly as solid as the hardware which will run the program about which one is reasoning, and my impression is that it was well-grasped, if begrudgingly, by the community. (This is akin to the well-known mantra that no end-to-end encryption scheme is invulnerable to someone looking over your shoulder and noting what keys you type; similarly, no software-only process isolation scheme is impervious to the hardware looking over its shoulder and "writing down" bytes someplace where everyone can access them)
- UncleMeat 9y ago
  Wait. Who has ever said this? We've had soundiness as a fundamental concept for years. I'm not aware of a single static analysis tool that is truly sound. Everything is always "sound with respect to X". The academics surely haven't been the ones making a claim that correct programs truly are immune to any and all problems. If we ended this period, we did it ten years ago.
- allenz 9y ago
  > the end of a period characterized, and not incorrectly, by the opinion that a safe programming language guarantees... I don't think that there was ever such a period. Provable correctness always had the caveat of highly idealized assumptions, and we've known from the start that hardware vulnerabilities such as timing attacks, rowhammer, gamma rays, and power loss can undermine those assumptions.
- sideshowb 9y ago
  Well, how about a provably secure hardware description language then?
carussell 9y ago
It's funny that you mention buffer overflows. An interesting thing to point out—and I'm not sure if anyone has; I've looked before—is that if you follow Meredith Patterson's line of reasoning about langsec for protocols in particular, you end up at the conclusion that C-style, NUL-terminated strings are the right way to do things. This doesn't mean there aren't other defects in the apparatus where C exploits thrive. It's just that (if you adhere to the langsec school of thought) you are required to confront the conclusion that it's been pinned on the wrong thing.
- richardwhiuk 9y ago
  Why are C style buffers any more correct than Pascal strings?
  - noblethrasher 9y ago
    LangSec says that we should use the weakest model of computation that can get the job done. Patterson specifically recommends hewing to regular expressions as much as possible, but otherwise going no higher than deterministic context-free for ordinary programs. Null-terminated strings can be recognized by a regular expression, but once you introduce a length field, you (theoretically) need at least a context-sensitive grammar, which is excessively powerful (read: difficult to reason about) for ordinary programs, according to LangSec.
    - jerf 9y ago
      Where theory and reality diverge, I choose to believe reality. A theory that says null-terminated strings are more secure than length-delimited ones is a theory that needs to be taken back to the shop and examined for why it is wrong. I can imagine a much, much richer theory that might produce "in a perfect world that didn't have any other errors, null-terminated strings would be better". For instance, while this is far from the only problem with null-terminated strings, a lot of their badness historically came from the mistake of mixing stack string data with stack values that say where to return, or mixing the strings with places where you can also put executable code. In a world that had a different kind of stack, null-terminated strings would be less bad. But they would still be bad enough that length-delimited would still be better from a security point of view. And theories of security that are this sensitive to the mistakes around them aren't very useful in the real world, where mistakes will abound and useful security theories need to be able to degrade with some grace whenever possible.

deleted 9y ago

[deleted]

alxlaz 9y ago

The author does not seem to mean "the end of langsec" as in "everyone will give up on it", but rather the end of a period characterized, and not incorrectly, by the opinion that a safe programming language guarantees the absence of unintentional unsafe behaviour. In short, that things which, within this "langsec framework", one could prove to be impossible, turn out to be possible in practice; in the author's own words: "The basis of language security is starting from a programming language with a well-defined, easy-to-understand semantics. From there you can prove (formally or informally) interesting security properties about particular programs. [..] But the Spectre and Meltdown attacks have seriously set back this endeavor. One manifestation of the Spectre vulnerability is that code running in a process can now read the entirety of its address space, bypassing invariants of the language in which it is written, even if it is written in a "safe" language. [...] Mathematically, in terms of the semantics of e.g. JavaScript, these attacks should not be possible. But practically, they work. " This is not really news. The limits of formal methods were, in my opinion, well-understood, if often exaggerated by naysayers, brogrammers or simply programmers without much familiarity with them. Intuitively, it is not too difficult to grasp the idea that formal proofs are exactly as solid as the hardware which will run the program about which one is reasoning, and my impression is that it was well-grasped, if begrudgingly, by the community. (This is akin to the well-known mantra that no end-to-end encryption scheme is invulnerable to someone looking over your shoulder and noting what keys you type; similarly, no software-only process isolation scheme is impervious to the hardware looking over its shoulder and "writing down" bytes someplace where everyone can access them)

UncleMeat 9y ago
Wait. Who has ever said this? We've had soundiness as a fundamental concept for years. I'm not aware of a single static analysis tool that is truly sound. Everything is always "sound with respect to X". The academics surely haven't been the ones making a claim that correct programs truly are immune to any and all problems. If we ended this period, we did it ten years ago.
allenz 9y ago
> the end of a period characterized, and not incorrectly, by the opinion that a safe programming language guarantees... I don't think that there was ever such a period. Provable correctness always had the caveat of highly idealized assumptions, and we've known from the start that hardware vulnerabilities such as timing attacks, rowhammer, gamma rays, and power loss can undermine those assumptions.
sideshowb 9y ago
Well, how about a provably secure hardware description language then?

carussell 9y ago

It's funny that you mention buffer overflows. An interesting thing to point out—and I'm not sure if anyone has; I've looked before—is that if you follow Meredith Patterson's line of reasoning about langsec for protocols in particular, you end up at the conclusion that C-style, NUL-terminated strings are the right way to do things. This doesn't mean there aren't other defects in the apparatus where C exploits thrive. It's just that (if you adhere to the langsec school of thought) you are required to confront the conclusion that it's been pinned on the wrong thing.

richardwhiuk 9y ago
Why are C style buffers any more correct than Pascal strings?
- noblethrasher 9y ago
  LangSec says that we should use the weakest model of computation that can get the job done. Patterson specifically recommends hewing to regular expressions as much as possible, but otherwise going no higher than deterministic context-free for ordinary programs. Null-terminated strings can be recognized by a regular expression, but once you introduce a length field, you (theoretically) need at least a context-sensitive grammar, which is excessively powerful (read: difficult to reason about) for ordinary programs, according to LangSec.
  - jerf 9y ago
    Where theory and reality diverge, I choose to believe reality. A theory that says null-terminated strings are more secure than length-delimited ones is a theory that needs to be taken back to the shop and examined for why it is wrong. I can imagine a much, much richer theory that might produce "in a perfect world that didn't have any other errors, null-terminated strings would be better". For instance, while this is far from the only problem with null-terminated strings, a lot of their badness historically came from the mistake of mixing stack string data with stack values that say where to return, or mixing the strings with places where you can also put executable code. In a world that had a different kind of stack, null-terminated strings would be less bad. But they would still be bad enough that length-delimited would still be better from a security point of view. And theories of security that are this sensitive to the mistakes around them aren't very useful in the real world, where mistakes will abound and useful security theories need to be able to degrade with some grace whenever possible.