认证程序的定义

Question

我看到了几个不同的研究小组，至少有一本书谈论了使用Coq设计认证程序。关于认证程序的定义是什么，有共识吗？从我所知道的情况来看，它的真正含义是该程序被证明是完整的并且类型正确。现在，程序的类型可能是一些非常奇特的东西，比如列表中有一个非空的证明，所有元素大于等于5，等等。然而，最终，这是一个认证的程序，只是Coq显示的程序是完整的和类型安全的，所有有趣的问题都归结为最终类型中包含的内容？

---

编辑1

基于wjedynak的回答，我看了一下泽维尔·勒罗伊的论文，这在下面的答案链接“现实主义的编译器的形式化验证”。我认为这包含了一些很好的信息，但我认为在这个研究序列中更多的信息可以在Sandrine Blazy和Xavier Leroy的论文Mechanized Semantics for the Clight Subset of the C Language中找到。这是“正式验证”文件增加优化的语言。在其中，Blazy和Leroy展示了Clight语言的语法和语义，然后在第5节中讨论了这些语义的验证。在第5节中，列出了用于验证编译器的不同策略，这在某种意义上提供了概述用于创建认证程序的不同策略。它们是：

1. 手册评论
2. 证明
3. 恪翻译
4. 测试可执行语义
5. 等价语义的性质与替代语义

在任何情况下，有可能可以添加的点，我当然想知道更多。

回到我原来对于认证程序的定义是什么的问题上，对我来说还是有点不清楚。 Wjedynak提供了一个答案，但实际上Leroy的工作包括在Coq中创建一个编译器，然后在某种意义上证明它。从理论上讲，它现在可以证明C程序的一些事情，因为我们现在可以进行C-> Coq->证明。在这个意义上，好像有这样的工作流程，我们可以

1. 在X语言写程序的程序从勒柯克步骤1中或者一些其他证据的辅助工具模型的
2. 形式。这可能涉及在Coq中创建编程语言的模型，或者可能涉及直接创建程序模型（即，在Coq中重写程序本身）。
3. 证明模型的一些性质。也许这是对价值的证明。也许这是证明声明的等价性（例如3 = 1 + 2或f（x，y）= f（y，x）等等）
4. 然后，根据这些证明，将原始程序。

或者，我们可以在证明助手工具中创建一个程序的规范，然后证明规范的属性，但不是程序本身。

无论如何，如果任何人有他们，我仍然有兴趣听取其他定义。

Answer 1

我同意这个概念似乎很模糊，但在我的理解中，一个认证的程序是一个配备的程序/以及正确性的证明。现在，通过使用丰富而富有表现力的类型签名，您可以做到这一点，因此不需要单独的证明，但这往往只是一个方便的问题。真正的问题是我们所说的正确性：这是一个规范问题。你可以看看例如泽维尔乐华。 Formal verification of a realistic compiler。

Answer 2

首先注意到“认证”这个短语具有轻微的法语偏见：其他地方经常使用“已证实”或“已证明”的表达方式。

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

另一个大的验证项目是使用Isabelle/HOL的L4.verified。这部分exposition解释了一些实际陈述和证明的内容，以及后果。不幸的是，实际的证据是绝密的，所以不能公开检查。

Answer 3

它可能意味着没有运行时错误（数值溢出，无效的引用...），这与大多数开发的软件相比已经很好，但仍然很弱。根据域的形式化，其他含义被证明是正确的;也就是说，它不仅必须在形式上不存在运行时错误，还必须被证明能够执行所期望的操作（必须已经精确定义）。

Answer 4

我的理解是，在这个意义上说，“认证”是as Makarius pointed out，这是一个由法语者选择的英语单词，其母语人士可能使用“正式验证”。 Coq在法国开发，拥有许多法语开发者和用户。

至于什么“形式验证”的意思，维基百科notes（许可证：CC BY-SA 3.0），即：

是证明的行为......的预期算法的系统相对于底层有一定的正确性形式规范或财产，使用形式化的数学方法。

（我知道你想比这更准确的定义。我希望以更新以后对这个答案，如果我找到一个。）

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

• 验证： “我们试图做出正确的事情吗？”，即是亲指定用户的实际需求风管？
• 验证：“我们做了我们想做的吗？”，即产品是否符合规格？

的landmark纸seL4: Formal Verification of an OS Kernel（克莱恩，等人。，2009）证实了这一解释：

愤世嫉俗的人可能会说，一个实现证明只能说明 实现具有完全相同的错误，该规范 包含。这是事实：证明并不能保证规范描述了用户期望的行为。 差异[与未验证的方法相比] [ ]是抽象程度和缺少整个类别的错误。

哪些类错误是那些？该阿格达教程gives some idea：

• 没有运行时错误（如I/O错误不可避免的错误进行处理;其他由设计除外）。
• 没有非生产性的无限循环。

Answer 5

经过认证的程序是与一个证据，该方案满足其规格，即，证书成对的程序。关键是存在可以独立于产生证明的工具检查的证明对象。

已验证的程序已经过验证，在此情况下可能通常意味着其规范已经在Coq等系统中正式化并证明是正确的，但证明不一定需要通过外部工具进行验证。

这个区别在科学文献中有很好的证明，并且不是特定于法语者。 Xavier Leroy在A formally verified compiler back-end的第2.2节中非常清楚地描述了它。