AdaCore Blog

A Readable Introduction to Both MISRA C and SPARK Ada

by Yannick Moy, Nicolas Setton, Ben Brosgol

MISRA C is the most widely known coding standard restricting the use of the C programming language for critical software. For good reasons. For one, its focus is entirely on avoiding error-prone programming features of the C programming language rather than on enforcing a particular programming style. In addition, a large majority of rules it defines are checkable automatically (116 rules out of the total 159 guidelines), and many tools are available to enforce those. As a coding standard, MISRA C even goes out of its way to define a consistent sub-language of C, with its own typing rules (called the "essential type model" in MISRA C) to make up for the lack of strong typing in C.

That being said, it's still a long shot to call it a security coding standard for C. Even when taking into account the 14 additional guidelines focusing on security of the "MISRA C:2012 - Amendment 1: Additional security guidelines for MISRA C:2012". MISRA C is first and foremost focusing on software quality, which has obvious consequences for security, but programs in MISRA C remain for the most part vulnerable to the major security vulnerabilities that plague C programs.

In particular, it's hard to state what guarantees are obtained when respecting the MISRA C rules (which means essentially respecting the 116 decidable rules enforced automatically by analysis tools). In order to clarify this, and to present at the same time how guarantees can be obtained using a different programming language, we have written a book available online. Even better, we host on our e-learning website an interactive version of the book where you can compile C or Ada code, and analyze SPARK code, to experiment how a different language with its associated analysis toolset can go beyond what MISRA C allows.

So that, even if MISRA C is the best thing that could happen to C, you can decide if C is really the best thing that could happen to your software.

Posted in #MISRA-C    #SPARK    #Safety    #Security   

About Yannick Moy

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). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.

About Nicolas Setton

Nico joined AdaCore in 2001 as an engineer, and has worked on many interesting things since. Now managing the IDE circle and Product Manager of GNAT Community.

About Ben Brosgol

Dr. Benjamin Brosgol is a senior member of the technical staff of AdaCore. He has been involved with programming language design and implementation for more than 30 years, concentrating on languages and technologies for high-integrity systems. Dr. Brosgol was a  Distinguished Reviewer of the original Ada language specification and a member of the design team for the Ada 95 revision. He has presented dozens of papers and tutorials over the years at conferences including ACM SIGAda, Ada-Europe, SSTC (Systems & Software Technology Conference), and ICSE (IEEE/ACM International Conference on Software Engineering).