I'm not convinced.
If lockpicking and other ancient hobbies are anything to go on, it doesn't matter how many redesigns you go through; people will just create new specialized/innovative tools to break/attack the most popular ones.
If lockpicking and other ancient hobbies are anything to go on, it doesn't matter how many redesigns you go through; people will just create new specialized/innovative tools to break/attack the most popular ones.
Programming languages can artificially limit the attack surface. (Up to hardware exploits which can subvert the processor itself.)
This is analogous to virtual attacks on information systems which are hardened against familiar routes of ingress and vulnerable to those which are wonderful and surprising.
Of course computers are eventually physical reality, too, and things like rowhammer show that you don’t even need traditional “bugs” to escape your mathematical utopia.
But all the bugs talked about here are entirely the fault of the software.
Are you going to fuzz the program "x = y+1; return x;", or are you convinced already that it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x), and that it will never access memory out of bounds?
Formal verification is exactly that, just usually in less obvious scenarios. Advanced type systems do the same implicitly by making expressions that would violate such properties (or where they cannot be proven) not type check.
Computers these days are sufficiently complex and with enough abstractions that there’s no such thing as a guarantee.
> Fuzzing is only relevant where formal verification cannot be exhaustively applied (which is reality in turing complete languages), or is too cost-prohibitive.
Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.
Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.
> it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x)
And it does not matter, since the point of formal verification is to help taking those issues into account.
Of course, even perfect software is susceptible to physical attacks on the hardware it’s running on, but that’s different.
For physical locks, you cannot even rigorously define the "input".
[1] Not always, unfortunately, if your language is turing complete. You might be able to prove weaker, but still very useful statements, like "no input will cause a point to be dereferenced out of bounds".
Most of the time, a barrier to elevated privileges that was not correctly implemented, i.e. a bug, not anything the designer did not anticipate.
> Can't you "brute force" even the most theoretically rock solid privilege boundary by simply attaching your own computer to the memory in question?
So? Does that mean it's not worth looking at the paths where the attacker does not have physical access of the machine that sits in some data center's secured basement?
I don't think this is obvious, even for theoretical software, much less for practical software. Even formal methods have limitations.
A very public recent example was of the formally proven logic in Intel and other processors around speculative execution (Spectre, Meltdown etc.). That logic was formally proven not to leak information, but the formal model wasn't actually sophisticated enough. Note that these weren't hardware bugs (they weren't bugs in the electrical components of the processor or in the analog logic), they were logic bugs in the processor's code (whether that was microcode or burned into the processor is less relevant).
In general, you can prove that a piece of software adheres to some specification, but you can't prove that the specification itself is complete enough.
Of course, realistic software has many more layers of uncertainty, and realistic formal verification is far to costly to apply to anything but very short programs.
Still, there are a lot of properties that are easy to state, and a lot of properties that are feasible to prove, and the intersection of these two can be very valuable in eradicating common issues in critical software, be it out-of-bounds pointers or your garden variety type confusion. (Again, not always possible, thanks to the halting problem, but often.)
The cost may indeed be prohibitive, though.
Had SQLite been written in a language that would have made it easier to perform a proof of correctness then it wouldn’t be nearly as widely used and because of that language choice and then it likely wouldn’t have had the resources (financial nor community input) to complete a proof anyway. So would it have actually been any less buggy if it weren’t a C project?
Sometimes worse is better and moaning about “what if” is neither constructive nor even warranted when you consider just how well written SQLite already is and how abundant the tests are.
> Sometimes worse is better and moaning about “what if” is neither constructive[...]
... and yet here we are talking about extremely dangerous and possibly far-reaching vulnerabilities in SQLite.
But there are definitely ways to mathematically prove that parts of a program do what they should, or do not do what they should not.
Whereas if I tell you that x is bigger than y if x is y plus 1, that’s definitive.
Examples are a sorted list that inadvertently becomes unsorted while the rest of the program still assumes ordering, or more simply and classically, a pointer that's pointing out of its assumed bounds.
There is no "security model" to consider on that level, and with respect to lockpicking I just wanted to explain why software engineers have access to wonderful tools and methodologies that designers of physical locks don't.
I took the comment in two parts; the second being a tangential suggestion that security is financial.
The first was more interesting. Taken to be a reply to your claim that x=y+1 implies x>y, it is grounded more in theory. The claim is one grounded in a given model - a prevailing mathematical one - and is undoubetdly correct in that model and in the many of the models we use around us.
That does not, surprisingly, make it true.
There are countless models in which it is false, though it seems unlikely these are useful models.
There are also models which are to a degree isomorphic to the current (standard?) models of fancy. In these may lie a way to subvert the expectation of their version of "x>y when x=y+1"
Most code doesn't check whether incrementing a variable causes an overflow, so in practice the test you're referring to is still vulnerable.
It's not magic or unpredictable, we know exactly how integers or any other representable data type behaves. (Also note that you were assuming integers here, as floating point would behave yet another way.)
I wasn't proposing a "test", I was demonstrating the difference between mathematical rigor and physical reality, and in my chosen domain for x and y, overflow is not happening.
Once you get into moving parts and, even worse, useful moving parts, things get a lot trickier. But if you severely limit your inputs you might be able to get somewhere. Like one of those locks where the mechanism pulls the key completely inside before applying it to the keyway: https://www.youtube.com/watch?v=OLsJDELd4lo https://www.youtube.com/watch?v=5J2rwawhZWI I'd expect many designs in that class to be immune to most definitions of 'picking'.
But the vast majority of security problems don’t usually rely on CPU bugs, do they?
I don’t claim it’s exhaustive in general, but it may well decimate a massively common class of problems, and eliminate some of them entirely.