MISRA C在安全可靠的编程中的地位

C是Linux内核中使用的主要语言，因具有无穷无尽的漏洞源而臭名昭着。只需查看模糊测试机器人syzbot自动报告的一长串开放错误，这些错误仍在等待修复。

小组讨论围绕着适合内核开发的替代更安全的语言，如Ada和Rust，以及形式验证的需求，以超越编译器可以提供的保证。事实上，目前在Linux内核上报告的许多内存和安全漏洞都会在Ada或Rust中完全停止该程序，这只会稍微好一点。查看内核补丁可以发现，通过在代码上指定简单的属性可以检测到许多问题，例如在哪种模式下哪些调用是合法的，应该保留的数据类型不变量，以及如何使用适当的工具静态验证它们。

令人惊讶的是，在讨论中根本没有提到MISRA C，尽管它已经将自己确立为许多行业的必备品，以防止C语言的谬误。MISRA C于1998年作为C的编码标准出现，最初是汽车行业的编码标准，并已进行了两次修订。当前版本是 米斯拉 C：2012。它侧重于避免 C 编程语言中容易出错的功能，而不是强制实施特定的编程风格。由Les Hatton撰写的一项关于C编码标准的研究发现，与十个典型的C编码标准相比，MISRA C是唯一一个专注于避免错误而不是样式执行的标准，并且有很大的差距。

C编程语言的普及，以及它的许多陷阱和陷阱，导致了MISRA C在C用于高完整性软件的领域中的巨大成功。这一成功促使工具供应商提出了许多竞争性的MISRA C检查器实现。工具在它们帮助执行的MISRA C指南的覆盖范围上尤其相互竞争，因为不可能执行MISRA C的所有16项指令和143条规则（统称为指南）。

特别是，143 条规则中有 27 条是不可判定的，因此没有工具可以始终检测所有违反这些规则的行为，而不会同时报告不构成违规的代码的“误报”。不可判定规则的一个例子是规则1.3：“不得发生未定义或关键的未指定行为。MISRA C：2012 的附录 H 列出了 C 编程语言标准中数百个未定义和关键未指定行为的案例，其中大多数无法单独确定。在大多数情况下，MISRA C检查器忽略了规则1.3等不可判定的规则，尽管已知违反这些规则会对软件质量产生巨大影响。

但是，对于其他编程语言，可以使用静态分析技术来解决这一挑战，而不会使用户被误报淹没。一个例子是由AdaCore，亚创和因里亚开发的SPARK工具集，它基于四个原则：

基础语言Ada通过定义良好的语言标准、强类型和丰富的规范功能，为静态分析提供了坚实的基础。

Ada 的 SPARK 子集通过控制歧义的来源（如函数中的副作用和名称的别名）来以基本方式限制基础语言以支持静态分析。

静态分析工具主要在单个函数的粒度上工作，使分析更加精确，并最大限度地减少误报的可能性。

静态分析工具是交互式的，允许用户在必要或需要时指导分析，并在无法证明用户提供的合同时提供反例。

SPARK可以在C代码库中逐步采用，通过SPARK采用的五个级别和支持将形式分析（SPARK）与传统基于测试的方法（C）相结合的“混合验证”，逐步获得保证。

火花石水平 - 基本保证

SPARK采用的第一个级别称为石头级别。它对应于符合 Ada 的 SPARK 子集的代码。仅采用此级别就可以保证许多无法对 C 强制执行的一致性属性。这些包括：

使用适当的打包系统，而不是C使用基于文本的文件，在翻译单元之间没有一致性要求;

严格且可读的语法，强调清晰度并最小化“陷阱”，而不是C的非常宽松的语法，这使得编写效果不是预期的程序变得容易，

遵守Ada和SPARK的强类型规则，而不是C的“糟糕的类型安全性，允许发生各种隐式类型转换，这可能会损害安全性，因为它们的实现定义方面可能会导致开发人员混淆。（米斯拉C：2012，附件C）

MISRA C试图通过各种指南来驯服C语言的这些可能的不一致。它特别定义了更强的类型规则（“基本类型模型”），并限制了函数参数/结果和控制结构的使用。虽然这些避免了开发人员混淆的常见来源，但它们故意不是防弹的，否则它们会使大多数C程序非法。

这些基本保证在SPARK中很容易通过一个名为GNATprove的工具进行简单的类似编译器的分析来实现，这要归功于定义ADA的SPARK子集的更强大的规则。

SPARK银级 - 强大的安全保障

MISRA-C指南还旨在防止更细微的错误，读取未初始化的数据，表达式中相互冲突的副作用以及未定义的行为，例如除以零或缓冲区溢出（这可能具有安全性和安全性后果）。所有这些都属于不可判定规则的范畴，很少有MISRA C检查器提供完整的检测。

这些在SPARK采用的白银级别上是完全被阻止的，这对应于使用流程分析（达到称为青铜的SPARK采用的第二级）和没有运行时错误的证明（达到第三级，即白银）来分析程序。要达到此级别，开发人员通常需要使用特定约束来定义类型，这些约束旨在支持这些约束，并为文件之间导出的函数提供合同 - 使用所谓的前提条件来指定调用方的义务，并使用后置条件来指定被调用方的义务。

达到白银级的过程涉及与 IDE 的交互。开发人员可能在程序的子集上运行 GNATprove 工具，调查 GNATprove 诊断，相应地更新程序，然后重复。GNATprove在每一步提供的详细信息都有助于促进这种互动，以指导开发人员。以下是 GNATprove 显示的消息示例：

在找到可能导致溢出的加法运算后，GNATprove给出了一个触发问题的值的示例，这里是最大的整数值（在SPARK中表示为整数‘Last）。“检查原因”清楚地解释了加法的结果应该适合机器整数，如果 X 是加法前的最大整数值，则情况并非如此。然后，GNATprove建议向函数Incr添加一个合适的前提条件可能会解决这个问题，在这里指定X不能是最大值。

超越白银级的火花

使用SPARK还有其他好处，远远超出了MISRA C检查器可以提供的。在黄金和白金级别，开发人员通过 SPARK 合约指定程序的属性，然后可以使用 GNATprove 来保证满足这些属性。开发人员还可以使用构成 GNATprove 分析基础的强大证明技术，使 GNATprove 警告能够检测死代码（也是 MISRA C 追求的目标）和代码中的不一致。

结论

从本质上讲，MISRA C追求的所有目标都可以在SPARK中最好地实现，它结合了更强大的基础语言（Ada）和强大的分析工具（GNATprove）。计划使用 MISRA C 规则的开发人员可以通过对其部分应用程序采用 SPARK 来获得更高的保证。

MISRA C中的规则代表了在关键应用程序中提高C代码可靠性的令人印象深刻的集体努力，重点是避免容易出错的功能，而不是强制实施特定的编程风格。然而，在基本层面上，MISRA C仍然建立在基础语言之上，而这种基础语言并不是真正以支持大型高保证应用程序为目标而设计的。很难将可靠性，安全性和安全性改造成一种从一开始就没有这些目标的语言。

由于C仍将是像Linux内核这样的大型程序的基础语言，我们可以预见两种趋势的共存，以更好地防止C程序中的谬误，其中MISRA C可以发挥作用，并用更安全的语言（如Rust和SPARK Ada）取代C作为部分代码。汽车行业的主要参与者已经开始走上后一条道路，如英伟达和捷太格特。

审核编辑：郭婷