4 ms·

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 c

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: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) https://learntla.com/introduction/ https://learntla.com/introduction/ http://prod.sandia.gov/techlib/access-control.cgi/2014/1420533.pdf http://prod.sandia.gov/techlib/access-control.cgi/2014/14205...

yannickmoy 9y ago
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: https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf https://github.com/fraunhoferfokus/acsl-by-example/blob/mast... This has inspired other researchers to do the same for SPARK, but currently they have done only the code/proofs, not yet the doc around it: https://github.com/yoogx/spark_examples/tree/master/spark-by-example https://github.com/yoogx/spark_examples/tree/master/spark-by... As I like that approach a lot, that's something I have adopted for the static analysis tools we develop around Ada and SPARK: http://docs.adacore.com/codepeer-docs/users_guide/_build/html/codepeer_by_example.html http://docs.adacore.com/codepeer-docs/users_guide/_build/htm... https://docs.adacore.com/spark2014-docs/html/ug/en/source/gnatprove_by_example.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/gn... This shares with the O'Reilly Cookbook series (https://ssearch.oreilly.com/?q=cookbook 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.
- nickpsecurity 9y ago
  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. https://lobste.rs/newest/nickpsecurity https://lobste.rs/newest/nickpsecurity 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. https://hal.archives-ouvertes.fr/hal-01681134/document https://hal.archives-ouvertes.fr/hal-01681134/document 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. https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf re your concrete examples 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. http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html 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. https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spark-gpl-editions.html https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spa... So, I gotta get SPARK working on my machine before trying to learn it. Sucks that it's been this difficult. I'll try again later this week.

yannickmoy 9y ago

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: https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf https://github.com/fraunhoferfokus/acsl-by-example/blob/mast... This has inspired other researchers to do the same for SPARK, but currently they have done only the code/proofs, not yet the doc around it: https://github.com/yoogx/spark_examples/tree/master/spark-by-example https://github.com/yoogx/spark_examples/tree/master/spark-by... As I like that approach a lot, that's something I have adopted for the static analysis tools we develop around Ada and SPARK: http://docs.adacore.com/codepeer-docs/users_guide/_build/html/codepeer_by_example.html http://docs.adacore.com/codepeer-docs/users_guide/_build/htm... https://docs.adacore.com/spark2014-docs/html/ug/en/source/gnatprove_by_example.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/gn... This shares with the O'Reilly Cookbook series (https://ssearch.oreilly.com/?q=cookbook 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.

nickpsecurity 9y ago
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. https://lobste.rs/newest/nickpsecurity https://lobste.rs/newest/nickpsecurity 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. https://hal.archives-ouvertes.fr/hal-01681134/document https://hal.archives-ouvertes.fr/hal-01681134/document 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. https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf https://www.cs.dartmouth.edu/~trdata/reports/TR2004-526.pdf re your concrete examples 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. http://infohost.nmt.edu/~al/cseet-paper.html http://infohost.nmt.edu/~al/cseet-paper.html 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. https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spark-gpl-editions.html https://bluishcoder.co.nz/2017/04/27/installing-gnat-and-spa... So, I gotta get SPARK working on my machine before trying to learn it. Sucks that it's been this difficult. I'll try again later this week.