Undecidable Rules and How to Deal with Them
Safety standards usually demand writing safety-critical software in compliance with specific coding guidelines to ensure safe, secure, and reliable applications. Following commonly-accepted development guidelines like MISRA, ISO/IEC TS17961:2013 or the CERT rules and recommendations is the most common approach to meet these demands.
Since MISRA C:2012, the MISRA guidelines are classified as decidable or undecidable, depending on the theoretical ability of a static analysis to answer the question "Does this code comply with this rule" with "yes" or "no". Undecidable rules require information about the program semantics, e.g., what value an object holds, or whether a particular program point is reachable. Rice's Theorem states that no static analysis can give a correct yes/no answer in every case once a rule addresses semantic properties of an application. However, depending on the analysis depth, it is possible to derive an answer with different levels of assurance: unsound static analyzers can miss guideline violations (false negative) as well as report spurious violations (false positive).
With a sound analyzer, the absence of false negatives can be proven as they can guarantee to never miss a violation.
This talk explains the concept of soundness, discusses to which degree the undecidable programming guidelines of popular standards like MISRA C can be covered by automatic tools, and what level of assurance can be achieved in practice.