Category Archives: Open Source

Muen Separation Kernel

By Jamie Ayre | December 10, 2013

The Institute for Internet Technologies and Applications at the University of Applied Science in Rapperswil (Switzerland) and AdaCore today announced a significant expansion of the Open Source software model into the domain of high-assurance systems with the preview release of the Muen Separation Kernel. The Muen Kernel enforces a strict and robust isolation of components to shield security-critical functions from vulnerable software running on the same physical system. To achieve the necessary level of trustworthiness, the Muen team used the SPARK language and toolset to formally prove the absence of run-time errors.


More info.
Also posted in Related Initiatives | Leave a comment

Trusted Key Manager for IKEv2

By Jamie Ayre | October 23, 2013

The HSR University of Applied Sciences in Switzerland has implemented the TKM from scratch using the Ada programming language. The new Design-by-Contract feature of Ada 2012 has been used for the implementation of state machines, to augment the confidence of operation according to the specification. The TKM works in conjunction with the strongSwan IKEv2 daemon to provide key management services for IPsec.

Read the project report http://www.codelabs.ch/tkm/ike-separation.pdf
Visit the TKM project page http://www.codelabs.ch/tkm/
Visit the strongSwan project page http://www.strongswan.org/
Posted in Open Source | Leave a comment

Axioms and Proofs: When Less is More

By Yannick Moy | February 15, 2013

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

Future Version of SPARK Will Be Based on Ada 2012

By Yannick Moy | November 30, 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.

Also posted in Events | Tagged , , | Leave a comment

ESA is Funding Students on Open-Source Projects this Summer

By Yannick Moy | June 29, 2012

The European Space Agency is reediting its SOCIS initiative this year. Open-source projects can submit proposals, and ESA will fund between 20 and 25 students to work during two months on these projects.

We submitted a project to extend our work on standard containers adapted to formal verification. Submit yours by July 15th!

Also posted in Related Initiatives | Leave a comment

Formalization and Comparison of MCDC and Object Branch Coverage Criteria

By Jamie Ayre | March 19, 2012

This paper was presented by Jerome Guitton at the recent ERTS 2012 conference:
This paper presents formal results derived from the COUVERTURE project, whose goal was to develop tools to support structural coverage analysis of unin- strumented safety-critical software. After briefly introducing the project context and explaining the need for formal foundations, we focus on the relationships between machine branch coverage and the DO-178B Modified Condition/Decision Coverage (MCDC) criterion. A thorough understanding of those relationships is important, since it provides the foundation for knowing where efficient execution trace techniques can be used to demonstrate compliance with the MCDC criterion. We first present several conjectures that were tested using Alloy models, then provide a formally verified characterization of the situations when coverage of object control-flow edges implies MCDC compliance.The full paper can de downloaded here.

Couverture erts2012
View more presentations from AdaCore

Also posted in Certification, Open-DO News, Papers and Slides | Leave a comment

Integrating Formal Program Verification with Testing

By Jamie Ayre | March 19, 2012

This is the paper that Yannick Moy presented at the recent ERTS 2012 conference:
Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software. They are becoming increasingly costly as, over time, they require the development and maintenance of a large body of functional and robustness tests on larger and more complex applications. Formal program verification offers a way to reduce these costs while providing stronger guarantees than testing. Addressing verification activities with formal verification is supported by upcoming standards such as do-178c for software development in avionics. In the Hi-Lite project, we pursue the integration of formal verification with testing for projects developed in C or Ada. In this paper, we discuss the conditions under which this integration is at least as strong as testing alone. We describe associated costs and benefits, using a simple banking database application as a case study. The full paper can de downloaded here.

Hi-Lite erts2012
View more PowerPoint from AdaCore

Also posted in Certification, Events, Open-DO News, Papers and Slides | Tagged , , , , | Leave a comment

Nose Gear Challenge Problem joins Open-DO

By Jamie Ayre | February 12, 2012

The Nose Gear Challenge Problem has joined the Open-DO forge. It was initially developed to stimulate and unify discussions at the 2nd Workshop on Theorem Proving in Certification held on December 5 – 6, 2011 in Cambridge, UK. The goal of this project is to consider how/if theorem proving can have any value in providing assurance in the context of DO-178C formal method supplement. The contributors to the project can use the Nose Gear problem example to explain their techniques.

Visit the Nose Gear Challenge Problem project page on the Open-DO forge.

Also posted in Certification, Related Initiatives | 1 Comment

code.NASA

By Jamie Ayre | January 5, 2012

An interesting new website added to the family of NASA websites. code.NASA, according the website, NASA “…will continue, unify, and expand NASA’s open source activities. The site will serve to surface existing projects, provide a forum for discussing projects and processes, and guide internal and external groups in open development, release, and contribution.”

More information can be found at:

http://open.nasa.gov/blog/2012/01/04/the-plan-for-code/

I particularly like the call for participation – “Will your code someday escape our solar system or land on an alien planet? We’re working to make it happen, and with your help, it will.”

Also posted in In the Press, Open-DO News, Related Initiatives | Leave a comment

Non-intrusive Code Coverage

By Jamie Ayre | November 16, 2011

In his recent Embedded Computing Design article, Ben Brosgol discusses “Non-intrusive code coverage for safety-critical software” and more specifically how a “tool that derives precise source-level coverage metrics from execution trace data for a non-instrumented program” can really help with DO-178B evidence requirements. Abstract below with a link to the the full article…

Certification standards such as DO-178B for avionics require evidence that the system source code is completely exercised by tests derived from requirements. Traditional tools obtain the coverage data for a test run through code instrumentation, but this complicates analysis since the code being exercised is not the code that will finally execute. A solution to this problem is provided by a combination of two new tools, one for target emulation and one for coverage analysis. GNATemulator translates target object code into native host instructions, with the resulting code running on the host. This approach is efficient (target code is not being interpreted dynamically) and convenient (a significant amount of development can be conducted without an actual target board). Running on an instrumented version of GNATemulator, the GNATcoverage tool non-intrusively provides coverage data at both the source and object levels. At the object code level the tool performs instruction and branch coverage. At the source code level it provides statement coverage, decision coverage, and Modified Condition/Decision Coverage (MC/DC), performing the necessary analysis when MC/DC cannot be deduced from object branch coverage, and fully supports all levels of DO-178B safety certification.

http://embedded-computing.com/non-intrusive-code-coverage-safety-critical-software

Also posted in Agile/Lean Programming, Certification, In the Press | 1 Comment

  • Categories

  • Open-DO Projects

    Agile
    Couverture
    GeneAuto/Ada
    HiberSource
    Hi-Lite
    Project P
    The Qualifying Machine
    Sparkel
    XReq

  • Contact

    info @ open-do.org