18

我看到几个不同的研究小组，以及至少一本书，都在谈论使用 Coq 来设计认证程序。对于认证项目的定义是否有共识？据我所知，它真正的意思是程序被证明是完全的并且类型正确。现在，程序的类型可能是非常奇特的东西，例如证明它是非空的、已排序的、所有元素 >= 5 等的列表。但是，最终，它是一个经过认证的程序，只有 Coq 显示的是完全的和类型安全的，所有有趣的问题都归结为最终类型中包含的内容？

编辑 1

根据 wjedynak 的回答，我查看了 Xavier Leroy 的论文“Formal Verification of a Realistic Compiler”，该论文链接在下面的答案中。我认为这包含了一些很好的信息，但我认为可以在Sandrine Blazy 和 Xavier Leroy的论文Mechanized Semantics for the C 语言的 Clight 子集中找到更多信息。这是“形式验证”论文添加优化的语言。在其中，Blazy 和 Leroy 介绍了 Clight 语言的语法和语义，然后在第 5 节讨论这些语义的验证。在第 5 节中，列出了用于验证编译器的不同策略，. 这些是：

  1. 人工审核
  2. 证明语义的性质
  3. 已验证的翻译
  4. 测试可执行语义
  5. 与替代语义等价

无论如何，可能有几点可以补充，我当然想了解更多。

回到我最初的问题，即认证程序的定义是什么，我仍然有点不清楚。Wjedynak 提供了一个答案，但实际上 Leroy 的工作涉及在 Coq 中创建一个编译器，然后在某种意义上对其进行验证。理论上，现在证明关于 C 程序的事情成为可能，因为我们现在可以进行 C->Coq->proof。从这个意义上说，似乎有这个工作流程我们可以

  1. 用X语言编写程序
  2. Coq 或其他证明辅助工具中步骤 1 中程序模型的形式。这可能涉及在 Coq 中创建编程语言模型，也可能涉及直接创建程序模型（即在 Coq 中重写程序本身）。
  3. 证明模型的一些性质。也许这是对价值观的证明。也许这是陈述等价性的证明（诸如 3=1+2 或 f(x,y)=f(y,x) 之类的东西。）
  4. 然后，根据这些证明，调用认证的原始程序。

或者，我们可以在证明辅助工具中创建程序的规范，然后证明关于该规范的属性，而不是程序本身。

无论如何，如果有人有替代定义，我仍然有兴趣听到它们。

4

5 回答 5

7

我同意这个概念似乎含糊不清，但在我的理解中，经过认证的程序是配备/连同正确性证明的程序。现在，通过使用丰富且富有表现力的类型签名，您可以做到这一点，因此不需要单独的证明，但这通常只是为了方便。真正的问题是我们所说的正确性是什么意思：这是一个规范问题。你可以看看例如 Xavier Leroy。一个现实的编译器的形式验证。

于 2014-01-24T15:58:26.610 回答
6

首先请注意，“已认证”一词带有轻微的法国偏见：在其他地方，经常使用“已验证”或“已证明”的表述。

无论如何，重要的是要问这实际上意味着什么。X. Leroy 和 CompCert 是一个很好的起点：这是一个关于 C 编译器验证的大项目，Leroy 总是热衷于向他的听众解释验证为何重要。尤其是在与“认证机构”的人交谈时，他们通常意味着测试，而不是证明。

另一个大型验证项目是使用 Isabelle/HOL的L4.verified 。说明的这一部分稍微解释了实际陈述和证明的内容，以及后果是什么。不幸的是，实际证明是绝密的，因此无法公开检查。

于 2014-02-02T22:17:25.263 回答
2

认证程序是与程序满足其规范的证明（即证书）配对的程序。关键是存在一个可以独立于生成证明的工具进行检查的证明对象。

一个经过验证的程序已经过验证，在这种情况下，这通常意味着它的规范已经被形式化并在像 Coq 这样的系统中被证明是正确的，但证明不一定由外部工具认证。

这种区别在科学文献中得到了很好的证明，并不是法语国家特有的。Xavier Leroy 在A正式验证的编译器后端的第 2.2 节中非常清楚地描述了它。

于 2017-08-02T15:30:32.227 回答
1

我的理解是，正如 Makarius 指出的那样，从这个意义上说，“认证”是法语国家选择的一个英语单词，而母语人士可能会使用“正式验证”。Coq 是在法国开发的，拥有许多讲法语的开发人员和用户。

至于“形式验证”是什么意思，维基百科指出（许可证：CC BY-SA 3.0）它：

是使用形式化的数学方法，证明系统所基于的预期算法相对于某种形式化规范或属性的正确性的行为。

（我意识到您想要一个比这更精确的定义。如果我找到一个，我希望将来更新这个答案。）

维基百科特别指出了验证和验证之间的区别：

  • 验证： “我们是否在努力做出正确的事情？”，即产品是否符合用户的实际需求？
  • 验证： “我们做了我们想要做的吗？”，即产品是否符合规格？

具有里程碑意义的论文seL4：OS Kernel 的正式验证（Klein 等人，2009）证实了这一解释：

愤世嫉俗的人可能会说实现证明只表明实现与规范包含的错误完全相同。这是真的：证明并不能保证规范描述了用户期望的行为。[在经过验证的方法中与未经验证的方法相比] 的区别在于抽象程度和不存在整类错误。

这些是哪些类别的错误？Agda 教程给出了一些想法：

  • 没有运行时错误（处理 I/O 错误等不可避免的错误；其他错误被设计排除在外）。
  • 没有非生产性的无限循环。
于 2017-08-01T20:47:35.163 回答
0

这可能意味着没有运行时错误（数字溢出、无效引用……），与大多数开发的软件相比，这已经很好，但仍然很弱。根据域形式化证明其他含义是正确的；也就是说，它不仅必须在形式上没有运行时错误，还必须证明它可以完成预期的工作（必须已经精确定义）。

于 2014-04-20T03:33:09.267 回答