[28 August 2018]

Volkswagen is in the news again today, in connection with their engine software that defeated pollution tests by detecting the test situation and changing the engine’s running characteristics.

One might wonder (at least I have wondered) why regulatory agencies don’t require that software for such applications come with a proof of correctness. One obvious answer is that many people think (wrongly) that such proofs are impossible for complicated software, or think (rightly) that if not impossible they are at least rather difficult and probably expensive. But are they more expensive than the recalls and the fines and the lasting hit to the company’s reputation? No, I suspect proofs of correctness would have been cheap by comparison.

Another obvious answer is that the software is almost certainly chock-full of proprietary information, trade secrets, etc., which a proof of correctness would almost certainly end up revealing to anyone who read and understood it. To protect the proprietary information, the proof would have to remain confidential. But then skeptical outsiders would have no way of checking that the proof is valid. There would be a certain inevitable temptation to cheat on the proof, or even to claim that a proof exists when none does. How might one go about persuading outsiders that one has not succumbed to that temptation?

Could zero-knowledge proofs be used to allow outsiders to verify that a formal proof exists showing that a particular piece of software has specified properties, without exposing unwanted information about the software?

Perhaps this amounts to the question: Does the problem of showing that a particular property holds of a piece of software (e.g. that it doesn’t turn on pollution controls only under test conditions) fall into the class NP-Complete? Or is there an NP-Complete problem we could use as a substitute for the informal demand to see that there is a proof for this particular version of this particular manufacturer’s engine control software?