MISRA C在安全和安全编程中的位置

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

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

令人惊讶的是，在讨论中根本没有提到 MISRA C，尽管它已成为许多行业的必备工具，以防止 C 语言的错误。MISRA C 于 1998 年作为 C 的编码标准出现，最初用于汽车行业，经过两次修订。当前版本是 MISRA 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、Altran 和 Inria 开发的 SPARK 工具集，它基于四个原则：

基础语言 Ada 通过定义明确的语言标准、强类型和丰富的规范特性为静态分析提供了坚实的基础。

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

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

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

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

SPARK Stone Level - 基本保证

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

使用适当的包系统，而不是 C 使用基于文本的文件包含，并且没有跨翻译单元的一致性要求；

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

遵守 Ada 和 SPARK 的强类型规则，而不是 C 的“较差的类型安全性 ［that］ 允许发生广泛的隐式类型转换 ［which］ 可能会损害安全性，因为它们的实现定义方面可能会导致开发人员混淆。 “（MISRA C:2012，附件 C）

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

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

SPARK 银级 - 强大的安全保障

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

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

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

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

SPARK 超越白银级

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

结论

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

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

由于 C 仍将是 Linux 内核等大型程序的基础语言，我们可以预见两种趋势的共存，以更好地防止 C 程序中的错误，其中 MISRA C 可以发挥作用，并用更安全的语言（如 Rust 和SPARK Ada 用于部分代码。

审核编辑：郭婷