3 ms·

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 le

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

by alricb 11y ago

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.