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采用的第一级称为石头级。它对应于符合 Ada 的 SPARK 子集的代码。仅采用此级别即可保证许多无法对 C 强制执行的一致性属性。其中包括：

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

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

遵守 Ada 和 SPARK 的强类型规则，而不是 C 的“糟糕的类型安全性，允许发生广泛的隐式类型转换，这可能会损害安全性，因为它们的实现定义方面可能会导致开发人员混淆。（MISRA 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 中表示为整数‘最后）。“检查原因”清楚地解释了加法的结果应该适合机器整数，如果 X 是加法前的最大整数值，则情况并非如此。然后，GNATprove 建议向函数 Incr 添加一个合适的前提条件可能会解决这个问题，在这里指定 X 不能是那个最大值。

超越银级的火花

使用SPARK还有更多的好处，远远超出了MISRA C检查器所能提供的。在黄金和白金级别，开发人员通过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 ）替换 C 作为部分代码。

审核编辑：郭婷