Hacker Proof Code Confirmed (opens in new tab)

This is a very good outreach paper on formal methods. One important thing has to be taken into account and is not quite straightforward to get from the article. Formal methods work on formal models. It is possible to have very good formal models for safety (stating e.g., that the train doors must always be closed when the train is in motion), but it is very hard to come up with good formal model for security (e.g., no one should be able to open the door when the train is in motion). Because of the adversarial setting of security, it is not a good idea to assume that you covered everything in your model (does your model formalize that guy with a crowbar?). Vulnerabilities are often found outside of the specifications of a system. A great example of that is side-channel attacks on cryptography.

Okay, here is my attack:

  1. Find drone operators home addresses, information whether they have significant others, kids. Most of this is public or fairly low security information.
  2. Send goon squad to pick up significant other and kids
  3. Send threatening message with proof you have significant other and kids with the correct level of pressure for drone operator to follow your instructions very carefully.
  4. Now disappear. Very quickly, yeah, the military doesn't like to demonstrate that it has glaring weaknesses in their security and tend to send goon squads the other way to solve the issue.

That said, ultimately I proposed a social engineering attack, there are quieter less threatening methods available that could be effective with enough planning. Ultimately the point here is, formal verification can't work, for it to work the model it is verified against must include every possible form of outside influence and the code at all levels must be 100% verified against that model.

So you need to verify everything (including the workstation doing the verification against absolutely every possibility) this is an exponentially hard problem. This is why formal verification is used only in small areas, and why it does not always work, please see the 1990 Arianne 4 launch failure, where while most of the avionics had been formally verified certain data tests had been removed for optimisation and when a sensor fed bad data meant the computer had a bad cast to different data type ditching important information.

In the world of iot devices, cell phones, and banking apps sorely needs formally verified code. It's kind of anti-agile but engineering still needs to happen in the backend of everything. Sadly, market pressures means shipping these shitty codes the moment it boots.

I like the idea of a formally verified https and crypto libraries because people re-use libraries quite extensively. Putting a few million dollars into critical infrastructure would be a very wise investment.