The Place for MISRA C in Safe & Secure Programming - A Comparison with SPARK

January 21, 2021

Story

As part of the Linux Security Summit Europe last October, I participated in a panel around the question, “Would Abandoning the C Language Really Help?”. C, which is the main language used in the Linux kernel, is notorious for having an endless source of vulnerabilities. Just look at the long list of open bugs automatically reported by the fuzzing robot syzbot that are still waiting for a fix.

The panel discussion revolved around alternative safer languages suitable for kernel development like Ada and Rust, as well as the need for formal verification to go beyond the guarantees that a compiler can provide. Indeed, many memory and safety vulnerabilities currently reported on the Linux kernel would stop the program altogether in Ada or Rust, which is only slightly better. Looking at kernel patches reveals that many issues could be detected by specifying simple properties on the code, like what calls are legal in which mode, the types of data invariants that should be preserved, and how to verify them statically using appropriate tools.

Surprisingly, MISRA C was not mentioned at all during the discussion, even though it has established itself as a must-have in a number of industries to protect against fallibilities of the C language. MISRA C appeared in 1998 as a coding standard for C, initially for the automotive industry, and has been revised twice. The current version is MISRA C:2012. It focuses on avoiding error-prone features of the C programming language rather than on enforcing a particular programming style. A study of coding standards for C, written by Les Hatton, found that, compared to ten typical coding standards for C, MISRA C was the only one to focus exclusively on error avoidance rather than style enforcement, and by a very large margin.

The popularity of the C programming language, as well as its many traps and pitfalls, have led to the huge success of MISRA C in domains where C is used for high-integrity software. This success has driven tool vendors to propose many competing implementations of MISRA C checkers. Tools compete in particular on the coverage of MISRA C guidelines that they help enforce, as it is impossible to enforce all of the 16 directives and 143 rules (collectively referred to as guidelines) of MISRA C.

In particular, 27 rules out of 143 are not decidable, so no tool can always detect all violations of these rules without at the same time reporting "false alarms" on code that does not constitute a violation. An example of an undecidable rule is rule 1.3: "There shall be no occurrence of undefined or critical unspecified behavior." Appendix H of MISRA C:2012 lists hundreds of cases of undefined and critical unspecified behavior in the C programming language standard, a majority of which are not individually decidable. For the most part, MISRA C checkers ignore undecidable rules such as rule 1.3, although violations of these rules are known to have a dramatic impact on software quality.

However, for other programming languages, static analysis technology is available that can tackle this challenge without inundating users with false alarms. One example is the SPARK toolset developed by AdaCore, Altran, and Inria, which is based on four principles:

• The base language Ada provides a solid foundation for static analysis through a well-defined language standard, strong typing, and rich specification features.
• The SPARK subset of Ada restricts the base language in essential ways to support static analysis, by controlling sources of ambiguity such as side-effects in functions and aliasing of names.
• The static analysis tools work mostly at the granularity of an individual function, making the analysis more precise and minimizing the possibility of false alarms.
• The static analysis tools are interactive, allowing users to guide the analysis if necessary or desired, and providing counterexamples when user-supplied contracts cannot be proved.

SPARK can be incrementally adopted in a C codebase, progressively gaining assurance through the five levels of SPARK adoption and by supporting “hybrid verification” that combines formal analysis (SPARK) with traditional testing-based methods (C) .

 

SPARK Stone Level - Basic Guarantees

The first level of SPARK adoption is called the Stone Level. It corresponds to code that conforms to the SPARK subset of Ada. Just adopting this level guarantees many consistency properties that cannot be enforced for C. These include:

• The use of a proper package system as opposed to C’s use of textual-based inclusion of files with no consistency requirements across translation units;

• Strict and readable syntax that emphasizes clarity and minimizes “gotchas”  as opposed to C’s very permissive syntax which makes it easy to write programs whose effect is not what was intended,
• Adherence to the strong typing rules of Ada and SPARK, as opposed to  C’s “poor type safety [that] permits a wide range of implicit type conversions to take place [which] can compromise safety as their implementation-defined aspects can cause developer confusion." (MISRA C:2012, Annex C)

MISRA C attempts to tame these possible inconsistencies of the C language with a variety of guidelines. It defines in particular stronger typing rules ("The essential type model") and restricts the use of function parameters/results and control structures. While these avoid common sources of developer confusion, they are intentionally not bulletproof, as they would otherwise make most C programs illegal.

These basic guarantees are easily achieved in SPARK with a simple compiler-like analysis by a tool called GNATprove, thanks to the stronger rules that define the SPARK subset of Ada.

SPARK Silver Level - Strong Safety & Security Guarantees

MISRA-C guidelines also aim at preventing more subtle errors, reads of uninitialized data, conflicting side-effects in expressions, and undefined behavior such as division by zero or buffer overflow (which can have safety as well as security consequences). All of this fall in the category of undecidable rules, for which few MISRA C checkers provide complete detection.

These are completely prevented at the Silver level of SPARK adoption, which corresponds to analyzing the program with both flow analysis (reaching the second level of SPARK adoption called Bronze) and proof of the absence of run-time errors (reaching the third level, i.e. Silver). To reach this level, a developer will generally need to define types with the specific constraints that they are designed to support and supply contracts on functions exported between files - using so-called preconditions for specifying the obligations on the caller, and postconditions for specifying the obligations on the callee.

The process for reaching the Silver level involves interaction with the IDE. The developer runs the GNATprove tool, possibly on a subset of the program, investigates the GNATprove diagnostics, updates the program accordingly, and repeats. Such interactions are facilitated by the detailed information provided by GNATprove at every step to guide developers. Here is an example of a message displayed by GNATprove:

After locating the addition operation which may cause an overflow, GNATprove gives an example of a value triggering the problem, here the largest Integer value (denoted Integer’Last in SPARK). The “reason for check” explains clearly that the result of the addition should fit in a machine integer, which is not the case if X is the largest integer value before the addition. Then, GNATprove suggests that adding a suitable precondition to the function Incr might solve the problem, by specifying here that X cannot be that largest value.

SPARK Beyond the Silver Level

There are further benefits of using SPARK, that go well beyond what MISRA C checkers can provide. At the Gold and Platinum levels, a developer specifies properties of the program through SPARK contracts and can then use GNATprove to guarantee that these properties will be met. A developer can also enable GNATprove warnings to detect dead code (also an objective pursued by MISRA C) and inconsistencies in the code, using the powerful proof technology that forms the basis of GNATprove analysis.

Conclusion

Essentially, all objectives pursued by MISRA C are best achieved in SPARK, with a combination of a stronger base language (Ada) and a powerful analysis tool (GNATprove). Developers who are planning to use MISRA C rules can achieve increased assurance by adopting SPARK for part of their applications.

The rules in MISRA C represent an impressive collective effort to improve the reliability of C code in critical applications, with a focus on avoiding error-prone features rather than enforcing a particular programming style. At a fundamental level, however, MISRA C is still built on a base language that was not really designed with the goal of supporting large high-assurance applications. It's hard to retrofit reliability, safety and security into a language that did not have these as goals from the start.

As C will remain the base language for large programs like the Linux kernel, we can foresee the coexistence of two trends to protect better against fallibilities in C programs, where MISRA C can play a role, and to replace C with safer languages like Rust and SPARK Ada for part of the code. Major actors in the automotive industry have started on this latter path, like NVIDIA and JTEKT.

References

Guidance for adoption of SPARK can be found at https://www.adacore.com/books/implementation-guidance-spark/

The GNATprove tool is freely available as part of the GNAT Community Edition at https://www.adacore.com/download

A detailed comparison of SPARK and MISRA-C, as well as various courses to learn Ada and SPARK, can be found at AdaCore's learn.adacore.com site.

About the Author

Yannick Moy is SPARK Product Manager at AdaCore and co-director of the ProofInUse joint laboratory with Inria. 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