C++中的形式化方法用于安全关键软件

Question

看起来C语言对于在代码中使用的形式化方法具有良好的支持（frama-c、VCC、verifast）。据我所知，C++似乎没有可比较的类似支持。

有哪些形式化方法可用于推理关于采用C++编写的安全关键软件的相关问题？

- willfredthebuel

---

如果您正在编写安全关键软件，您可能需要遵守认证标准并向安全机构负责。这些标准明确说明了他们对您的期望。那是C++代码吗？通常不是，尽管您可以解释为什么认为它是更好的工具。形式化方法？通常也不是，尽管航空新DO-178C标准中有一个附录。在您的情况下适用哪个标准和机构？ - Pascal Cuoq

在我们的情况下，我们正在研究没有任何特定编码标准指导的2类医疗设备，但确实有软件过程标准。在2类和3类设备领域，Misra是一个相当安全的选择，但也不需要正式方法。这个问题与我们未来的开发和学习有关，而不是一个具体的项目。我听说DO178C标准有一个关于正式方法的部分，我已经订购了一本书来了解情况。这是一个后续问题，看看其他人在C++中使用了什么。 - willfredthebuel

你可能需要查看MISRA C++编码准则。有一些静态分析工具支持这个标准。这些工具还有其他的检查器，可以增强MISRA标准的检查。 - Thomas Matthews

我与Frama-C开发团队关系密切，可以说他们正在开发一个C++前端。这是欧盟项目的一部分，该项目还涉及VeriFast也在开发C++前端，并分享了部分资源。有关信息可在http://llvm.org/devmtg/2014-04/PDFs/Posters/FramaC.pdf上找到。 - Pascal Cuoq

Pascal Cuoq - 虽然我很容易同意你应该有一个标准和权威，但通常你并没有。这是一个严重的问题。我见过的一些最糟糕的C++代码在安全关键代码中。 - Mike Crawford

Answer 1

我与一家医疗公司合作，他们使用Coverity和Klocwork检查代码是否存在潜在问题，例如资源泄漏和未初始化指针的使用。

然而，这些只是工具，并非安全关键代码的标准。

我看到MISRA正在制定C++标准。他们早先从C开始，大约5年前开始着手C++。一个大问题是MISRA C++标准规定不得使用模板。这实际上限制了你在C++中所能做的事情。但是，你可以将该文档用作起点。例如，你可能希望将软件中使用的模板限制为标准库和boost。

请注意，Klocwork有一个MISRA C++扩展。

然而，编写良好的代码的最佳方法之一是使用单元测试和集成测试进行测试。多年来，我发现这比大多数其他方法更可靠。

- Alexis Wilke

---

正式方法与MISRA无关。MISRA只是一种编码标准，用于将编程语言简化为安全子集。如果你想要更加严格、应用特定的安全标准，那么就需要同时使用正式方法和编程语言的安全子集。 - Lundin