SPARK 2014 – Future directions

Stuart Mathews gave this talk at the recent SPARK User Group. In it he presents the next generation of the SPARK language which will extend the range of programs that can be automatically verified and provides an innovative means for combing formal verification and testing.

Posted in Open-DO News | Leave a comment

Directions in Secure Software Development

Rod Chapman, Altran Praxis, gave this talk at the recent SPARK User Group. This talk reflected on our experiences with building secure systems with SPARK and other formal methods, including the lessons learned from the MULTOS CA, Tokeneer and SPARKSkein projects, and the relationship between safety- and security-critical development. In recent years, there has been a huge resurgence in interest in static analysis of software, largely driven by the perception of “security vulnerabilities” in both specific systems and programming languages in general. This talk also considered the trends emerging in this market, both good and bad, and proposed one view of what the future might hold for secure systems development.

Posted in Open-DO News | Leave a comment

Axioms and Proofs: When Less is More

In formal verification, we ultimately rely on automatic provers to decide whether formulas are valid (always true) or not. In GNATprove for example, we rely mostly on the ability of prover Alt-Ergo to analyze quickly the formulas we generate, and answer yes when the formula is valid or no when the formula is invalid (so there is a problem with the code or the assertions in the program). The reality is that the prover may take a long time to reply yes/no, and that in some cases it just replies I don’t know!

A promising approach to help automatic provers answer more quickly is to reduce the size of the formula. Typically, this formula contains thousands of axioms defining all relevant symbols from the program (functions, types, constants), as well as describing the context in which the formula should hold (typically a path or set of paths through a function, as produced by a verification condition generator). Researchers have proposed strategies to start with a small subset of these axioms, and incrementally grow it until a proof is found. At AdaCore, Duc Hoang is ending today a 6 months internship on that subject.

We have devised a strategy based on definition links, as in the work of Josef Urban (”An overview of methods for large-theory automated theorem proving”) and SInE, with a graph-based approach, similar to the work of Couchot et al. (”A graph-based strategy for the selection of hypotheses” & “Graph Based Reduction of Program Verification Conditions”).

This work is publicly available, if others want to try it out (main switch is -autoselect), in the git repository for our version of Alt-Ergo:

git clone https://forge.open-do.org/anonscm/git/alt-ergo/alt-ergo.git

We had a discussion a few days ago on this subject and others related to Alt-Ergo with CEA-LIST research lab and OCamlPro company, both interested in a shared development of Alt-Ergo. If you are also interested in joining this effort, contact us at AdaCore.

Posted in Open Source | Tagged , , | Leave a comment

not Taking Assumptions for Granted

The Merriam-Webster dictionnary defines an assumption as “a fact or statement (as a proposition, axiom, postulate, or notion) taken for granted”. This is indeed the role that assumptions play in formal verification of programs, as performed in Frama-C platform or GNATprove. Assumptions may either be related to the proof of a single function (like “this other function called should respect its contract”) or related to the proof methodology and tools used (like “the type system of the program should not be bypassed”). The problem is that the overall verification of a software, as done in certification, should ultimately discharge such assumptions, either by some other automatic verification activity, or by manual review. Because assumptions are not taken for granted in software certification.

Researchers have started taking assumptions seriously, in particular for certification. See for example this paper at FM 2012, and the paper “Tool Integration with the Evidential Tool Bus” (or ETB) from SRI. The Frama-C platform already has a built-in mechanism for storing the assumptions on which individual proofs of properties depend (see their paper “Combining Analyses for C Program Verification”). The SPARK technology also provides a way to summarize how all properties of interest were checked, inclusing manual review, so that there are no pending assumptions besides the implicit ones depending on the approach.

What we have been discussing last Monday with Simon Cruanes (a coauthor of the SRI paper above) and Frama-C team members Julien Signoles and Virgile Prevosto, is how to combine verification results from different tools (some doing formal verification, some doing dynamic verification like testing) on different languages (Ada and C) in a way that no assumption is forgotten. The Datalog language used to express constraints in the ETB seems a good start. We are now going to experiment with the ETB and its Datalog language to see if that allows us to express and check the verification constraints mandated by various certification standards, for our tools.

Note that the CEA will host soon Maria Christakis (a coauthor of the FM 2012 paper above) and SRI researchers Natarajan Shankar and Sam Owre, which whom we’ll discuss this topic. To be continued.

Posted in Certification | Tagged , , , | Leave a comment

DO-330/ED-215 Benefits of the New Tool Qualification Document

As part of the DO-178C/ED-12C revision effort, a new document Software Tools Qualification Considerations (DO-330/ED-215) was developed. Its goal is both to replace the software tool qualification guidance of DO-178B/ED-12B and also to enable and encourage the use of this “mature” guidance outside the airborne domain. Since it may be used independently, DO-330/ED-215 is not considered as a supplement to DO-178C/ED-12C; it is thus titled differently from the specialized technology supplements.

The purpose of this document is to describe how DO-330/ED-215 impacts the current tool qualification approach of DO-178B/ED-12B and how it provides more relevant guidance for both tool users and tool providers.

We first review the rationale for a Tool Qualification document. But before the application of DO-330/ED-215, a fundamental pre-condition is to establish for the project the tool qualification criteria and the Tool Qualification Levels (TQLs). As an example, we show how DO-178C/ED-12C determines the criteria and TQLs for the airborne domain. In this domain, the criteria are based on the possible impact of a tool error on the software life cycle processes.

We then highlight the main impact of DO-330/ED-215 on current practice, and provide the relevant information to help the reader to apply this new guidance.

Some supporting information is provided in an appendix of DO-330/ED-215. We describe one of the most important topics, addressing the possible certification credit when using a qualified AutoCode Generator (ACG).

The author, Frédéric Pothon ACG Solutions, and several of the contributors and reviewers participated in the DO-178C/ED-12C working group and subcommittees.

Download document.

© Frédéric Pothon, 2012
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License.

Posted in Open-DO News | Leave a comment

Future Version of SPARK Will Be Based on Ada 2012

At the SPARK User Day yesterday in Bath, Altran-Praxis and AdaCore announced that the SPARK language will undergo a major transformation, to both extend the subset of Ada included in SPARK, and to use the new specification features of Ada 2012 instead of special comments like in today’s SPARK language. This is only fair that, SPARK annotations being the source of inspiration for many of the new specification features in Ada (pre- and postconditions, quantified expressions, etc.), their executable Ada version is now included in SPARK. This future version is expected to be released Q1 2014.

This is something we have been working on for almost 3 years now, between Altran-Praxis and AdaCore, inside the Hi-Lite project. We have been able to show that, not only we can extend the range of programs which can be proved automatically correct with respect to their specification, but we can combine much more easily testing and formal verification than what was considered possible until now.

Given the results achieved already, some (like the Microsoft researcher Rustan Leino who asked me this question at the SPARK User Day) could wonder why we don’t plan to release a product sooner. This was answered by a current SPARK customer, Robert Dorn from Secunet, who said that they want “first, that the future SPARK language and toolset allows them to express and prove as much as the existing one, and only then, that it extends the language and provides improved and new tools”. The work done in Hi-Lite is mostly concerned with automatic proof of functional properties. We are now working also on the expression and verification of data and information flow properties that are so important for many SPARK users.

We will continue to provide GPL releases of prototypes of these future tools to the community in 2013.

Posted in Events, Open Source | Tagged , , | Leave a comment

DO-178C/ED-12C vs DO-178B/ED-12B: Changes and Improvements

This document identifies all the changes in the new release DO-178C/ED-12C, explains their rationale, and highlights the impact of these changes on the various software processes. The PDF can be downloaded here.

© Frédéric Pothon, 2012
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License.

Posted in Certification, Papers and Slides | Leave a comment

Use of formal methods in critical systems conference

This conference will take place in Toulouse on November the 12th. It is in French as is the announcement providing more details below:

Les animateurs du DAS Systèmes Embarqués, avec le soutien du thème IFSE du RTRA AE/SE, ont le plaisir de vous annoncer la programmation d’un cycle de conférences techniques sur les méthodes formelles de développement. Non, ne partez pas tout de suite : les méthodes formelles sont faites pour vous !

Ces méthodes ne sont pas assez connues mais ont un potentiel énorme pour faire progresser la productivité ET la qualité intrinsèque des développements de logiciels embarqués et de leurs outils de développement et de vérification. Et elles ne sont pas si difficiles à mettre en œuvre : certains l’ont déjà fait, avec succès, pourquoi pas vous ?

Nous vous proposons donc un cycle de conférence/forum pour vous présenter bien sûr les fondements théoriques de ces méthodes, mais surtout faire un état de l’art et de la pratique, démystifier, échanger, et pourquoi pas monter ensemble des projets pour “passer à l’acte” ? Les intervenants seront à la fois des scientifiques et universitaires les plus compétents dans ces domaines et des utilisateurs “de terrain” qui ont déjà pratiqué ces méthodes et vous livreront leurs retours d’expérience.

La première conférence de ce cycle aura lieu le mardi 13 Novembre 2012 à l’IAS, 23 Avenue Edouard Belin, Toulouse, sur le thème de “l’Utilisation des méthodes formelles dans les systèmes critiques”.

Read More »
Posted in Certification, Events | Tagged , , | Leave a comment

GNATprove Distinguished at VerifyThis Competition

I participated last week in the VerifyThis Verification Competition, which took place on Thursday afternoon during the Formal Methods 2012 conference in Paris. The goal was to apply verification tools to three small challenge programs, to compare approaches and learn from each other’s tools.

I used Ada 2012 as a programming and specification language (using preconditions and postconditions to specify contracts for subprograms) and our prototype GNATprove, a proof tool developed in project Hi-Lite, to formal verify that the code implements its contract and does not raise run-time errors (integer overflows, array index out of bounds, etc.) I completed challenge 1 and I did a part of challenge 2, but I had not enough time to complete it or start on challenge 3.

The competition was followed on Friday by a very interesting explanation session where each team showed how it addressed the problems with its tools. It was particularly interesting to see different solutions from teams using the same language (for example, the two teams using Why3 had quite different solutions for challenge 2), as well as the interaction between the user and the proof tool in KIV, KeY, Why3, etc. I think the problems and their solutions will be added soon to the VerifyThis repository, but if you cannot wait, you can also ask the organizers for a tarball of the submissions.

To come to the title of this post, the organizers awarded a distinction to GNATprove for its integration of proving and run-time assertion checking, of which I’m very proud. As I explained them, this integration was essential in helping me during the competition:

  • For the first problem, I was stuck with a postcondition that I could not prove, and I did not manage to figure out why. So I decided to write a small test to make sure at least that the code and the contract were not contradictory. I executed it, and it raised an exception saying the postcondition was wrong! (because Ada 2012 contracts are executable, the compiler can transform them into run-time assertions, including quantifiers that are transformed in loops) It was then easy to pinpoint the root cause of the problem, the use of “<" instead of "<=" in the test of the main loop.
  • For the second problem, I decided to implement the iterative version of the algorithm, which is more complex to specifiy and verify than the recursive one, but also more representative of critical embedded software. The algorithm is divided in two passes, each one performing two nested loops on the input array, with loop invariants to write for the proof to go through. Being able to execute these loop invariants as regular assertions made me quite confident that I had not written wrong assertions, before I even start proving something.

Hope to see even more participants at the next software verification competition, either VSTTE’s one or VerifyThis!

Posted in Events | Tagged , , , , | 1 Comment

GNATprove tool available

We are happy to announce the first release of GNATprove. This tool is used for formal verification of Ada programs and is being developed as part of the Hi-Lite project. We provide binary distributions for x86 linux, x86 windows and x86-64 bit linux. More details can be found on the following page:

http://www.open-do.org/projects/hi-lite/gnatprove/

For questions, remarks, or issues please contact us on hi-lite-discuss@lists.forge.open-do.org

Posted in Related Initiatives | 5 Comments
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org