This brings up something I've often wondered about: we can basically guarantee that a very short snippet of code (say, a few lines) is secure, right? However, there is no real way to guarantee that full programs are secure. Can we not truly guarantee that some portion of code is secure, or is it simply the amount of code that makes it impractical (and financially infeasible)? If the latter, what is the practical boundary?
> we can basically guarantee that a very short snippet of code (say, a few lines) is secure, right?
That's the problem, we can't do that. Between hardware flaws like rowhammer, meltdown, spectre, etc. it's not possible to say that a piece of code isn't going to trigger something intentionally or not.
You can say that something very very likely doesn't trigger any known vulnerability, but only while also specifying the exact hardware to run it on and probably other external variables.
> Between hardware flaws like rowhammer, meltdown, spectre, etc. it's not possible to say that a piece of code isn't going to trigger something intentionally or not.
I guess I was thinking software vulnerabilities specifically (although in the context of this article I should have thought about the hardware side more). Or to be even more specific, flaws that are from that program in particular.
You can formally prove that a program is a refinement of a specification, or that a subroutine always obeys certain invariants (when executed honestly.) See Dafny and ADA-SPARK for examples.
It reduces to theorem proving with a SAT solver like Z3, if your language is Turing-complete and your invariants are abitrarily general. SAT solvers are fast and powerful these days, but the usual issues are:
1. It's too cumbersome to define invariants or write the type of specs that can check program correctness.
2. Things get exponential as state space increases.
Modern checked languages are finally addressing #1, though they will sometimes have blind spots (e.g. Dafny can't reason about concurrency, TLA+ (which can) is very abstract and high level.)
Writing programs as bundles of isolated, formally verified modules, then proving the correctness of the program with a high-level spec that assumes module correctness, lets you scale to real, large programs. This is how Dafny works, for example -- functions declare pre and post-conditions, and so Dafny can throw away its reasoning about callee function's internals when checking a caller.
This strategy really is overlooked! It's powerful enough that you can eliminate memory/argument checks at compile time, ditch all your unit tests and KNOW your program implements a spec. It should be mandatory for all safety-critical systems that can't rely on hardware fail-safes (e.g. airplanes.)
Software side there's a lot that can be proven and said about small sections of programs. I think a sibling commenter talked about an ISO standard related to that (And I think it covers some hardware bits). My layman's understanding of it is that it's a way to specify as many assumptions about how the code will be run, where, and what side effects it will have and no others. That makes for a really nice set of assertions but the end effect is that you can't say anything about certain kinds of programs; i.e. This program is safe, That program can't be safe, and then these programs are unknowable. Godel should never have been allowed to publish anything.
we can basically guarantee that a very short snippet of code (say, a few lines) is secure, right?
I’m not sure that’s true, but even if it is, you have to ask: Which few lines?
Let’s say we have the technology that can analyse (say) five lines of code and prove them completely correct and secure. That doesn’t mean you can prove a 500 line program to be secure by running the analysis on each 100 sets of five consecutive lines. Code in one place can affect the logic elsewhere. So now to prove a 500 line program correct, we’d need to analyse every possible combination of 5 lines chosen from the 500 => 255244687600 different proofs to check!
It's not just that. Before you can prove anything "correct" you need to define what "correct" means. Now you have the meta problem of proving that your definition of "correct" is correct.
