…through formal software verification. This seems like sort of a big deal. Particularly in the era of the Internet of Things and self-driving cars. Of course, the weakest link in security will remain the flawed unit between the seat and the keyboard.
18 thoughts on “Hacker-Proof Code”
Comments are closed.
Still boggled that “we” haven’t standardized on bare minimums like digitally signing email.
The entire field of phishing relies on exactly that PEBCAK.
A standard exists for signing and encrypting email (one implementation at https://www.enigmail.net/ ) , but it’s not a default supported function of any major email client. And the very popular webmail doesn’t play well with the security considerations.
And yes, widespread use of secure email signatures would make spam a bit easier to deal with.
Formal verification of software was a ‘new thing’ when I was in college circa 1980. Huge blobs of ‘proof’ for trivial amounts of code.
Looking back at it, I’m perhaps overestimating my skepticism, but I seem to remember thinking it just added an additional level of indirection: even if the ‘proof compiler’ was bug-free, you would still have the potential for a flaw in the underlying design.
In other words, you could have a provably-correct implementation of a broken idea.
It’s entirely possible that this is in fact not snake oil, but I’d need to spend more time than I have to spare to convince myself otherwise.
Final comment, google ‘Fred Brooks’ and ‘No Silver Bullet’ and read the essay. Also, read “The Mythical Man-Month” and think about how it applies to ‘big policy’ at the government level.
Here endth the rant.
As a software engineer I’ll believe it when they can use their formal verification tool to verify its own code. Even then it doesn’t mean that the software won’t depend on code which isn’t according to spec (something which unit testing can handle) or that the spec is poorly written (which unit testing can’t handle either).
Formal verification methods are supposedly used in chip hardware design with some measure of success though.
something something Turing machine
something something Halting Problem
Oh you can solve the Halting Problem with so called 2nd order logic.
It’s always been about human failure, not the computer. For 40 years I’ve argued there is no reason code can’t be made secure and for 40 years people have been telling me I’m wrong. Here we have an article that says a formal proof exists. Which is just another case where I just needed to let time pass for everyone else to catch up.
there’s no way to run a program through every conceivable input
There is no need to. That isn’t how most proofs work.
a program that includes its formal verification information can be five times as long as a traditional program that was written to achieve the same end
This assumes the formal verification has to be part of the code itself. I don’t see that it has to be. Also, more code means more possibility of errors.
My code has errors. The libraries it calls have errors (almost all the major issues in the system I support in my day job have come from third-party libraries that we didn’t write). The operating system has errors. The hardware the operating system runs on has errors. The specification for the code has errors.
And when you throw in neural networks, as many people are trying to do for things like image recognition… it’s game over.
Oh, and most hackers break in through buffer overflows and the like that let them inject their own code into the program. Those are not hard to eliminate just by using buffers that can’t overflow or underflow.
They’re also some of the things that cause those third-party library crashes, because they aren’t using safe buffers. One of the reasons our code rarely crashes and is hard to hack is because we are. We never, ever trust any external input, it’s always validated.
Pascal. The hacker-proof language!
The code is available on GitHub, if you’d like to check it out. The formal methods approach is specific to the processor, for what it’s worth. Here is a good place to start, if you’re interested.
What’s the difference between this and the static provability of the earlier (non-object-oriented) version of Ada?
But can it prove code will fail in a safe manner given input outside the scope of the specification?
If that can be defined, then that behavior can be verified, yes.
I just know I HAD a working Program Prover Program lying around here somewhere since the 80s. Trouble is, it only runs on a Silicon-On-Sapphire CPU with Gallium Arsenide MRAM caches and Mag Bubble Memory.
Sorry ’bout that.
Um, you left out Josephson junctions — that must be why your program doesn’t work.
Program verification has made steady progress in the last few decades. One interestnig set of tools closely related are SMT (Satisfiability Modulo Theories) solvers. These are an offshoot of boolean satisfiability solvers that have become practically important due to improved algorithms. There’s a standard interface for these solvers, SMTLIB, that allows different solvers to be plugged into applications that need theorem proving.
There’s also been steady interest in work with dependent types. These are datatypes in which component types depend on other values. There’s an isomorphism (Curry-Howard) between such types and logical assertions with quantifiers, and between programs having such types and (constructive) proofs of the logical assertions.
Formal Verification – The “Gold” Standard… 🙂
“I believe that the final bug in TeX was discovered and removed on November 27, 1985. But if, somehow, an error still lurks in the code, I shall gladly pay a finder’s fee …