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.