3 ms·

It wouldn't even be that hard: Just require the vendors to publish the state machine diagram, and if an examiner discovers a hidden “weird machine”[1], they rec

It wouldn't even be that hard: Just require the vendors to publish the state machine diagram, and if an examiner discovers a hidden “weird machine”[1], they recommend a sanction that depends on how powerful the weird machine is. If it’s Turing equivalent, then it gets banned outright. If the weird machine was knowingly created and hidden, then we start talking about fines and other penalties. [1] http://en.m.wikipedia.org/wiki/Weird_machine http://en.m.wikipedia.org/wiki/Weird_machine

azernik 12y ago
Most IT equipment is not built in such a way that its behavior is formally-verifiable or even formally-describable as a state machine - for the most part, we're talking about a full Linux installation that comes with the vendor's preferred web server (for administration) and default routing configuration.
- noblethrasher 12y ago
  Sorry, I should have made it more explicit that I'm just talking about the stuff at the edges. For instance, we can do this with something like a TCP library just by evaluating it against the state machine published in the RFC. Similarly, custom protocols are ultimately just state machines, and it's easier to effect secureness when you limit the protocol to a regular or context-free grammar[1]. But, if the vendor insists that their protocol needs a more powerful grammar, then at least we can start talking about security/feature trade-offs in formal terms (i.e. vendors would have to justify their decisions with math and computer science instead of feature checkboxes and pricing psychology). [1] http://www.cs.dartmouth.edu/~sergey/langsec/ http://www.cs.dartmouth.edu/~sergey/langsec/
  - moe 12y ago
    How do you "limit the protocol to a regular or context-free grammar" in a consumer internet router?
    - noblethrasher 12y ago
      Since IP4 and TCP each have a “length field”, they're stuck being context-sensitive I suppose. But, on the other hand, since the length fields are bounded, you could treat each value as a separate token (though it would create a huge state machine). But, routers are not the only edge devices that worry me. Smart tvs|phones|toasters|… are also edge devices with respect to the topology of your “personal area network”.
  - azernik 12y ago
    Sure that works for a restricted set of vulnerabilities. But generally security vulnerabilities don't stem from bad protocol implementations, but from misconfigurations of generally-functioning software, and bad choice of policy. (For example, this vulnerability was just an extra hardcoded admin account in the router's web console.
    - noblethrasher 12y ago
      If I know what the state machine/protocol looks like, I can have a better idea about how much stuff should be present. For example, if the vendor claims that the product is limited to a regular grammar (a “plus” for security), but the implementation contains extra stuff in the data section, then an audit can flag it since a finite state machine should (theoretically) only need code.
  - drdaeman 12y ago
    Having documentation or source code is nice, but not going to help, because you have to verify the system in question actually conforms to the documentation. With the software - to a certain extent - this is possible with static analysis, but with hardware this is nearly damn impossible. Nonetheless, having a solid formalizations for network protocols is a good idea. But this just won't happen.

azernik 12y ago

Most IT equipment is not built in such a way that its behavior is formally-verifiable or even formally-describable as a state machine - for the most part, we're talking about a full Linux installation that comes with the vendor's preferred web server (for administration) and default routing configuration.

noblethrasher 12y ago
Sorry, I should have made it more explicit that I'm just talking about the stuff at the edges. For instance, we can do this with something like a TCP library just by evaluating it against the state machine published in the RFC. Similarly, custom protocols are ultimately just state machines, and it's easier to effect secureness when you limit the protocol to a regular or context-free grammar[1]. But, if the vendor insists that their protocol needs a more powerful grammar, then at least we can start talking about security/feature trade-offs in formal terms (i.e. vendors would have to justify their decisions with math and computer science instead of feature checkboxes and pricing psychology). [1] http://www.cs.dartmouth.edu/~sergey/langsec/ http://www.cs.dartmouth.edu/~sergey/langsec/
- moe 12y ago
  How do you "limit the protocol to a regular or context-free grammar" in a consumer internet router?
  - noblethrasher 12y ago
    Since IP4 and TCP each have a “length field”, they're stuck being context-sensitive I suppose. But, on the other hand, since the length fields are bounded, you could treat each value as a separate token (though it would create a huge state machine). But, routers are not the only edge devices that worry me. Smart tvs|phones|toasters|… are also edge devices with respect to the topology of your “personal area network”.
- azernik 12y ago
  Sure that works for a restricted set of vulnerabilities. But generally security vulnerabilities don't stem from bad protocol implementations, but from misconfigurations of generally-functioning software, and bad choice of policy. (For example, this vulnerability was just an extra hardcoded admin account in the router's web console.
  - noblethrasher 12y ago
    If I know what the state machine/protocol looks like, I can have a better idea about how much stuff should be present. For example, if the vendor claims that the product is limited to a regular grammar (a “plus” for security), but the implementation contains extra stuff in the data section, then an audit can flag it since a finite state machine should (theoretically) only need code.
- drdaeman 12y ago
  Having documentation or source code is nice, but not going to help, because you have to verify the system in question actually conforms to the documentation. With the software - to a certain extent - this is possible with static analysis, but with hardware this is nearly damn impossible. Nonetheless, having a solid formalizations for network protocols is a good idea. But this just won't happen.