What is “defensive code” and why do we care?
We’ve heard that a million times already, and are getting ready to hear it a million times again: software development is more and more important in industrial processes, and software reliability is becoming more and more of a key concern. The cost of software failure is not restricted to any specific market or limited to purely financial penalty with serious impact also eroding reputation and brand names. Domains such as finance, automotive and medical devices have been very prolific in this area in the past few years. As a result, good practices or even certification processes are getting more and more central. Developing reliable software involves many things, from qualified personnel to development tools, programming guidelines, requirements definition and quality assurance. The ultimate goal is either to reduce the probability of software error, or reduce the impact of said software errors.
To make progress in the latter, a common technique is the use of so-called defensive code. Defensive code consists most commonly of checking the domain of a given variable and ensuring that it is acceptable before performing a given computation. This could be useful to detect potential division by zero and therefore preventing an unexpected crash, or generally speaking to identify early on a value that doesn’t make sense and avoid performing a computation – or worse, an action outside of the normal function. Think of a medical irradiation device that would be asked to provide 100 times more of any reasonable dosage of radiation, or a car cruise control that would set itself to several thousands of km/h. Or to a negative value. Defensive code is intended to detect these breaches of consistency, and treat them appropriately.
Given the complexity of systems being developed today, such errors have to be expected. This may be due to a hardware error, a malfunctioning sensor, an integration error between two independently developed components, an error in the documentation, or due to a programming error. But the fact of the matter is, sometime, somewhere, a value will be wrong. Failure to detect and react to it will lead to catastrophic events. Mitigation measures must be implemented. Defensive code is almost always part of the answer.
Unfortunately, defensive code brings its own set of challenges. Traditionally, defensive code is a set of “if” conditions at the beginning of a function. In other words, this is code that has to be written and maintained as any other code. This increases development costs and risks. How can it be assured that said defensive code is always added – and furthermore is correct? This decreases the performance of the application – extra conditions will have to be systematically checked when entering functions. This increases maintenance costs – refactoring or changing this defensive code may require changes to be made in many places. This increases verification costs. How can this defensive code be verified – in particular knowing that in some places it’s there to provision for conditions that are unexpected and therefore not planned? Not to mention the fact that this defensive code is usually in the implementation of the function, and maintaining the information at specification level - or even at model level – is yet another cost and source of potential inconsistencies.
In this paper, we’ll show how modern programming languages such as Ada 2012 can help managing the challenges of defensive code, by allowing developers to move said code from the implementation of the function to the function specification. We’ll show how these specifications can be the basis of static analysis, with the final objective of identifying and removing unnecessary defensive code in the application. We’ll conclude with a word of common sense, re-stating that Ada will help improve software engineering in this regard but can still be used incorrectly, as some well-known industrial catastrophes still painfully remind us.
Defensive by design
Ada is a programming language well known by industries that have history in reliable software such as avionics, space, defense or transportation. One of the main reasons is that the language has been designed to enforce or ease the use of a number of good practices of programming, in particular by allowing data checks to be more easily deployed across the program. Instead of being manually written in the executable code, these checks are usually defined at the specification level, the compiler being then responsible for deploying them where appropriate.
The most common and simple check of this kind is a dynamic check. Suppose for example that a system is handling physical units such as a speed on a vehicle. By design, it is possible to identify values that make sense and values that do not. In a typical C program, this “making sense” is difficult to implement. But surely, if a value significantly out of bounds is received by one of the systems, one can expect that said system will not behave properly. Let’s this in action in an example:
#DEFINE MAX_SPEED = 200
#DEFINE MIN_SPEED = 0
void setAutoCruise (float speed) {
if (speed > MAX_SPEED || speed < MIN_SPEED) {
return;
}
// code
}
void setSpeed (float speed) {
if (speed > MAX_SPEED || speed < MIN_SPEED) {
return;
}
// code
}
Within this example, tests for speed domain have to be done twice, in the implementation of both subprograms. It’s expected that similar tests would be written and maintained in other parts of the system. Having to write such tests manually is extremely cumbersome, and awkward. Ideally, we would like to be able to identify an abstraction associated with the physical unit speed, and associate constraints with it. In some languages, such as C++ or Java, we may want to encapsulate this data in a class. However, the overhead for something as simple as a scalar value can quickly become unreasonable.
Ada offers a different solution to this. It allows to define a type as a high level abstraction, and associated to this type semantic properties. In particular, we can define boundaries to said type, and then type parameters appropriately. The example may become in Ada:
type Speed_Type isnew Float range 0.0 .. 200.0;
procedure Set_Auto_Cruise (Speed : Speed_Type) is
begin
-- code
end Set_Auto_Cruise;
procedure Set_Speed (Speed : Speed_Type) is
begin
-- code
end Set_Speed;
By default, these two pieces of code are supposed to do the exact same thing. The Ada semantics are enforcing a check at parameter passing time. However, the above code offers additional flexibility over the C version for a number of reasons:
- Obviously, checks don’t have to be written. This removes the burden of making sure that they are indeed written.
- There is no extra code to cover, or lack of coverage to be justified. This can have a significant impact in case of certification activities.
- Depending on testing and deployment strategies, such checks can be easily activated or deactivated by using compiler switches. Some team may like to enable them all at test time for example, and only keep the critical ones after deployment as not to pay the performances footprint.
- But most important of all – the requirement on the domain of speed is now known at the subprogram specification level – it is part of its profile. It is no more an implementation detail. The caller knows now there is an expectation to respect this constraint otherwise something will go wrong.
This is just one of the many examples where this “Strong typing” feature of the Ada language can be useful. But Ada provides additional ways or raising internal constraints at the level of subprogram and parameter specification. To give another example, pointers are often a source of many vulnerabilities in code, to which many languages have tried to provide different solution. None of which are fully satisfactory, and Ada is no exception to the rule. Its design is made as to avoid the use of pointers as much as possible, but there are programming structures that just can’t be written effectively without the use of some kind of indirection. Among the potential problems that may arise when using pointers is the question of the handling of null values. Again, management of such values often results in the development of defensive code. Here’s an example in C:
typedefstruct _Cell Cell;
struct _Cell {
Cell * next;
Cell * prev;
int value;
};
void add (Cell *C, int val) {
if (C == NULL) {
return;
}
// code
}
Once again, the above code can be easily simplified by modifying the specification in Ada:
type Cell isrecord
Next : access Cell;
Prev : access Cell;
Value : Integer;
endrecord;
procedure Add
(Cell : notnullaccess Cell; Val : Integer) is
begin
-- code
end Add;
Programming by contracts
Of course, there’s only so many cases of defensive code patterns that can be taken into account as part of the language pre-built stereotypes. In many situations, defensive code has to go beyond basic checks for nulls and domains, and may have to check more complex relationships. Let’s look at another example:
First_Char : Integer;
Line : array (1 .. 1024) of Character;
function Get_Char return Character is
C : Character;
begin
C := Line (First_Char);
First_Char := First_Char + 1;
return C;
end Get_Char;
In the above code, the first line of the subprogram intends to access the character of the array “Line” indexed by “First_Char”. There is of course a potential run-time error here, in case of First_Char being out of the boundaries of Line. A natural way to protect the code against such problem is to add defensive code in the function itself, such as:
function Get_Char return Character is
C : Character;
begin
if First_Char in Line'Range then
C := Line (First_Char);
First_Char := First_Char + 1;
return C;
else
return ASCII.NUL;
endif;
end Get_Char;
While this is perfectly acceptable from a run-time error avoidance perspective, this implies the creation of a potential additional requirement on the function, which states that if First_Line is out of the boundaries, the index is not incremented and a default value is returned. The consequences can be disturbing at the caller level. Consider:
loop
Current_Char := Input.Get_Char;
exitwhen Current_Char in 'A' .. 'Z';
endloop;
In the above code, if First_Char happens to be out of bounds, the loop will never exit. So the introduction of unmanaged defensive code may introduce further problems. So let’s try something else. Instead of hiding defensive code in the body of this subprogram, we’re going to translate the fact that First_Char has to be in Line range into a precondition of Get_Char. In other words, we’re going to specify at subprogram profile level that Get_Char has to be called with First_Line within the boundaries of Line:
function Get_Char return Character
with Pre => First_Char in Line'Range;
function Get_Char return Character is
C : Character;
begin
C := Line (First_Char);
First_Char := First_Char + 1;
return C;
end Get_Char;
We now clearly have stated that it is the responsibility of the caller to verify the membership. Surely, the developer of the loop didn’t follow this. There are various ways of bringing it to his attention – the most common one being, as for other kinds of checks, to enable run-time verification. In other words, the compiler can generate a run-time check to verify that at each call the constraint is respected. We’ll see later on that other techniques such as static analysis and formal proof can be used as well.
While the precondition is probably the easiest and most common contract, others are available to further specify behavior and expectations. For example, in the above example, we could have specified that the value of First_Char is incremented by the subprogram. As a result, taking the precondition and the postcondition, we know that we cannot assume that First_Char is within the boundaries of Line after the call, but at worst is one step beyond the last element:
function Get_Char return Character
with Pre => First_Char in Line'Range,
Post => First_Char = First_Char'Old + 1;
Generally speaking, such a postcondition can be used to describe the behavior or requirements of a subprogram. However, this way of using contracts requires more developer involvement and is outside the scope of this paper.
Contracts can be defined at type level as well, as to further specify valid values for a given data kind. We saw in the previous section a simple case of a range of values associated to a type. The notion of predicate allows it to go further, and to specify an arbitrary Boolean expression to define specific value. This may result in types that are defined by a non-continuous range of values. For example, the following type defines an integer that only allows for even values:
type Even isnew Integer
with Dynamic_Predicate => Even mod 2 = 0;
Such predicate can even be defined at type level and define interactions between components of such types. For example, the following code defines a stack in Ada, specifying that the size has to be below maximal size:
type Stack (Max_Size : Integer) isrecord
Data : Data_Array (1 .. Max_Size);
Size : Integer;
endrecord
with Dynamic_Predicate => Stack.Size < Stack.Data'Last;
From a defensive code point of view, these constructions allow the definition of constraints in the code that can either drive writing of further subprogram contracts or allow the reliance on explicit properties. This will depend on the verification strategy described later.
In order to complete the picture, it’s important to mention the existence of assertions. These are common to many languages, and have the advantage of being clearly identified as assumptions made on the normal execution of the code. In other words, they are known to be additional checks, and shouldn’t have influence over the normal execution of the code (they should be always true).
The main disadvantage of using these assertions is that they are not known by the specification. However, they can serve a key role in verification techniques, in particular for static analysis and formal proof. For the sake of completeness, here’s an example of such assertion in the Get_Char code:
function Get_Char return Character is
C : Character;
begin
pragma Assert (First_Char in Line'Range);
C := Line (First_Char);
First_Char := First_Char + 1;
return C;
end Get_Char;
Dynamic verification – the GNAT case
Once constraints, contracts and assertions are defined, it’s tempting to look for ways to verify that they are correctly enforced. One could argue that the sole fact that they’re part of the specification already gives a certain level of assurance. At least, the diligent developer has ways to verify how he’s supposed to use entities of the program with little ambiguity. However, no matter how well behaved one developer can be, there will always be the possibility of a genuine mistake. Hence the need for verification.
The most common way to verify enforcement of these rules is to translate all these assertions into dynamic checks. For a type range, this will translate into a domain check at various point in the program, such as assignments, parameter passing or conversions. For a precondition, it will be a check after parameter elaboration. For a postcondition, it will be a check after result evaluation.
Different processes and design principles will require the activation or de-deactivation of checks at various stages of the development. For example, high integrity applications aim for zero defect (or upsilon, rather) in the final binary. Leaving checks active in such applications would just end up reducing runtime performance. Worse – in a number of cases, it’s better to carry on with an incorrect result than to raise an exception on an error. Thus the tendency of such processes is to enable as many check as possible during unit and integration testing, as to find potential defects as soon as possible, and to deactivate everything in production mode.
On the other end of the spectrum, in less reliable software, it’s better to have a proper crash rather than continuing a wrong computation. In such case, leaving some level of check in the final binary may be beneficial to the overall reliability. Nonetheless, even in these cases, some of these checks may not be desirable. GNAT offers various switches and pragma allowing the fine tuning of verification overhead.
In particular, there are three main categories
- “regular” checks of the language, such as range or array index checks, active by default, that can be deactivated through the compiler switch –gnatp
- validity checks at all points of occurrence deactivated by default, that can be activated through the compiler switch –gnatVa
- assertions, such as preconditions, deactivated by default, that can be activated through the compiler switch –gnata.
If finer granularity is needed, it’s possible to enable / disable checks within an arbitrary section of a file. This is useful for example in case of a performance bottleneck for which confidence is high. Let’s go back to our Get_Char example. As we are accessing an element in an array, the compiler will generate a check by default to ensure that First_Char is within the range of Line. Assuming that the level of verification around callers is sufficient, one developer may want to write:
function Get_Char return Character is
pragma Suppress (All_Checks);
C : Character;
begin
C := Line (First_Char);
First_Char := First_Char + 1;
return C;
end Get_Char;
Of course, if by mistake First_Char is beyond the boundaries of Line, we’re back to the persistent risk of buffer overflow. To be manipulated with great care. It’s interesting to compare this to similar code with C, as to illustrate the difference of philosophy between the two languages. C would promote efficiency by default, allowing to access to an array without check and letting to the developer the liberty to add additional safety conditions around operations. Ada will promote safety by default, allowing developer to specifically indicate places where the trade-off should be reversed. Subsequently, in terms of code review, identifying these places becomes an easier task.
Static verification and pragmatism
Testing is one thing, but with all this information in the code, isn’t there some things that we could see just by looking at it? Couldn’t we deduce by some basic computation that such a variable is obviously in range, or has a high chance of not being? That a precondition is always respected by design, or except in some easy to identify corner cases? Welcome to the world of static analysis.
Ideally, a static verification should combine three characteristics:
- it should be “sound”, that is leave no potential problem
- it should be “precise”, that is, don’t report false alarms
- it should be “automatic”, that is, doesn’t require additions to the code or manual analysis
Reality teaches us that it’s possible to get two of this things in the same tool, but never three. As for dynamic analysis, selection of tools and techniques will depend on the level of integrity to be achieved, as well as the desired development process.
The Ada language comes with tools that are targeting various combinations. One category of tools is the so called abstract interpretation tools, such as CodePeer. These can take as input an arbitrary set of Ada sources, and look for potential run-time errors. The efficiency of such tools is directly linked to their way to handle false positives, and to allow developers to concentrate on the most interesting pieces of code in the application.
On the other end of the spectrum, tools such as SPARK allow a much more precise analysis of the code. However, they only work on a specific subset of the language, forbidding certain features such as the use of pointers or exceptions handlers. Moreover, additional assertions and contracts are typically required to achieve full automatic proof. Writing correct and efficient assertions, as well as driving automatic proof tools may require specific training not usually part of software development curricula.
Usage of these tools has often suffered from a high level of ambition. It’s easy to believe that it will be possible to resolve an entire category of error with one of these tools just by the magic of a button and a little set of fixes. The reality is quite different. Trying to do it all almost systematically leads to intense frustration from developers and disappointment from managers. This is too bad, because there is a very pragmatic way of considering those things.
In Ada, static analysis and dynamic analysis rely on the same notation. When a developer starts to write a constraint, a range or a precondition for example, he can delay the final decision on how it’s going to be verified. Try with static analysis, fallback to dynamic analysis if it happens to be to complex, or come back to static analysis later on. These decisions can be taken at fine granularity, down to the subprogram itself, hence creating a program that presents a hybrid and pragmatic verification strategy. This is most definitely key to optimizing verification costs.
And the beauty of it – all of this can be done without a single line of defensive code.
This is no silver bullet
In 1996, the well-known crash of Ariane 5 was attributed to a piece of defensive code for which failure was not handled. As a matter of fact, the Ariane 5 issue is even more uncomfortable than that: the defensive code was wrong to start with. Values were perfectly reasonable in the end and should have been accepted by the software. The irony is that the language that was used at the time was specifically planned to simplify and automate the production of said defensive code, and was the one that we’ve been advocating for today: Ada. Lesson learned, the language is always a tool that can help software engineering, but never replace proper development process.
None of the techniques or tools presented today can offer any cost reduction or safety improvement by themselves. However, if properly integrated, they offer potential significant gain at many levels. They support improvement of specification, and link this directly to verification activities, while remaining in a formalism that is known and understood by software engineers. They’re not coming without challenges, and often require adjustments in the way software is being developed. One of the most significant changes being the fact that verification becomes embedded in code development, as opposed to be being done subsequently.
At the end of the day though, the outcome is clear – reducing the amount of unnecessary code reduces maintenance and the verification burden. Why not try that out?
About the authors
Quentin Ochem has a software engineering background, specialized in software development for critical applications. He has over 10 years of experience in Ada development. He works today as a technical account manager for AdaCore, following projects related to avionics, railroad, space and defense industries. He also teaches the avionics standard DO-178B course at the EPITA University in Paris.
Martyn is a Technical Account Manager at AdaCore. He first encountered Ada in 1992 while studying for a Bachelor’s degree in Computing. Until this point the C programming language had dominated his experience of programming and it was a breath of fresh air to meet concepts such as packages, subprograms as procedures and functions and of course the concept of the Ada Task.
His use of Ada continued in his professional career but he also dabbled in C/C++ through his work for an Embedded Software Tools Vendor and as an Independent Consultant resulting in a thorough understanding of the challenges in modern software development.
Martyn holds a Bachelor’s Degree with Honors in Computing from Oxford Brookes University.
