Writing software that’s secure, reliable, and safe requires dedication, experience, and good tools. Using programming languages like C and C++ to develop these types of applications, so that developers can improve the quality of their code, usually means relying on additional software such as static-analysis tools.
Ada and it subset, SPARK, incorporate most features addressed by static-analysis tools. However, these programming languages do it one better by allowing programmers to be more specific in their code. Therefore, the compiler can do more checking based on these explicit specifications. Ada 2012’s contract support goes further, still allowing programmers to provide pre and post conditions for functions and subroutines as well as the ability to specify type invariants.
More Articles About Ada and SPARK
The extreme approach takes advantage of SPARK’s formally verifiable proofs. By using the contract definitions, SPARK can prove that an application meets the specifications. In most case, the checks specified in the contracts will be removed from the generated code because all of the checking has been done by the compiler.
So how can one evaluate Ada and SPARK?
1. AdaCore’s learn.adacore.com provides interactive Ada and SPARK training materials.
If you like some heavy reading, then check out John Barne’s Programming in Ada 2012. This rather hefty book is in depth and a useful reference, but not a great idea for novice Ada programmers. Instead, I recommend AdaCore’s new learn.adacore.com website (Fig. 1). It includes a pair of courses: Introduction to Ada and Introduction to SPARK. There’s also an online ebook entitled Ada for the C++ or Java Developer. The ebook can be downloaded as a PDF file.
The other two courses aren’t available as a PDF file at this point because they’re sprinkled with interactive code blocks (Fig. 2) that can be compiled and run. These use the actual Ada and SPARK tools running on AdaCore’s web server. Most of the blocks are designed to run as is to show what the compiler would report as an error or what the results of running the code would emit.
It’s possible to edit the code and rerun/check it to experiment with the environment without having to install the development environment. That chore isn’t difficult, but it’s much more tedious to load and edit code while having to refer back to a description. On the other hand, the web-based approach intersperses the prose about the code with the code itself.
2. The Ada and SPARK course.
The Ada and SPARK courses are extensive but not exhaustive. Likewise, they address the basics like packages; child and nested packages are left for future courses. The Ada course does cover important topics like object-oriented programming, multitasking, and generics. The SPARK course touches on flow analysis, proof of program integrity, and proof of functional correctness.
There are many myths about Ada and SPARK. Hopefully checking out Ada and SPARK will help dispel some of them and ultimately highlight the advantages of Ada and SPARK. These courses will not make you an Ada or SPARK maven, but they should make you more comfortable with the languages and what they’re capable of accomplishing.
AdaCore also has a number of free PDF ebooks including the latest, AdaCore Technologies for Cyber Security by Roderick Chapman and Yannick Moy. About half of it presents AdaCore’s products, including Ada and SPARK compiler, and how they can help address cybersecurity issues.
What will be useful for an embedded developer is the “Security Vulnerabilities and Their Mitigation section.” This presents mitigation recommendations for Common Weakness Enumeration (CWE) maintained by Mitre.
CWE addresses generic problems that can crop up in almost any application. The two at the start of the section address data-validation issues. CWE 20 addresses improper input validation, while CWE 1019 deals with how to validate input errors. Of course, the mitigation approaches are presented in the context of Ada and SPARK. Some, like Weak or No Crypto have mitigations that would be the same regardless of what programming language is used.
