Thomas Dullien/Halvar Flake’s presentation Weird Machines, exploitability, and proven unexploitability won’t embed but you can watch it on Vimeo.
Great presentation of the paper I mentioned at: Weird machines, exploitability, and provable unexploitability.
Includes this image of a “MitiGator:”
Views “software as an emulator for the finite state machine I would like to have.” (rough paraphrase)
Another gem, attackers don’t distinguish between data and programming:
OK, one more gem and you have to go watch the video:
Proof of unexploitability:
Mostly rote exhaustion of the possible weird state transitions.
The example used is “several orders of magnitude” less complicated than most software. Possible to prove but difficult even with simple examples.
Definitely a “watch this space” field of computer science.
Appendices with code: http://www.dullien.net/thomas/weird-machines-exploitability.pdf