3 ms·

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 m

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.
hisham_hm 9y ago
That depends on what you mean by "getting the job done". If what you want is to write a reference description of a protocol for a paper, and make mathematical proofs of the protocol's properties, that's one thing. (The weakest model of computation there means you'll spend less proof effort around your surroundings -- language, environment -- and more on the protocol, giving you less leeway for error). If you want to write a real-world implementation of the protocol, then the story is different, because the complexities of the real world are unavoidable. You will add complexity to your toolset, to deal with the aspects of the environment that you abstracted away in your paper. When we write proofs for papers about type systems, we use ultra-simple languages like some typed variants of lambda calculus, which are the simplest thing that gets the job done. But once the type properties are proved, no one is expected to write their real programs that way -- they are expected to replicate those properties in the real world instead.

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.

hisham_hm 9y ago

That depends on what you mean by "getting the job done". If what you want is to write a reference description of a protocol for a paper, and make mathematical proofs of the protocol's properties, that's one thing. (The weakest model of computation there means you'll spend less proof effort around your surroundings -- language, environment -- and more on the protocol, giving you less leeway for error). If you want to write a real-world implementation of the protocol, then the story is different, because the complexities of the real world are unavoidable. You will add complexity to your toolset, to deal with the aspects of the environment that you abstracted away in your paper. When we write proofs for papers about type systems, we use ultra-simple languages like some typed variants of lambda calculus, which are the simplest thing that gets the job done. But once the type properties are proved, no one is expected to write their real programs that way -- they are expected to replicate those properties in the real world instead.