49 entries tagged with #Testing
Every year the GNAT Pro product family acquires new members and capabilities, to help our customers develop safer, more secure and more efficient code on newer hardware and software platforms. Moving forward, our goal is to offer a clear view on the future development of our technology. As part of this effort, we have made available a public roadmap for AdaCore products on our documentation platform.
This week we announced a new tool called RecordFlux. The goal of RecordFlux is to address one of the most critical parts of the software stack in terms of security, binary protocol parsers/serializers.From a protocol specification written in the RecordFlux Domain Specific Language (DSL), the tool can generate provable SPARK code. This means memory safety (no buffer overruns), absence of integer overflow errors, and even proof of functional properties. In this blog post I will try to explain how this is a game changer for cybersecurity.
This blog describes the concept and benefits of differential fuzz testing. In addition, the post describes setting up, executing and analyzing the results of a differential fuzzing campaign for the Libkeccak and XKCP cryptographic libraries.
Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser for the case study that NVIDIA and AdaCore published today. Our journey begins with the NVIDIA Security Team. Like many other security oriented teams in our industry today, they were looking for a measurable answer to the increasingly hostile cybersecurity environment and started questioning their software development and verification strategies.
Fuzzing Out Bugs in Safety-Critical Embedded Software: Paul Butcher from AdaCore talks to Brandon Lewis from Embedded Toolbox
When an enthusiastic Ada programmer and a SPARK expert pair up to prove the most "stupid" sorting algorithm, lessons are learned! Join us in this eye-opening journey.
A retrospective on learning Ada and developing a tool with it in 2021 from 2021 Ada Crate of the Year Winner Paul Jarrett.
In June of 2021 we announced the launch of a new programming competition called Ada/SPARK Crate Of The Year Awards. We believe the Alire source package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem. Today we are pleased to announce the results. But first, we want to congratulate all the participants, and the Alire community at large, for reaching 200 crates in the ecosystem in January of this year. We truly believe in a bright future for the Ada/SPARK open-source ecosystem with Alire at the forefront. Reaching this milestone is a great sign, inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.
Through the HICLASS UK research group, AdaCore has been developing security-focused software development tools that are aligned with the objectives stated within the avionics security standards. In addition, they have been developing further guidelines that describe how vulnerability identification and security assurance activities can be described within a Plan for Security Aspects of Certification.
A couple years ago I started to tackle what was probably my most daunting project at the time, an embedded USB Device stack written 100% in Ada.
This post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at yet more performance improvement via proof-driven "operator narrowing", porting the library to GNAT Community 2021, and the effect that has on proof and performance of the code.
This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and comparing results with those for the original "TweetNaCl" C implementation.
Some of you may recall an AdaCore blog post written in 2017 by Thales engineer Lionel Matias titled "Leveraging Ada Run-Time Checks with Fuzz Testing in AFL". This insightful post took us on a journey of discovery as Lionel demonstrated how Ada programs, compiled using GNAT Pro and an adapted assembler pass can be subjected to advanced fuzz testing. In order to achieve this Lionel demonstrated how instrumentation of the generated assembly code around jump and label instructions, could be subjected to grey-box (path aware) fuzz testing (using the original AFL v2.52b as the fuzz engine). Lionel explained how applying the comprehensive spectrum of Ada runtime checks, in conjunction with Ada's strong typing and contract based programming, enhanced the capabilities of fuzz testing beyond the abilities of other languages. Ada's advanced runtime checking, for exceptions like overflows, and the scrutiny of Ada's design by contract assertions allow corner case bugs to be found whilst also utilising fuzz testing to verify functional correctness.
The AFT (Autonomous FireTruck) is a prototype of an autonomous firetruck that can put out fire without risking people's lives. This project won a finalist prize in the Make with Ada 2019/20 competition.
Blaine Osepchuk's project won a finalist prize in the Make with Ada 2019/20 competition. This project was originally posted on Hackster.io here. For those interested in participating in the 2020/21 competition, registration is now open and project submissions will be accepted until Jan 31st 2021, register here.
A code obfuscator is a method of sharing coding discussions of real-world examples without giving away proprietary or classified information. This article shows an example of an Ada obfuscator, written in the SPARK language and using the Libadalang library to intelligently hide names and text within the source.
This blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification instead of run-time enforcement of the abstraction’s semantics. We will prove that there are no reads of unassigned variables, no array indexing errors, no range errors, no numeric overflow errors, no attempts to push onto a full stack, no attempts to pop from an empty stack, that subprogram bodies implement their functional requirements, and so on. As a result, we get a maximally robust implementation of a reusable stack abstraction providing all the facilities required for production use.
One of the most powerful features of Ada 2012* is the ability to specify contracts on your code. Contracts describe conditions that must be satisfied upon entry (preconditions) and upon exit (postconditions) of your subprogram. Preconditions describe the context in which the subprogram must be called, and postconditions describe conditions that will be adhered to by the subprogram’s implementation. If you think about it, contracts are a natural evolution of Ada’s core design principle. To encourage developers to be as explicit as possible with their expressions, putting both the compiler/toolchain and other developers in the best position to help them develop better code.
Over the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under the 2-clause BSD licence. This blog entry goes into a bit more technical detail on one particular aspect of the project: the challenge of re-writing and verifying "constant time" algorithms using SPARK.
For nearly four decades the Ada language (in all versions of the standard) has been helping developers meet the most stringent reliability, safety and security requirements in the embedded market. As such, Ada has become an entrenched player in its historic A&D niche, where its technical advantages are recognized and well understood. Ada has also seen usage in other domains (such as medical and transportation) but its penetration has progressed at a somewhat slower pace. In these other markets Ada stands in particular contrast with the C language, which, although suffering from extremely well known and documented flaws, remains a strong and seldom questioned default choice. Or at least, when it’s not the choice, C is still the starting point (a gateway drug?) for alternatives such as C++ or Java, which in the end still lack the software engineering benefits that Ada embodies..
The Danish Technical University has a yearly RoboCup where autonomous vehicles solve a number of challenges. We participated with RoadRunner, a 3D printed robot with wheel suspension, based on the BeagleBone Blue ARM-based board and the Pixy 1 camera with custom firmware enabling real-time line detection. Code is written in Ada and formally proved correct with SPARK at Silver level.
A question that our users sometimes ask us is "do you use CodePeer at AdaCore and if so, how?". The answer is yes! and this blog post will hopefully give you some insights into how we are doing it for our own needs.
My colleague, Carl Brandon, and I have been running the CubeSat Laboratory at Vermont Technical College (VTC) for over ten years. During that time we have worked with nearly two dozen students on building and programming CubeSat nano satellites. Because of their general inexperience, and because of the high student turnover rate that is natural in an educational setting, our development process is often far from ideal. Here SPARK has been extremely valuable to us. What we lack in rigor of the development process we make up for in the rigor of the SPARK language and tools. In November 2013 we launched a low Earth orbiting CubeSat. The launch vehicle contained 13 other university built CubeSats. Most were never heard from. One worked for a few months. Ours worked for two years until it reentered Earth's atmosphere as planned in November 2015.
The promise behind the SPARK language is the ability to formally demonstrate properties in your code regardless of the input values that are supplied - as long as those values satisfy specified constraints. As such, this is quite different from static analysis tools such as our CodePeer or the typical offering available for e.g. the C language, which trade completeness for efficiency in the name of pragmatism. Indeed, the problem they’re trying to solve - finding bugs in existing applications - makes it impossible to be complete. Or, if completeness is achieved, then it is at the cost of massive amount of uncertainties (“false alarms”). SPARK takes a different approach. It requires the programmer to stay within the boundaries of a (relatively large) Ada language subset and to annotate the source code with additional information - at the benefit of being able to be complete (or sound) in the verification of certain properties, and without inundating the programmer with false alarms.
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.
Fuzzing is a very popular bug finding method. The concept, very simple, is to continuously inject random (garbage) data as input of a software component, and wait for it to crash. If, like me, you find writing robustness test tedious and not very efficient in finding bugs, you might want to try fuzzing your Ada code.Here's a recipe to fuzz-test your Ada code, using American Fuzzy Lop and all the runtime checks your favorite Ada compiler can provide.Let's see (quickly) how AFL works, then jump right into fuzzing 3 open-source Ada libraries: ZipAda, AdaYaml, and GNATCOLL.JSON.
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.
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.
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.
This post has been updated in March 2017 and was originally posted in March 2016.
At AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our coding standard checker GNATcheck to deal with more syntactic or weakly-semantic checks. The recent Libadalang technology, developed at AdaCore, provided us with an ideal basis to develop specialized light-weight static analyzers. As an experiment, we implemented two simple checkers using the Python binding of Libadalang. The results on our own codebase were eye-opening: we found a dozen bugs in the codebases of the tools we develop at AdaCore (including the compiler and static analyzers).
AdaCore will be hosting a joint webcast next Monday 12th December 2pm ET/11am PT with SPARK experts Yannick Moy and Rod Chapman. Together, they will present the current status of the SPARK solution and explain how it can be successfully adopted in your current software development processes.
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?
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.
As seen in the previous blog article, AdaCore relies heavily on virtualisation to perform the testing of its GNAT Pro products for VxWorks.
We are pleased to announce that on April 27th our partner, Vector, will host a webinar to showcase their latest VectorCAST/Ada release!
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.
We are pleased to announce our latest release of SPARK Pro! A product that has been jointly developed alongside our partner Altran and following the global AdaCore Tech Days, you can now see the SPARK 2014 talk, Formal Verification Made Easy by AdaCore’s Hristian Kirtchev, on YouTube.
When the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM cortex-M4 CPU which is supported by GNAT. So I backed the campaign, first to be part of the cool kids and also to try some Ada hacking on the device.
This post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new approach using generic packages as formal parameters to make these new containers highly configurable at compile time.
One of the main challenges to get certification in Ada projects is the achievement of 100% code coverage but in most projects an amount of more than 95% structural coverage is hard to achieve. What can you do with the last 5% of code that can't be covered? DO-178C for example, provides a framework for the integration of various techniques in the development process to solve the problem. In this webinar you learn how static analysis and dynamic testing can help complete analysis for pieces of code that are not covered.
I've recently written an article (in two parts) over at Electronic Design about applying different methods of verification to the same small piece of code. The code in question is an implementation of binary search, and I applied Testing, Static Analysis (using the AdaCore tool CodePeer) and Formal Verification (using the AdaCore tool SPARK 2014).
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.
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.
In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.
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.
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.
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.
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.