Sergey Bratus, a Dartmouth computer science researcher, writes on language-theoretic security, weird machines, and exploit programming.
HN cites his langsec work on input validation and 'weird machines' when discussing parsing flaws, exploits, and CPU bugs.
There was this recent security presentation about formal language-theoretic reasons why message-length prefixes are a bad idea. http://www.cs.dartmouth.edu/~sergey/langsec/
The problem was that it causes unnecessary complexity in validation and parsing, as <length-of-message><message>... describes a context-sensitive grammar, while a more XML-, JSON-like syntax with delimiters <delim><message></delim>... is context-free. The complexity of proper CSG validation can be exploited for resource-depletion/DOS attacks, while not validating the syntax of a message leaves part of the program that uses the data in these messages with potentially invalid data, putting it into an inconsistent state, possibly leading to DOS or worse exploits.
At least that's what I got from their presentation, which was very interesting BTW, especially the part about "weird machines"--that's basically the inconsistent state, the emergent machine that is made out of all the things an attacker can make a system do by exploiting it. It was also extremely geeky.
It just left me wondering: if I understood this right, every protocol that uses message-length prefixes is at least vulnerable to resource-depletion attacks, and there's no way of solving this short of proving P=NP. But that's quite a lot of protocols! Why isn't the Internet burning down as we speak?
I think gpcz was suggesting something more along the lines of an entirely new approach to protocol implementation, like VPRI's TCP/IP stack that Jeff Moser describes[1], rather than just swapping out C for something else while keeping the hand-written aspect.
> Let's say we want to build the TCP/IP stack of an operating system. A traditional implementation might take 10,000 lines of code. What if you rethought the design from the ground up? What if you could make the IP packet handling code look almost identical to the RFC 791 diagram which defines IP?
If the industry as whole could agree on this approach in a move similar to the Dijkstra/structured programming move that happened a few decades back, the sort of verifiable interoperability + security that Meredith Patterson and Sergey Bratus (who you may recognize from Occupy Babel![2]) call for would be closer to reach[3].
1. Jeff Moser. Towards Moore's Law Software: Part 3 of 3. https://www.youtube.com/watch?v=UzjfeFJJseU
2. Occupy Babel!. http://www.cs.dartmouth.edu/~sergey/langsec/occupy/
3. Meredith Patterson. LANGSEC 2011–2016. https://www.youtube.com/watch?v=UzjfeFJJseU
> Naive question: is it viable if we started using [a Turing-complete programming language]
This is actually a good question. The people who are not asking and going right ahead with that plan are doing a dangerous thing. <https://www.cs.dartmouth.edu/~sergey/langsec/occupy/> It's not viable because a subset of people would like to have the following properties upheld:
• Parsing configuration should be decidable and finish in finite time.
• Parsing configuration should not be a security exploit.
• I should not have to implement the Emacs runtime just to parse its configuration file.
> something that's both more flexible but still strict and unambiguous. I wonder if it's possible?
This really depends on what you mean by these words; I'm interested to hear your idea in detail. Meanwhile, have a look at Dhall <https://dhall-lang.org/> and the other languages mentioned in <https://news.ycombinator.com/item?id=29221643> and compare.
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/
> Robustness_principle
A slight variation on this is important for security. Be liberal in what you accept, but define what "liberal" means. It's important to define what counts as a valid input. If you don't have a validation/recognizer verify that the input is acceptable, you are probably creating a "weird machine"[1] waiting to be exploited in ways you didn't expect.
I highly recommend Meredith and Sergey's talk[2][3] at 28c3, "The Science of Insecurity", where they explain this from a language-theoretic perspective.
[1] http://www.cs.dartmouth.edu/~sergey/wm/
[2] https://media.ccc.de/v/28c3-4763-en-the_science_of_insecurity
[3] http://www.cs.dartmouth.edu/~sergey/langsec/insecurity-theory-28c3.pdf
> This begs the question: if old features are this broken, what about the new ones
You can find so called "specification updates", which - as the name implies - update the specs to match actually released hardware ;)
Available for all CPU families from both Intel and AMD, easily go into tens or hundreds of positions. (Though I haven't seen the Ryzen one released yet).
And then somebody recently linked this (2010) - allegedly there are bugs exploitable for privilege escalation:
http://cs.dartmouth.edu/~sergey/cs258/2010/D2T1%20-%20Kris%20Kaspersky%20-%20Remote%20Code%20Execution%20Through%20Intel%20CPU%20Bugs.pdf