AdaCore Blog

Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.

73 entries written by Yannick Moy

by Yannick Moy

Security Agency Uses SPARK for Secure USB Key

​ANSSI, the French national security agency, has published the results of their work since 2014 on designing and implementing an open-hardware & open-source USB key that provides defense-in-depth against vulnerabilities on the USB hardware, architecture, protocol and software stack. In this project called WooKey, Ada and SPARK are key components for the security of the platform. This is a very compelling demontration of both the usability and the power of safe languages and formal verification to develop secure systems.

#SPARK    #Security    #Formal Methods   

by Yannick Moy

How Ada and SPARK Can Increase the Security of Your Software

There is a long-standing debate about which phase in the Software Development Life Cycle causes the most bugs: is it the specification phase or the coding phase? A recent study by NIST shows that, in the software industry at large, coding bugs are causing the majority of security issues. Choosing a safer language like Ada or SPARK is a critical component for reducing these vulnerabilities that result from simple mistakes. In a new freely available booklet, we explain how these languages and the associated toolsets can be used to increase the security of software.

#Ada    #SPARK    #Security   

by Yannick Moy

Two Days Dedicated to Sound Static Analysis for Security

​AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they are used to increase the security of software-based systems. The program gathers top-notch experts in the field, from industry, government agencies and research institutes, around the three themes of analysis of legacy code, use in new developments and accountable software quality. Here is why it is worth attending.

#SPARK    #Frama-C    #Security    #Formal Methods    #Static Analysis   

by Yannick Moy

Secure Software Architectures Based on Genode + SPARK

​SPARK user Alexander Senier presented recently at BOB Konferenz​ in Germany their use of SPARK for building secure mobile architectures. What's nice is that they build on the guarantees that SPARK provides at software level to create a secure software architecture based on the Genode operating system framework​. They present 3 interesting architectural designs that make it possible to build a trustworthy system out of untrustworthy building blocks. Almost as exciting as Alchemy's goal of transforming lead into gold! Here is the video of that presentation.

#SPARK    #Mobile    #Security   

by Yannick Moy

Tokeneer Fully Verified with SPARK 2014

Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran (Praxis at the time) in 2003 using the previous generation of SPARK language and tools, as part of a project commissioned by the NSA to investigate the rigorous development of critical software using formal methods. The project artefacts, including the source code, were released as open source in 2008. Tokeneer was widely recognized as a milestone in industrial formal verification. We recently transitioned this software to SPARK 2014, and it allowed us to go beyond what was possible with the previous SPARK technology. We have also shown how security vulnerabilities introduced in the code can be detected by formal verification.

#SPARK    #Formal Methods   

by Yannick Moy

For All Properties, There Exists a Proof

With the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to see the options that are available for proving it with SPARK. We present three ways to complete a proof beyond what automatic provers can do: using an alternative automatic prover, proving interactively inside our GPS IDE, and using an alternative interactive prover.

#SPARK    #Formal Methods   

by Yannick Moy, Martin Becker, Emanuel Regnath

Physical Units Pass the Generic Test

The support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue has been mostly solved for Ada in 2012 by our colleagues Ed Schonberg and Vincent Pucci who introduced special aspects for specifying physical dimensions on types. This dimension system did not attempt to deal with generics though. As was noted by others, handling generics in a dimensional analysis that is, like in GNAT, a compile-time analysis with no impact on the executable size or running time, is the source of the problem of dimension handling. Together with our partners from Technical Universitat München, we have finally solved this remaining difficulty.

#GNAT     #typing   

by Yannick Moy

Prove in the Cloud

We have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now experiment live with SPARK without installing first the toolset. Something particularly interesting for academics is that all the code for this widget is open source. So you can setup your own proof server for hands-on sessions, with your own exercises, in a matter of minutes.

#SPARK   

by Yannick Moy

SPARK Tutorial at FDL Conference

Researcher Martin Becker is giving a SPARK tutorial next week at FDL conference. This post gives a link to his tutorial material (cookbook and slides) which I found extremely interesting.

#SPARK   

by Yannick Moy

New SPARK Cheat Sheet

Our good friend Martin Becker has produced a new cheat sheet for SPARK, that you may find useful for a quick reminder on syntax that you have not used for some time.

#Formal Verification    #SPARK   

by Yannick Moy

Proving Loops Without Loop Invariants

For all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to facilitate writing loop invariants by improving the documentation and the technology in different ways, but writing loops invariants remains difficult sometimes, in particular for beginners. To completely remove the need for loop invariants in simple cases, we have implemented loop unrolling in GNATprove. It turns out it is quite powerful when applicable.

#Formal Verification    #SPARK   

by Yannick Moy

Research Corner - Focused Certification of SPARK in Coq

The SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more complex properties. But the SPARK toolset being itself a complex tool, it is not free of errors. To get confidence in its results, we have worked with academic partners to establish mathematical evidence of the correctness of a critical part of the SPARK toolset. The part on which we focused is the tagging of nodes requiring run-time checks by the frontend of the SPARK technology. This work has been accepted at SEFM 2017 conference.

#SPARK   

by Yannick Moy

Applied Formal Logic: Searching in Strings

A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of string search, and to find a previously unknown bug in a faster version of string search called quick search. Frama-C and SPARK share similar history, techniques and goals. So it was tempting to redo the same proofs on equivalent code in SPARK, and completing them with a functional proof of the fixed version of quick search. This is what I'll present in this post.

#Dev Projects    #Formal Verification    #SPARK   

by Yannick Moy

Research Corner - FLOSS Glider Software in SPARK

Two years ago, we redeveloped the code of a small quadcopter called Crazyflie in SPARK, as a proof-of-concept to show it was possible to prove absence of run-time errors (no buffer overflows, not division by zero, etc.) on such code. The researchers Martin Becker and Emanuel Regnath have raised the bar by developing the code for the autopilot of a small glider in SPARK in three months only. Their paper and slides are available, and they have released their code as FLOSS for others to use/modify/enhance!

#Formal Verification    #Dev Projects    #SPARK   

by Yannick Moy

Research Corner - Floating-Point Computations in SPARK

It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the values taken by entities in the program. Thanks to the recent changes in SPARK 17, users can now benefit from much better provability for these programs, by combining the capabilities of different provers. For the harder cases, this requires using ghost code to state intermediate assertions proved by one of the provers, to be used by others. This work is described in an article which was accepted at VSTTE 2017 conference.

#Formal Verification    #SPARK   

by Yannick Moy

Frama-C & SPARK Day Slides and Highlights

The Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with Frama-C) and for Ada programs (with SPARK). Here is a summary of what was interesting for SPARK users. We also point to the slides of the presentations.

#SPARK   

by Yannick Moy

New Guidance for Adoption of SPARK

While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on formal program verification. To help with that process, AdaCore has collaborated with Thales throughout the year 2016 to produce a 70-pages detailed guidance document for the adoption of SPARK. These guidelines are based on five levels of assurance that can be achieved on software, in increasing order of costs and benefits: Stone level (valid SPARK), Bronze level (initialization and correct data flow), Silver level (absence of run-time errors), Gold level (proof of key properties) and Platinum level (full functional correctness). These levels, and their mapping to the Development Assurance Levels (DAL) and Safety Integrity Levels (SIL) used in certification standards, were presented at the recent High Confidence Software and Systems conference.

#Formal Verification    #SPARK   

by Yannick Moy

(Many) More Low Hanging Bugs

We reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology. The two checkers we described discovered 12 issues in the codebase of the tools we develop at AdaCore. In this post, we are reporting on 6 more lightweight checkers, which have discovered 114 new issues in our codebase. This is definitely showing that these kind of checkers are worth integrating in static analysis tools, and we look forward to integrating these and more in our static analyzer CodePeer for Ada programs.

#Static Analysis    #Libadalang   

by Yannick Moy, Nicolas Roche

A Usable Copy-Paste Detector in A Few Lines of Python

After we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a copy-paste detector based on Libadalang. It turned out to be both easier than anticipated, and much more efficient and effective than we could have hoped for. In the end, we hope to use this new detector to refactor the codebase of some of our tools, and we expect to integrate it in our IDEs.

#Libadalang    #Static Analysis    #refactoring   

by Yannick Moy

VerifyThis Challenge in SPARK

This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program verification platforms to use their favorite tools on common challenges. The first challenge this year was a good fit for SPARK, as it revolves around proving properties of an imperative sorting procedure. In this post, I am using this challenge to show how one can reach different levels of software assurance with SPARK.

#Formal Verification    #SPARK   

by Yannick Moy

GNATprove Tips and Tricks: Proving the Ghost Common Divisor (GCD)

Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first algorithms that humans devised. So it's quite appealing to try to prove it with an automatic proving toolset like SPARK. It turns out that proving it automatically is not so easy, just like understanding why it works is not so easy. In this post, I am using ghost code to prove correct implementations of the GCD, starting from a naive linear search algorithm and ending with Euclid's algorithm.

#Formal Verification    #SPARK   

by Yannick Moy

Two Projects to Compute Stats on Analysis Results

Two projects by Daniel King and Martin Becker facilitate the analysis of GNATprove results by exporting the results (either from the log or from the generated JSON files) to either Excel or JSON/text.

#Dev Projects    #Open Source    #SPARK   

by Yannick Moy

Rod Chapman on Software Security

Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how difficult it is to produce secure software. Of course, it would not be Rod Chapman if he did not have also a few hints at how they have done it at Altran UK over the years. And SPARK is central to this solution, although it does not get mentioned explicitly in the talk! (although Rod lifts the cover in answering a question at the end)

#Security    #SPARK   

by Yannick Moy

Proving Tetris With SPARK in 15 Minutes

I gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the recording.

#SPARK    #FOSDEM   

by Yannick Moy

New Year's Resolution for 2017: Use SPARK, Say Goodbye to Bugs

​NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities"​ in which they single out five approaches which have the potential for creating software with 100 times fewer vulnerabilities than we do today. One of these approaches is formal methods. Among formal methods, the report highlights strong suits of SPARK, and cites SPARK projects as example of mature uses of formal methods. NIST is not the only ones to support the use of SPARK. Editor Bill Wong from Electronic Design has included SPARK in his "2016 Gifts for the Techie". So if your new year's resolutions include software without bugs, have a look at SPARK in 2017.

#VerificationTools    #Formal Methods    #SPARK   

by Yannick Moy

SPARK Cheat Sheets (en & jp)

The SPARK cheat sheet usually distributed in trainings has recently been translated to Japanese. Here they are, both in English and in Japanese. My modest Xmas present.

#SPARK   

by Yannick Moy

GNATprove Tips and Tricks: What’s Provable for Real Now?

One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). Since then, we have integrated static analysis in SPARK, and modified completely the way floating-point numbers are seen by SMT provers. Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations.

#Formal Verification    #SPARK   

by Yannick Moy

Research Corner - SPARK on Lunar IceCube Micro Satellite

Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar IceCube that will map water vapor and ice on the moon. In their paper, they explain how the use of proof with SPARK is going to help them get perfect software in the time and budget available.

#SPARK   

by Yannick Moy

Verified, Trustworthy Code with SPARK and Frama-C

Last week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified, trustworthy code - formal verification of software". Attendees from many different branches of Thales (avionics, railway, security, networks) were given an overview of the state-of-practice in formal verification of software, focused on two technologies: the SPARK technology that we develop at AdaCore for programs in Ada, and the Frama-C technology developed at CEA research labs for programs in C. The most interesting part of the day was the feedback given by three operational teams who have experimented during a few months with either SPARK (two teams) or Frama-C (one team). The lessons learned by first-time adopters of such technologies are quite valuable.

#SPARK    #Formal Methods   

by Yannick Moy

The Most Obscure Arithmetic Run-Time Error Contest

Something that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course, everyone knows about overflow checks and range checks (although many people confuse them) and division by zero. After all, these are typical errors that do show up in programs, so programmers are aware that they should keep an eye on these. Or do they?

#Formal Verification    #SPARK   

by Yannick Moy

Research Corner - SPARK 2014 vs Frama-C vs Why3

Ready for a bloody comparison between technologies underlying the tools for SPARK 2014 vs Frama-C vs Why3? Nothing like that in that article we wrote with developers of the Why3 and Frama-C toolsets. In fact, it's a bloody good comparison really, that emphasizes the differences and benefits in each technology.

#Formal Verification    #SPARK   

by Yannick Moy

Research Corner - Proving Security of Binary Programs with SPARK

Researchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on proving security of binary programs. In this work, they use SPARK as intermediate language and GNATprove as proof tool, which is an atypical and interesting use of the SPARK technology.

#Formal Verification    #SPARK    #Security   

by Yannick Moy

GNATprove Tips and Tricks: Using the Lemma Library

A well-know result of computing theory is that the theory of arithmetic is undecidable. This has practical consequences in automatic proof of programs which manipulate numbers. The provers that we use in SPARK have a good support for addition and subtraction, but much weaker support for multiplication and division. This means that as soon as the program has multiplications and divisions, it is likely that some checks won't be proved automatically. Until recently, the only way forward was either to complete the proof using an interactive prover (like Coq or Isabelle/HOL) or to justify manually the message about an unproved check. There is now a better way to prove automatically such checks, using the recent SPARK lemma library.

#Formal Verification    #SPARK   

by Yannick Moy

Did SPARK 2014 Rethink Formal Methods?

David Parnas is a well-known researcher in formal methods, who famously contributed to the analysis of the shut-down software for the Darlington nuclear power plant and designed the specification method known as Parnas tables and the development method called Software Cost Reduction. In 2010, the magazine CACM asked him to identify what was preventing more widespread adoption of formal methods in industry, and in this article on Really Rethinking Formal Methods he listed 17 areas that needed rethinking. The same year, we started a project to recreate SPARK with new ideas and new technology, which lead to SPARK 2014 as it is today. Parnas's article influenced some critical design decisions. Six years later, it's interesting to see how the choices we made in SPARK 2014 address (or not) Parnas's concerns.

#Formal Verification    #SPARK   

by Yannick Moy

Formal Verification of Legacy Code

Just a few weeks ago, one of our partners reported a strange behavior of the well-known function Ada.Text_IO.Get_Line, which reads a line of text from an input file. When the last line of the file was of a specific length like 499 or 500 or 1000, and not terminated with a newline character, then Get_Line raised an exception End_Error instead of returning the expected string. That was puzzling for a central piece of code known to have worked for the past 10 years! But fair enough, there was indeed a bug in the interaction between subprograms in this code, in boundary cases having to do with the size of an intermediate buffer. My colleague Ed Schonberg who fixed the code of Get_Line had nonetheless the intuition that this particular event, finding such a bug in an otherwise trusted legacy piece of code, deserved a more in depth investigation to ensure no other bugs were hiding. So he challenged the SPARK team at AdaCore in checking the correctness of the patched version. He did well, as in the process we uncovered 3 more bugs.

#SPARK    #Legacy    #Formal Methods   

by Yannick Moy

SPARK Prez at New Conference on Railway Systems

RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write abstract software specifications, whose refinement in terms of concrete implementation can be proved automatically using SPARK tools.

#SPARK   

by Yannick Moy, Jamie Ayre, Emma Adby

Ada Lovelace Bicentennial

The three of us attended the Ada Lovelace Symposium in Oxford (UK). The two days were one fantastic discovery after another about the life, achievements and legacy of Ada Lovelace, the programming pioneer who lent her name to the Ada language.

#Lovelace   

by Yannick Moy

GNATprove Tips and Tricks: What’s Provable for Real?

SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known fixed-point reals, called this way because their precision is fixed (contrary to floating-points whose precision varies with the magnitude of the encoded number). This support is limited in some ways when it comes to proving properties of computations on real numbers, and these limitations depend strongly in the encoding chosen. In this post, I show the results of applying GNATprove on simple programs using either floating-point or fixed-point reals, to explain these differences.

#Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Support for Ravenscar

As presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in the Ravenscar profile of Ada. This profile restricts concurrency so that concurrent programs are deterministic and schedulable. SPARK analysis makes it possible to prove that shared data is protected against data races, that deadlocks cannot occur and that no other run-time errors related to concurrency can be encountered when running the program. In this post, I revisit the example given by Pavlos to show SPARK features and GNATprove analysis in action.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

GNATprove Tips and Tricks: User Profiles

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users.

#Formal Verification    #SPARK   

by Yannick Moy

The Eight Reasons For Using SPARK

Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do.

#Formal Verification    #Design Method    #Certification    #SPARK   

by Yannick Moy

New Book About SPARK 2014

I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying!

#SPARK    #Formal Methods    #Teaching   

by Yannick Moy

SPARK 2014 Rationale: Type Predicates

Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARKSkein: From tour-de-force to run-of-the-mill Formal Verification

In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous version of the SPARK technology. We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants.

#Dev Projects    #Formal Verification    #SPARK   

by Yannick Moy

How Our Compiler Learnt From Our Analyzers

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.

#Compilation    #Formal Verification    #SPARK   

by Yannick Moy

A Building Code for Building Code

In a recent article in Communications of the ACM, Carl Landwehr, a renowned scientific expert on security, defends the view that the software engineering community is doing overall a poor job at securing our global information system and that this is mostly avoidable by putting what we know works to work, to the point that most vulnerabilities could be completely avoided by design if we cared enough. Shocking! Or so it should appear.

#Ada    #SPARK    #Static Analysis    #Security   

by Yannick Moy

GNATprove Tips and Tricks: Minimizing Rework

As automatic proof is time consuming, it is important that rework following a change in source code is minimized. GNATprove uses a combination of techniques to ensure that, both for a single user, and when working in a team.

#Formal Verification    #SPARK   

by Yannick Moy

AdaCore Tech Days Prez on SPARK

Hristian Kirtchev, who leads the developments of the GNAT compiler frontend, gave a very clear presentation of SPARK at the last AdaCore Tech Days in Boston. This was recorded, here is the video.

by Yannick Moy

GNATprove Tips and Tricks: Catching Mistakes in Contracts

Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by pinpointing suspicious constructs that, although legal, do not make much sense. These constructs are likely to be caused by mistakes made by the programmer when writing the contract. In this post, I show examples of incorrect constructs that are signaled by GNATprove.

#Formal Verification    #Compilation    #SPARK   

by Yannick Moy

GNATprove Tips and Tricks: Keeping Justifications Up-To-Date

GNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications may become obsolete across time. To help with that, GNATprove now issues a warning on useless justifications.

#Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Functional Update

While attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently express how record and array objects are modified by a procedure. A special attribute Update is defined in SPARK to make it easy to express such properties.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Object Oriented Programming

Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known statically. The standard for civil avionics certification has recognized this specific problem, and defines a specific verification objective called Local Type Consistency that should be met with one of three strategies. SPARK allows using one of these strategies, by defining the behavior of an overridden subprogram using a special class-wide contract and checking that the behavior of the overriding subprogram is a suitable substitution, following the Liskov Substitution Principle.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Ghost Code

A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the original program. If you're careful or lucky enough, the additional code you write will not impact the program being verified, and it will be removed during compilation, so that it does not inflate binary size or waste execution cycles. SPARK provides a way to get these benefits automatically, by marking the corresponding code as ghost code, using the new Ghost aspect.

#Formal Verification    #SPARK   

by Yannick Moy

Using Coq to Verify SPARK 2014 Code

In the first release of SPARK 2014, GNATprove only provided support for automatic provers, in particular Alt-Ergo. Automatic provers are very handy when it comes to perform a big numberof simple proof. But they can fail to prove valid formulas when the proof involves some advanced reasoning. As mentioned in a previous post, one check left unproved might invalidate assumptions on which are based the proofs of multiple other checks. This is a case where manual proof may be useful for SPARK 2014 users. The development version of GNATprove now supports Coq to perform manual proof.

#Formal Verification    #SPARK   

by Yannick Moy

Using SPARK to Prove AoRTE in Robot Navigation Software

Correctness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that even NASA has not solved it. Researchers have used SPARK to do precisely that for 3 well-known robot navigation algorithms. Their results will be presented at the major robotics conference IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2014) this coming September.

#Formal Verification    #SPARK    #Robotics   

by Yannick Moy

Short Video Demo of SPARK 2014

New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!

#Formal Verification    #Language    #SPARK   

by Yannick Moy

Use of SPARK in a Certification Context

Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.

#Formal Verification    #Certification   

by Yannick Moy

Contextual Analysis of Subprograms Without Contracts

We have implemented a new feature in GNATprove for analyzing local subprograms in the context of their calls. This makes it possible to benefit from the most precise analysis for local subprograms, without incurring the cost of adding contracts to these subprograms.

#Formal Verification    #SPARK   

by Yannick Moy

Studies of Contracts in Practice

Two recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts (Eiffel obviously, Java with JML contracts and C# with Code Contracts). I'm reporting what I found interesting (and less so) in these two studies.

#Language    #Formal Verification    #Contracts   

by Yannick Moy

GNATprove Tips and Tricks: How to Write Loop Invariants

Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants are necessary for various loops, we detail here a methodology for how users can come up with the right loop invariants for their loops. This methodology in four steps allows users to progressively add the necessary information in their loop invariants, with the tool GNATprove providing the required feedback at each step on whether the information provided is sufficient or not.

#Formal Verification    #SPARK   

by Yannick Moy

Case Study for System to Software Integrity Includes SPARK 2014

My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.

#Formal Verification    #Certification    #SPARK   

by Yannick Moy

Muen Separation Kernel Written in SPARK

The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been proved free from run-time errors. This project is part of the secure multilevel workstation project by Secunet, a German security company, which is using SPARK and Isabelle to create the next generation of secure workstations providing different levels of security to government employees and military personnel. I present why I think this project is worth following closely.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

Rail, Space, Security: Three Case Studies for SPARK 2014

We will present three case studies using SPARK 2014 at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February 2014, in three different domains: rail, space and security. The lessons learned in those three case studies are particularly interesting. Here is the companion paper that we wrote.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

GNATprove Tips and Tricks: Referring to Input in Contracts

In a previous post about pre-call values, I described how the Ada language rules implemented in the compiler prevent surprises when referring to input values in the postcondition, using the Old attribute. Unfortunately, these rules also make it difficult to express some complex postconditions that may be useful when doing formal verification. In this post, I describe how contract cases allow the expression of these complex contracts, while still detecting potential problems with uses of the Old attribute.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Global State

Global variables are a common source of programming errors: they may fail to be initialized properly, they can be modified in unexpected ways, sequences of modifications may be illegal, etc. SPARK 2014 provides a way to define abstractly the global state of a unit, so that it can be referred to in subprogram specifications. The associated toolset checks correct access to global variables in the implementation.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Mixing SPARK and Ada Code

The first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification within the overall Ada application. This post presents the solution we've come up with for SPARK 2014.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Loop Variants

Loop variants are the little-known cousins of the loop invariants, used for proving termination of subprograms. Although they may not look very useful at first, they can prove effective as I show with a simple binary search example. And we came up with both an elegant syntax and a slick refinement for loop variants in SPARK 2014, compared to similar constructs in other languages.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Loop Invariants

Formal verification tools like GNATprove rely on two main inputs from programmers: subprogram contracts (preconditions and postconditions) and loop invariants. While the first ones are easy to understand (based on the "contract" analogy, in which a subprogram and its caller have mutual obligations), the second ones are not so simple to grasp. This post presents loop invariants and the choices we made in SPARK 2014.

#Language    #Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Pre-call and Pre-loop Values

Subprogram contracts are commonly presented as special assertions: the precondition is an assertion checked at subprogram entry, while the postcondition is an assertion checked at subprogram exit. A subtlety not covered by this simplified presentation is that postconditions are really two-state assertions: they assert properties over values at subprogram exit and values at subprogram entry. A special attribute Old is defined in Ada 2012 to support these special assertions. A special attribute Loop_Entry is defined in SPARK 2014 to support similar special assertions for loops.

#Formal Verification    #SPARK   

by Yannick Moy

MISRA-C 2012 vs SPARK 2014, the Subset Matching Game

The MISRA C subset of C defines around 150 rules that restrict C programs for critical software development. Of these, 27 rules are classified as undecidable, which means that few MISRA C checkers (if any) will help checking those hardest rules. Here is how SPARK 2014 can help checking similar rules in Ada programs.

#Formal Verification    #SPARK    #MISRA-C   

by Yannick Moy

SPARK 2014 Rationale: Specification Functions

Specifying a program's behavior is seldom expressible in a satisfiable way without the capability of abstraction provided by function calls. Yet, specification functions must obey specific constraints like absence of side-effects and termination, that have led to different solutions in various specification languages. Here is what we did in SPARK 2014.

#Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Contract Cases

Besides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a contract by cases. A little history helps understanding how we came up with this new feature.

#Formal Verification    #SPARK   

by Yannick Moy

Project Hi-Lite Wrap-up

After three years of hard work, we have reached last week the end of project Hi-Lite, whose goal was to simplify the use of formal methods. We're proud to publicize the results obtained, in particular the new version of SPARK and the associated tool GNATprove. Here's a summary of the wrap-up meeting.

#Formal Verification    #SPARK