4 ms·

LangSec: Taming the Weird Machines

16 points by jsnell 11y ago

nickpsecurity 11y ago
Stuff like this is a good case of history repeating. The high-assurance systems certified to B3 and A1 had many of the same principles. The system had to be broken into modules, each was implemented in a functionalish way, safer subsets of languages were used, many components were FSM's, all execution states modeled/analyzed, compositions analyzed, and so on. LANGSEC rediscovered some of these ideas. It would probably benefit from a thorough study of old and current methods in high assurance to supplement what its subfield is doing. Maybe even accelerate it in case something was already achieved. Good news is they're both building tools and getting mainstream attention. Great news, actually. :) The problem I have is that the use narrower languages thing is mostly talk with little worked examples that people might adopt. The descriptions, like reducing attacker's playground, remind me of promises of MAC, capability systems, language VM's, and so on. Might be a good thing where same solid principles apply yet again but might also show new stuff will be inadequate. Just not sure at this point. I think the approach taken by SAFE, certified kernels, SVA-OS, and JX is going to end up best route. These raise abstraction up a bit from the machine to primitives with inherent security and safety properties. Then, developer can use high-level language to express themselves with trusted tools converting that to usage of the primitives. Or do it directly like a macro ASM or C library. A language like Haskell, ML, or typed Racket can take over from there with many integrated, Turing-Incomplete DSL's for specific functions. That's how I'm seeing it go if LANGSEC methods go anywhere near real security.
- lmeyerov 11y ago
  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.

16 points by jsnell 11y ago

Stuff like this is a good case of history repeating. The high-assurance systems certified to B3 and A1 had many of the same principles. The system had to be broken into modules, each was implemented in a functionalish way, safer subsets of languages were used, many components were FSM's, all execution states modeled/analyzed, compositions analyzed, and so on. LANGSEC rediscovered some of these ideas. It would probably benefit from a thorough study of old and current methods in high assurance to supplement what its subfield is doing. Maybe even accelerate it in case something was already achieved. Good news is they're both building tools and getting mainstream attention. Great news, actually. :) The problem I have is that the use narrower languages thing is mostly talk with little worked examples that people might adopt. The descriptions, like reducing attacker's playground, remind me of promises of MAC, capability systems, language VM's, and so on. Might be a good thing where same solid principles apply yet again but might also show new stuff will be inadequate. Just not sure at this point. I think the approach taken by SAFE, certified kernels, SVA-OS, and JX is going to end up best route. These raise abstraction up a bit from the machine to primitives with inherent security and safety properties. Then, developer can use high-level language to express themselves with trusted tools converting that to usage of the primitives. Or do it directly like a macro ASM or C library. A language like Haskell, ML, or typed Racket can take over from there with many integrated, Turing-Incomplete DSL's for specific functions. That's how I'm seeing it go if LANGSEC methods go anywhere near real security.

lmeyerov 11y ago
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.