This is good writeup but very misleading title. Article essentially describes using SPARK to avoid runtime errors in firmware such as overflows. But that is far cry from avoiding drone crashes. You can do lot of these things with sophisticated code analysis (although not all of it). But the thing is that it doesn't solve the primary issues of algorithmic errors or even errors that might occur because of things like timing issues or sensor noise. Of course, it doesn't do anything about obstacle detection and avoidance. I would imagine that very small number of crashes occurs due to runtime errors in firmware.
There have been lot of other work going on for verifiability for realtime firmware code. For example P programming language: https://github.com/p-org/P. But still it doesn't tackle the issues mentioned above that causes majority of crashes.
> it doesn't solve the primary issues of algorithmic errors
SPARK does more than described in this post, and you can indeed use it to verify correctness properties of your algorithms. If I remember correctly, it interfaces with Why3, which is itself a platform for interfacing with many many provers like Z3, Vampire, CVC4, etc.
SPARK does more than just "sophisticated code analysis". If you ask it to.
Doesn't this just shift probable bugs from code to the proof? At least if you are not Nasa/Intel/Amazon with a lot of resources to dedicate to this?
I guess (just a guess, maybe misinformed) that proper testing and fuzz testing of code is considerably more beneficial than finding bugs by trying to prove it.
Proofs are often useful even if sometimes they are not "fully" trusted in some sense, and a lot of mechanisms and research in formal methods is about removing "trusted" components in viable ways. You don't even need to get especially mathematical, sometimes bog-standard engineering is enough to cover the margin of error depending on your goals... (e.g. if you have a property shown by an SMT solver to be true, you can do things like a 3-way tiebreaker and compare 3+ smt solvers for their output for a better guarantee).
The people working on formal validation tech are well aware of these limitations in the tech -- the concept of a "Trusted Basis" is a core component of the whole field, around which many techniques revolve.
Systems like seL4 use different approaches, such as "translation validation" which completely removes the need to trust a compiler toolchain, for example (because they do an automated equivalence proof between the generated assembly and a high level specification, they can just not care about the compiler). Interestingly, I know someone who worked on seL4 before its public release -- in fact at several points in the process, they got some parts of the specification wrong. You'd think this would be a death blow. But it still turned out many of these incorrect specifications weren't totally wrong, or useless at all -- in some cases they simply were not strong enough to show other desirable properties. To handwave an example: Maybe they wanted to show "No process can violate the address space of another process or halt it illegitimately" as the specification, but accidentally said "No part of the system can be put an invalid state or hung with core kernel APIs". They aren't the same thing, but it turns out, the second, 'wrong' case still eliminates a useful class of errors (while being a subset of the real specification, because to be unable to interfere with the address space of any other process or hang it somewhat implies you can't hang it, or corrupt it illegitimately, through system APIs.)
It's not (except maybe very rarely) as simple as "proof is bad" or "proof is good". There is a spectrum here along which you can assess their utility -- just like any engineering challenge.
It does take a lot of resources to do though, this is correct. The tech is improving at a pretty fast pace, and we're already getting to the point of having fully verified compilers and OSs (CompCert, seL4). It is certainly becoming more viable to do this all the time. It's still not easy, and takes a very, very different set of skills than most engineers are equipped with.
> I guess (just a guess, maybe misinformed) that proper testing and fuzz testing of code is considerably more beneficial than finding bugs by trying to prove it.
For average software, this is true, but it's mostly a cost question. Frankly you don't need mathematics to make shit, insecure software less insecure, you can absolutely improve them without that.
But they don't really do the same thing anyway; proofs show a mathematical absence (or prove a mathematical fact) of certain classes of errors. Fuzzers can only show the existence of certain errors -- they cannot definitively prove anything other than "Some bugs exist".
There was a paper recently (I can't find it) that explored this idea; essentially the authors injected obvious, "should-be detectable" bugs into many pieces of software, then ran fuzzers over the software to see how many of the injected bugs could be found. The takeaway was, IIRC: fuzzers didn't find anything close to the real number of injected bugs, not even considering bugs that weren't found and were not injected by the authors. Which means that despite their automation triumphs, we could very easily be missing real, catastrophic errors, at a very high rate.
Fuzzers haven't definitively proven that there isn't another Heartbleed out there, somewhere.
Still, I don't think you can use it to avoid (physical) crashes due to an incorrect algorithm, simply because theorem provers work on a cognitive basis but control systems operate on continuous fields (i.e. transfer functions defined over the complex numbers).
Believe it or not, people working on theorem proving are aware that computers use finite arithmetic, and they take this into account. Yes, floating-point computations are hard and painful to verify. But no, it's not that easy to hand-wave away the whole field :-)
Honestly, it seems floating point computations are, by some measure, possibly pretty old at this point in the formal methods world! Intel has been investing in formal verification of its floating point units since at least the 90s when FDIV hit them, and this was when the tech was way worse than what we have today!
Hell, CompCert -- which you can download today -- already has a proven adherence to IEEE-754 floating point, implemented by specifying IEEE-754 semantics in Coq, then using that to create a proof the compiler correctly preserves the semantics of IEEE-754 during the compilation process.
People doing theorem proving and formal methods know what complex numbers are, I can assure you. Mathematicians have plenty of statements about the properties of complex numbers, and many theorem provers have libraries that even formalize those statements and proofs in mechanized, automated ways that can be trusted. I'm not sure how "complex numbers are involved" is any more of a mystical problem than "finite-field arithmetic is involved" is a problem: it isn't.
I think I get what you mean, though. No, you cannot prove "my drone is magical and awesome and will never crash land even if I tell it to, and it takes the best pictures of any drone". You cannot mathematically prove "My on-board sensor will always work and defy the laws of physics and never be inaccurate". You CAN mathematically prove "My drone control software never reaches an illegitimate state, that would cause the system to deadlock or hang due to a software error, making the drone crash in a possibly dangerous, uncontrolled way". You CAN prove "My software will respond within exactly N cycles, at most, to any external incoming sensor signal".
That kind of guarantee is extremely valuable for such systems. It isn't easy (and requires deep, conjoined assumptions and proofs of both the hardware and software), but it's hardly impossible.
And sure, there is only so much the model can prove to you, at some point it has to exist "in the real world". This isn't really a counter-point to the actual formal methods field, though.
To couch it in a more concrete example: when people like Intel say "our CPUs don't catch on fire", they only mean it in a very specific sense. Sure, you can shove newspaper up next to your heatsink, and then when it catches on fire say "See! You were wrong!" But the reality is that their statement is sort of couched in the assumption that, well, you aren't going to do that. It's fairly reasonable to assume some limitations of your model. But this really has very little to do with being able to formalize general mathematics (like complex numbers or finite fields or N-dimensional spaces) using a theorem prover, or whatever.
I don't get the point, it looks to me like the typical C mentality that memory corruption isn't an issue and every 10x programmer is able to write alone C code without errors.
Meanwhile the CVE database maintainers and black hats appreciate this mentality.
IMO secure software comes from knowledge and care as much as from a safer language, if not more. But then there is performance, in which what no "modern" "safe" language even comes close to C.
>Meanwhile the CVE database maintainers and black hats appreciate this mentality.
And how much of CVE-worthy software is not written in C ?
> in which what no "modern" "safe" language even comes close to C.
Modula-2 and Pascal dialects were as fast as C back in the 80's and 90's, before the industry decided to settle on C as UNIX got adopted and just like node.js and JavaScript, C escaped outside UNIX.
The quality of C code in home computers was a joke even to junior Assembly programmers.
Of course C is fast in 2016, with UB all over the place and 40 years of research in compiler optimizations taking advantage of it.
> And how much of CVE-worthy software is not written in C ?
And how much software is written in C without any need of doing so?
But never mind, the only way to convince you guys is to have CVE meltdown after meltdown, until the industry has lost so many millions that it will eventually change.
Millions of dollars and euros are spent in language research, how to make C code safe, since the language got adopted.
He writes out a list of places where C++ is undoubtly better and can help write safer code over the alternatives when you question him -- not perfect code, just code that better utilizes modern features, to help reliability -- and your response is... to avoid his question, address nothing, and do some random handwaving with an FQA.
Honestly, the response would be funny if it wasn't just a little bit pathetic. But I've learned not to expect much from people who can only handwave with no actual substance. Programmers are good at that.
2016 and people still take the C++FQA for real, uau!
Ada is a great language and I also would rather use it instead of C++, but it isn't packaged with any SDK for the OSes that I care about, nor does it have a good integration history with Java and .NET.
Using third party tooling for production code is always an extra development cost, so I do the best with the lemons I get.
There have been lot of other work going on for verifiability for realtime firmware code. For example P programming language: https://github.com/p-org/P. But still it doesn't tackle the issues mentioned above that causes majority of crashes.