I've been collecting some books on proof to build a foundation for better learning formal verification of software. The capabilities of modern provers, esp if combined with automated methods, can handle a lot more practical software than in the past. Even those like SPARK Ada with a lot of automation has properties that require manual proof. Certain things might also be easier to prove manually with a more powerful logic.
My hope is that I find enough feedback on good/bad of cheap or free resources on this topic that I can determine some default recommendations for people curious. The problems can be addressed with supplementary material. Eventually, the defaults would be good enough that the process would happen faster. A larger number of people centering on the same resources might become a community for helping new people. That might increase the inflow. Simultaneously, some percentage of these people are working on tools, esp automated, to make the proof process more productive. Over time, we might have a much larger segment of people working on formal verification than we do now. Maybe even large enough to sustain more tool development by contributions or licensing.
So, that's why I'm looking at books like this with what I think they might help us achieve. I'm way too out of my depth to know if it will work. I just know accessibility, better learning materials, and network effects always help.
Example tools below for sequential programs, concurrency, and hardware:
I would be interested in your repository of resources, is it something you plan to make public soon?
Something I find very useful as a developer is to see how tools work on concrete examples. For formal verification, this is well examplified by the document "ACSL by Example" about Frama-C:
This shares with the O'Reilly Cookbook series (https://ssearch.oreilly.com/?q=cookbook) the goals to get very concrete immediately, on code that the reader might have to write or have already written.
It's funny you mention that because I've been collecting those Frama-C, SPARK, and WhyML papers in case anyone wants to port examples between languages. One of the things I [re-]downloaded a week or two ago for that was ACSL by Example. :) I also got floating point verification (I know you all are doing that), one on string functions, and one on GMP for big integers. I don't have any of it published in an online repo yet. I mostly just submit it to Lobste.rs for their crowd that likes deeper tech and give it to individual people via social media or email.
The stories section of that link has examples including recent ones on floating point and interior point. The interior point paper you might find interesting since they have a specific specification and coding style to achieve full automation.
You might also find Lea Wittie's work on Clay interesting. I was looking at her dissertation in case one could use SPARK in similar way to model I/O or concurrency.
I like that you're all doing that. That does help a lot. I plan to do my part to some degree in the near-ish future: I bought the High-Integrity Applications book for SPARK and Stavely's Toward Zero-Defect Programming for Cleanroom.
SPARK book looks well-written but kind of packed with info esp on the language. Might take some time for me to learn. The Cleanroom book is highly approachable with the method mostly being algebraic focused on human understanding with symbolic-style verification of some control flow mechanisms. That was from a skim, though, with full method maybe being harder. My plan is to get back into feel of doing this stuff by trying Cleanroom first followed by using what SPARK book teaches me on all the same stuff. Both during and after learning SPARK, I'll use it on little functions like in the ACSL by Example book. Note that this assumes some other research doesn't take higher priority for me like my Brute-Force Assurance concept that mixes languages with their verification tooling.
I took the first steps of trying to get the SPARK GPL environment downloaded and installed. That wasn't working for some reason. It's harder than necessary to install: should be a well-packed installer like most things are on major Linux distros (esp Ubuntu) if wanting maximum adoption/experimentation. Since newest stuff from download link failed, I pulled older stuff through Synaptic which at least got GNAT working on doublec's Hello World example below. SPARK 2014 refused to run on it, though.
Thanks for the links to interesting articles. Definitely interested in the interior point formalization and proof. As I expected, it's already quite hard even without taking floats into account. (In the conclusion they say "We worked with real variables to concentrate on runtime errors, termination and functionality and left floating points errors for a future work.") Our experience with industrial users using floats is that most are not interested if we don't deal with floats. Otherwise no guarantees can be given for the actual code.
Re learning SPARK, we'll have a brand new learning website during the year for Ada and SPARK, to replace the e-learning website u.adacore.com. This should make it far easier to learn Ada/SPARK, hopefully with online tweakable examples as on https://cloudchecker.r53.adacore.com/
"Our experience with industrial users using floats is that most are not interested if we don't deal with floats. Otherwise no guarantees can be given for the actual code."
That makes sense. The reason I kept it was that I saw some conference...
...talking about doing ERA as what looks like a replacement for floats. If it gets built, then the code for reals will either be verified directly or an equivalence checker between a real and float implementation will be next move. So, any papers verifying reals might have work that comes in handy later is my thinking.
"we'll have a brand new learning website during the year for Ada and SPARK, to replace the e-learning website u.adacore.com. This should make it far easier to learn Ada/SPARK"
Thank you! That and the list will probably be very helpful.
"I'm curious about your Brute-Force Assurance concept, can you say more?"
I was describing it a lot but I noticed a lot of verification tech is getting patented in U.S. for questionable reasons. I'm a bit concerned about possibility a party in U.S. will patent it, lock it up, or troll implementers if I describe it in detail in way that doesn't count as prior art. From what I've been told, putting it in a peer-reviewed journal would establish prior art to block that. Decent shot anyway. So, I think I'm going to try to do a detailed write-up first to make sure as many people can adopt it as possible. I'm also thinking about an appendix that consist of a brainstorming session of every way I can think of possibly applying it to block some mix-and-match type of bogus patents.
I can tell you the concept involves translating a program into an equivalent representation in multiple languages to run their associated tooling on it. The results are assessed manually or automatically to see if they apply to original form. Original is fixed repeatedly until the tools each say Ok. Each tool is picked for being good at something others aren't. Rust for temporal safety, SPARK for automated proving, a tool-specific language for termination checking, (more properties/tools here), and finally C for its tooling and final release. I've seen people attempt to integrate different logics or use multiple tools. I've never seen people do that cross-language using everything from test generators to static analysis to proofs. It seems my hackish idea is pretty original.
Note: Original inspiration was two fold. C had the best speed along with most tools. Most concurrency-analysis tools were for Java. I thought I could get safe concurrency in C for free by working within a C-based mockup of the Java model that Java's tools analyzed. Additionally, a lot of system code was done in C++ which is seemingly impossible to analyze as much as C. My concept was a C++-to-C compiler, apply all static analysis available in C, figure out what problems apply to C++ code, fix them, and repeat. Thinking on these for more languages and problems as I watched high-assurance certifications take years led to my hackish idea that's intended to replace rare experts with a pile of cheap, well-trained amateurs letting tools do most of the work.
re verification and WhyML
Whatever work I do, whether proprietary or FOSS, will be targeted in tech and price at maximizing uptake more than profit. Might be dual-licensed with intent SPARK, Frama-C, and Rust folks benefit whether building commercial stuff on it or FOSS. I noticed most build on Why3 with it having its own programming language (WhyML). I've also seen researchers working directly in WhyML to prove properties. It seems my tool should target it so both SPARK and C can use results. The correctness of assembly is still a problem with existing verified compilers being for CompCert C, C0, Simpl/C, and SML.
My next cheat of an idea is compiling WhyML programs directly to assembly. So, I ask:
(a) Do you think that's possible to begin with? I've only glanced at WhyML. Since I don't use it, I don't know if it's enough of a programming language that it could be efficiently compiled or too abstract for that.
(b) If that's possible, then have you seen any research already trying to build a WhyML-to-assembly compiler or equivalence checker?
I also always mentally retarget every assurance method I know on a new stack since high-assurance security demands we use every approach. So, when looking at this, I'm also thinking of contract-based test generation for properties expressed in Why3 on WhyML code, fuzzing the WhyML-to-x86 result with Why3 properties in as runtime checks, retargeting a static analyzer to work on it directly, and so on. If it can be verified and executed, then maybe someone can port lightweight, verification tools straight to Why3/WhyML to knock out issues before proofs or just more easily check code that would otherwise require manual proof.
Funny that you pointed to the workshop at KAIST. My colleague Johannes Kanig presented SPARK there, he's on the front row with a SPARK t-shirt. :-)
Regarding your Brute-Force Assurance Concept, it connects to the concept we're pushing at AdaCore of System to Software Integrity, in which we're looking at ways to preserve assurance from higher level descriptions at system level down to code. I must admit we're still in the early stages, exploring with customers how to go from SysML or Simulink to code in SPARK while preserving properties.
Your concept of using the best available tools is certainly attractive, if indeed they can be made to collaborate, and if the translations can be made trustworthy. That's something we're quite familiar with, as this is the bread-and-butter for tool building really. :-) One of the challenges in connecting languages and tools is that all the pieces are constantly moving. This is also what makes C so attractive as an intermediate language: it does not move.
WhyML has some advantages as an intermediate language. But note that the way we use it in our SPARK toolchain would not allow compiling through WhyML. Our translation only preserves the axiomatic semantics of the program, not its operational semantics. So we try to get equi-provability, but not an executable WhyML code.
If you start with WhyML though, you can either extract it to OCaml (see http://why3.lri.fr/doc-0.83/manual009.html) or to C (see https://hal.inria.fr/hal-01519732v2/document). One of the authors of this last paper, Raphael Rieu-Helft, is currently doing his PhD on getting this extraction to C formally proved, so that it can be used for efficient security components in WhyML. So maybe what you're looking at could be done with formally verified translation from WhyML to C and then formally verified compilation to assembly. We've also looked at having a SPARK frontend to CompCert in the past, but so far we've seen no commercial interest in that approach.
"if indeed they can be made to collaborate, and if the translations can be made trustworthy."
That is the trick. I think at the least one can, aside from using subsets close to each other, use equivalence tests that runs through all paths and key values of ranges. In high-assurance systems, one should already be using such tools given they'll catch lots of errors. So, the same tests can be re-run on the new variant in new language to see if it gives same output. This might produce reasonable, if not perfect, level of confidence. If going for semantic checks, I'm eyeballing the K Framework that was used in the C Semantics by Runtime Verification Inc. Connecting that semantics to C++, SPARK, or Rust has its own advantages. Alternatively, I work in Abstract State Machines annotated with the properties of execution that lets me then just do equivalence checks on ASM's. There's a compiler that does that.
"This is also what makes C so attractive as an intermediate language: it does not move."
That's one reason to value it. I recommend C compatibility by default these days to take advantage of ecosystem of tooling, esp compilers and verification, without performance penalties or abstraction gap failures. Although I used to recommend alternatives, the bandwagon effect showed itself to be unbeatably powerful. Some new languages getting rapid adoption are doing so partly due to seemless integration with C or otherwise legacy code. So, if I was designing SPARK-like language today, it would use C's data types and calling conventions with a compile-to-C option available from day 1. I'd possibly even build it on top of C itself with metaprogramming.
I don't like having to do such things. The momentum behind C deployment from embedded to PC to servers is just too huge. The shooting BB at freight train metaphor comes to mind. ;)
"But note that the way we use it in our SPARK toolchain would not allow compiling through WhyML."
Appreciate the tip. Means executable version of SPARK in Why might even make nice side project for some student. Thanks for the links. The Why-to-C work I submitted to Lobste.rs previously. It was great to see someone tacke GMP. I didn't know he was formally proving Why-to-C, though. If he does, your WhyML-to-C-to-assemby idea is a neat possibility. Here's one in return in case you haven't seen it that extracts Coq to C with several fold reduction in TCB. Might allow proven-C to be integrated into SPARK work or be modifiable to extract to SPARK for SPARK+Coq work.
"We've also looked at having a SPARK frontend to CompCert in the past, but so far we've seen no commercial interest in that approach."
I have a love/hate perception of CompCert: love the work, hate it went proprietary. I imagine AbsInt charges a fortune for commercial licenses. If so, that could motivate the no commercial interest part given they'd pay two companies. Have you all thought about using one of the other toolchains that's FOSS to do that stuff? Aside from CompCert, there's these: Flint's C0 used in Verisoft; Simpl with Simpl/C used for seL4; KCC's K Framework + C Semantics; CakeML. The first three would be modified for SPARK using any SPARK-to-C mapping and/or tools you already have with some portion of work, esp on low-level stuff, already done for you. Such are most practical. I'm sure you raised an eyebrow at CakeML. My idea, which a proof engineer independently came up with, was using the imperative, low-level IR's as a target for stuff verified Why3-style or certified compilers. He was using StackLang with me looking at WordLang. Either way, the starting point is an imperative language with formal semantics verified down to machine code for x86, PPC, and ARM. Again, only sensible if C-based or more SPARK-like toolchains look impractical but these IL's do somehow.
But that's not the same as having a full certified (in the sense of Coq) compiler. If we were to use a CompCert-like approach, we'd have to redo it in Coq. Not a small feat.
Regarding approaches that build safety/security by developing a language on top of C, that has been tried so many times that I don't think it can work. The use of the same syntax is deceptive, as you end up doing a lot of redesign/rewrite (as anyone who has done program proof would expect), so none of these sticked. Even those trying to enforce properties by design and runtime checking instead of proof (CCured, Cyclone). Better to stick with C then and use an appropriate toolset like Frama-C.
My hope is that I find enough feedback on good/bad of cheap or free resources on this topic that I can determine some default recommendations for people curious. The problems can be addressed with supplementary material. Eventually, the defaults would be good enough that the process would happen faster. A larger number of people centering on the same resources might become a community for helping new people. That might increase the inflow. Simultaneously, some percentage of these people are working on tools, esp automated, to make the proof process more productive. Over time, we might have a much larger segment of people working on formal verification than we do now. Maybe even large enough to sustain more tool development by contributions or licensing.
So, that's why I'm looking at books like this with what I think they might help us achieve. I'm way too out of my depth to know if it will work. I just know accessibility, better learning materials, and network effects always help.
Example tools below for sequential programs, concurrency, and hardware:
https://en.wikipedia.org/wiki/SPARK_(programming_language)
https://learntla.com/introduction/
http://prod.sandia.gov/techlib/access-control.cgi/2014/14205...