3 ms·

There's a funny excluded middle here: On one side, small high-risk systems should be verified, so LangSec approaches seem archaic and lightweight. We should be

There's a funny excluded middle here: On one side, small high-risk systems should be verified, so LangSec approaches seem archaic and lightweight. We should be advocating higher-assurance testing & verification approaches like model checking, symbolic execution, and proof systems. On the other side, we see big systems that matter in the aggregate. That means stuff that scales: containerization, DLP + DLP honeypots, anomaly detection, and maybe eventually, information flow security. That leaves LangSec in a funny place.

alricb 11y ago
In a sense, langsec is complementary to verification, as it pertains more to specification than to implementation. Partly it's about using the least powerful level of the Chomsky hierarchy you can get away with, but, if you need to go higher, to do so unequivocally: if you need a CFG, go for a CFG, don't try to wing it with a regex.
- lmeyerov 11y ago
  Sort of. For example, instead of langsec, why not stuff the parser into a module, and implement higher-order contracts at the module boundary? At that point, we get dynamic enforcement of much richer policies, and model checking of richer static ones.
  - nickpsecurity 11y ago
    BOOM! We're thinking along the same lines. Plus, people in safety-critical industries, CompSci, and Eiffel's customer base took up Design-by-Contract or strong specifications for modules with positive results every time I saw it. They all saw the benefits. This became true with more complex code bases. So, stuff like you describe is close to the sweet spot some of us are hoping to find between hardcore, specialist stuff and quick-and-easy, lightweight stuff to knock out most pervasive issues in interfaces and implementations. Note: Far as interfaces, there's been recent work on contracts for passage of time (i.e. ordering of events). So, even temporal considerations might be specified this way in a tool like Eiffel, SPARK, or Java/C# in future.
  - alricb 11y ago
    You still need to think of what's inside the module and how it behaves. It's nice that a contract allows you to, say, kill an attempt at denial of service that messes with the parser, but it's better to make your parser resistant to denial of service in the first place. In fact, at the design level, you need to consider making whatever language you'll have to recognize as simple to handle as possible, with a recognizer that has the least computational power possible. In a real application example, it would be great to isolate the ASN.1 parsing in TLS in some sort of prison, guarded by ruthless guards charged with blowing the parser's brains out if it so much a looks the wrong way. But it would actually be better to use a language that can be parsed with a simpler automaton that is more amenable to verification and inspection, because even if you hold a gun to its head, the parser can still give you the wrong answer.
    - lmeyerov 11y ago
      If someone is running verifiers on the contract language, or worried that their policies are wrong, they can restructure the underlying code or the policies. You're assuming the only verifiable things are parser languages from the 70s.
      - alricb 11y ago
        In many cases you just have to parse stuff (using a recognizer). If you want to verify that your parser is, in fact, parsing the right way, then you have to look at it formally.
nickpsecurity 11y ago
I see it mainly ending up in parsers, transforms, protocols, and function composition. That by itself would be fine given all the problems in those. Then, other stuff handles all the wild code that most certainly won't be LANGSEC compatible but will run the world's software. ;) It's another tool in the toolbox. My hope is they'll find new wisdom on just how expressive one needs to be for optimal productivity, readability, and verification tradeoff. Meanwhile, there's work in DSL-based, verified kernels and software that's already gotten closer to that. A race between all of them to figure out similar things. I wonder who will win. Example of project using DSL's for high-assurance security/correctness http://www.cs.yale.edu/publications/techreports/tr1436.pdf http://www.cs.yale.edu/publications/techreports/tr1436.pdf

alricb 11y ago

In a sense, langsec is complementary to verification, as it pertains more to specification than to implementation. Partly it's about using the least powerful level of the Chomsky hierarchy you can get away with, but, if you need to go higher, to do so unequivocally: if you need a CFG, go for a CFG, don't try to wing it with a regex.

lmeyerov 11y ago
Sort of. For example, instead of langsec, why not stuff the parser into a module, and implement higher-order contracts at the module boundary? At that point, we get dynamic enforcement of much richer policies, and model checking of richer static ones.
- nickpsecurity 11y ago
  BOOM! We're thinking along the same lines. Plus, people in safety-critical industries, CompSci, and Eiffel's customer base took up Design-by-Contract or strong specifications for modules with positive results every time I saw it. They all saw the benefits. This became true with more complex code bases. So, stuff like you describe is close to the sweet spot some of us are hoping to find between hardcore, specialist stuff and quick-and-easy, lightweight stuff to knock out most pervasive issues in interfaces and implementations. Note: Far as interfaces, there's been recent work on contracts for passage of time (i.e. ordering of events). So, even temporal considerations might be specified this way in a tool like Eiffel, SPARK, or Java/C# in future.
- alricb 11y ago
  You still need to think of what's inside the module and how it behaves. It's nice that a contract allows you to, say, kill an attempt at denial of service that messes with the parser, but it's better to make your parser resistant to denial of service in the first place. In fact, at the design level, you need to consider making whatever language you'll have to recognize as simple to handle as possible, with a recognizer that has the least computational power possible. In a real application example, it would be great to isolate the ASN.1 parsing in TLS in some sort of prison, guarded by ruthless guards charged with blowing the parser's brains out if it so much a looks the wrong way. But it would actually be better to use a language that can be parsed with a simpler automaton that is more amenable to verification and inspection, because even if you hold a gun to its head, the parser can still give you the wrong answer.
  - lmeyerov 11y ago
    If someone is running verifiers on the contract language, or worried that their policies are wrong, they can restructure the underlying code or the policies. You're assuming the only verifiable things are parser languages from the 70s.
    - alricb 11y ago
      In many cases you just have to parse stuff (using a recognizer). If you want to verify that your parser is, in fact, parsing the right way, then you have to look at it formally.

nickpsecurity 11y ago

I see it mainly ending up in parsers, transforms, protocols, and function composition. That by itself would be fine given all the problems in those. Then, other stuff handles all the wild code that most certainly won't be LANGSEC compatible but will run the world's software. ;) It's another tool in the toolbox. My hope is they'll find new wisdom on just how expressive one needs to be for optimal productivity, readability, and verification tradeoff. Meanwhile, there's work in DSL-based, verified kernels and software that's already gotten closer to that. A race between all of them to figure out similar things. I wonder who will win. Example of project using DSL's for high-assurance security/correctness http://www.cs.yale.edu/publications/techreports/tr1436.pdf http://www.cs.yale.edu/publications/techreports/tr1436.pdf