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.
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).
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.
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.
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.
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”.
