智能合约和形式验证

在之前一篇关于人工智能的文章（ ）中，我指出了“自动编程”的不可能性。 今天想聊一个相关的话题：以太坊式智能合约的形式化验证。 有人声称基于“深度学习”实现智能合约的自动形式化验证，确保合约的正确性。 但是，今天我要告诉大家的是，和自动编程一样，全自动的合约验证也是不可能的。

随着区块链技术的愈演愈烈，不少人开始对以太坊的“智能合约语言”做文章。 其中一些是从事PL的人。 他们试图对用Solidity等语言编写的智能合约进行形式化验证 ，声称用严格的数理逻辑方法自动验证智能合约的正确性。 其中一种方法是利用“深度学习”，在训练后自动生成霍尔逻辑的“前置条件”和“后置条件”。

霍尔逻辑

我好像把你弄糊涂了……让我们从 Hoare Logic 开始吧。

Hoare Logic() 是一种形式验证方法，用于验证程序的正确性。 它的做法是先在代码上标注一些“前置条件”和“后置条件”（pre-conditions and post-conditions），然后进行逻辑推理来验证代码的一些基本属性，比如balance after转移是正确的。

举一个非常简单的霍尔逻辑例子：

{x=0} x:=x+1 {x>0}

意思是如果一开始x等于0，那么执行x:=x+1后，x应该大于0。这里的前置条件是x=0，后置条件是x > 0。如果x从0开始，执行x:=x+1后，x会大于0，所以这段代码是通过验证的。

Hoare Logic的系统将所有这些前置条件和后置条件以及代码串联起来，经过逻辑推导和验证，可以做出这样的保证：当前置条件满足时，代码执行后，后置条件必须是真实的。 如果满足所有这些条件，系统将认为这是“正确的程序”。 注意，这里所谓的“正确”完全是由人决定的，系统并不知道“正确”是什么意思。

Hoare Logic在程序安全方面确实可以起到一定的作用，已经应用到一些实际项目中。 例如，在Microsoft Windows的驱动程序代码中，有一种名为SAL的“安全标记语言”EVM可以运行比特币脚本吗，它实际上是Hoare Logic的一种实现。 但是，前置条件和后置条件是什么，必须自己在代码中标注，否则系统无法运行。

比如上面的例子，系统怎么知道我想要属性“x>0”呢？ 只有我自己写。 所以要使用Hoare Logic，就必须在代码上标注很多前置条件和后置条件。 如何写出这些条件，需要深刻理解编程语言和形式逻辑的原理。 这项工作需要训练有素的专家，并且需要花费大量时间。

无法自动生成标注

所以即使有了Hoare Logic，程序验证也不是一件容易的事。 于是有人趁火打劫，提出了类似减肥药的想法，声称要用“深度学习”对已经标注好的代码进行学习，最后让机器自动标注这些前置条件和后置条件。 还处于“幻想”阶段，但已经将“自动标注”作为其“优势”写入了白皮书：“我们的方法是自动的，其他项目是手动的……”

可惜的是，“自动标注”其实和“自动编程”一样是天方夜谭。 自动编程的困难在于机器无法知道你想做什么。 同理，自动标注的难点在于机器没有办法知道你想让代码满足什么属性。 这些信息只存在于你的心中。 如果你不表达，其他人或机器都不会知道。

除非你把它写出来，否则机器永远不知道函数的参数应该满足什么条件（前置条件），也不知道函数的返回值应该满足什么条件（后置条件）。 比如上面的例子，程序执行完之后机器怎么知道你想让x大于0呢？ 除非你告诉它，否则它无法知道。

你可能会问，深度学习就没有帮助了吗？ 想想看……你可以给一个深度学习系统数千万行已经标记好的代码。 你可以把整个Windows系统、整个Linux系统、FireFox的代码，加上一些战斗机、飞船的代码，输入到深度学习系统中进行“学习”。 现在问问系统，我接下来要写一个新的功能，你知道我要做什么吗？ 你知道我希望它满足什么属性吗？ 你还不知道！ 只有我知道：这是用来铲我猫的便便的：p

因此，用深度学习来自动标记霍尔逻辑的前后条件，就像“自动编程”一样，是在试图实现“读心术”，这显然是不可能的。 作为经验丰富的 PL 和形式验证专家，这些人应该知道这不能自动完成。 他们想出了这样一个想法，并把它作为一个优于其他智能合约项目的优势，当然，只是为了愚弄外行，为了发行硬币和收钱；）

如果可以利用深度学习生成前置条件和后置条件，从而完全自动验证程序的正确性，那么这种方法早该在形式化验证领域被炒了。 每个形式验证专家都希望能够完全自动地证明程序的正确性，但他们早就知道这是不可能的。

设计一种语言告诉机器我们想要什么，什么叫“正确”，这本身就是PL专家和形式验证专家的工作。 语言设计好之后，我们还是要靠优秀的程序员来写这些代码，告诉机器我们要做什么。 我们不得不依靠优秀的安全专家，给代码加上前置条件和后置条件的注解，告诉机器什么叫“正确安全的代码”……这一切都必须人工完成，机器无法自动完成.

当然，我也不排除在智能合约中手动添加Hoare Logic标记的可行性，具有一定的价值。 只是想提醒大家，这些标签必须手动编写，不能自动生成。 另外，虽然工具可以起到一定的辅助作用，但是如果编写代码的人不小心，并不能保证程序是完全正确的。

如何保证智能合约的正确性？ 这和保证程序的正确性是一样的问题。 只有知道如何编写干净简单的代码并进行严谨的思考，我们才能编写正确的智能合约。 您可以参考我之前的一些文章，了解如何编写干净、简单、严谨和可靠的代码。

做智能合约验证工作或许能赚钱，但很无聊，没有成就感。 为此，我拒绝了几个与区块链相关的合作项目。 虽然我对区块链的其他一些想法很感兴趣（比如去中心化的共识机制），但我并不看好智能合约的正确性验证。

智能合约是一个神话

事实上，我认为智能合约的整个概念是不可靠的，是一个很大的误解。 在比特币和以太坊系统中，根本不应该有脚本语言，也没有存在的必要。

比特币解锁脚本的执行方式一开始就存在低级错误，导致注入安全漏洞。 用户可以编写恶意代码，导致脚本运行系统出错。 比特币最初的解锁方式是将两段代码（解锁脚本+锁定脚本）以文本形式拼接在一起，然后执行。 以文本方式处理程序是编程语言实现方式的大忌。 稍有经验的黑客都知道，这里很可能存在可攻击点。

以太坊的 Solidity 语言从一个低级错误开始，导致价值 5000 万美元的以太币被盗。 以太坊的智能合约系统消耗了大量的计算资源，同时也会造成严重的性能问题。

虽然比特币和以太坊的作者很可能是密码学和分布式系统领域的大师，但我不得不坦白承认他们都是 PL 门外汉 :p 但是，如果他们是这些语言的专家会不会更好？ 我不这么认为。

第一个问题是PL领域充满了各种宗教，还有许多传教士。 一般的PL专家都会把问题复杂化，他们会在自己的“信仰”中努力设计出完美的语言EVM可以运行比特币脚本吗，而不顾他人的死活。 如果你运气不好，你会遇到那种谈论“纯函数”、单子、依赖类型、线性逻辑的极客……然后就没有人会使用设计的语言了：p

负责任的 PL 科学家一开始就尽量避免创造新语言。 如果不用新语言也能解决问题，就不要设计新语言，系统中也尽量不要使用嵌入式语言。 所以，如果我设计了比特币，我根本就不会为它设计语言。

允许用户编程是危险的！ 很少有用户能够编写出正确可靠的代码，开发出没有错误的语言系统是非常罕见的。 错误的语言系统设计会给黑客以编写恶意脚本进行破坏的可乘之机。 从来没有任何一种语言及其编译器、运行时系统从一开始就是正确的，并且需要很多年才能稳定下来。 此外，你还得考虑性能问题，这对于去中心化的分布式系统来说就更难了。 这对于普通语言来说问题不大，你不需要用它来控制飞行器。 然而，数字货币系统的语言几乎不允许出现这样的问题。

所以与其心存恐惧地设计这些智能合约语言，还不如压根就没有这个功能。

我们真的需要那些脚本的功能吗？ 比特币虽然有脚本语言，但其实常用的脚本不超过5种，直接输入硬编码即可。 虽然以太坊的白皮书提出了那么多应用前景，但是在EVM上有没有有价值的应用呢？ 我认为我们不需要这些智能合约。 数字货币只要做好一件事，能够安全高效的作为货币使用，就已经很好了。

美元、人民币、黄金……有合约功能吗？ 不是，为什么数字货币一定要绑定这个功能？ 我觉得这违背了模块化设计的原则：一个东西只做一点点，把它做到最好。 数字货币应该像货币一样，只需要能够实现简单的转账和兑换功能即可。 合约应该是另一个独立的系统，不应该与货币捆绑在一起。

合同呢？ 留给律师和会计师，或使用单独的系统。 你有没有想过为什么世界上的法律制度不是由程序控制自动执行的？ 为什么我们需要律师和法官，而不仅仅是机器人？ 为什么有些国家的法院仍然需要陪审团，而不是仅仅根据法律条款来审判案件？ 这不仅仅是历史遗产。 你需要了解法律的本质，才能明白没有人为干预的机械化执法是行不通的。 智能合约是把人从系统中彻底剔除，那会出问题。

期望太多的功能实际上是一种过度工程。 花精力去折腾智能合约系统，可能会大大延迟数字货币被世界接受的时间。 老实说，在尝试了多种数字货币并了解了它们使用的技术之后，我发现这些技术非常有趣。 不过，这些数字货币还处于试验阶段，距离真正用作货币还有一定距离。 专注于改善它们作为货币的功能将加速它们被其他人采用。 但是花精力去研究智能合约，我觉得是误入歧途。

在这一点上，我认为比特币比它的后继者（比如以太坊）更真实。 虽然比特币也有脚本语言，但并不过分强调此类脚本的作用。 比特币的脚本语言非常简单而且不是图灵完备的。 这迫使用户编写功能简单、不损害系统性能且易于验证的脚本。 相比之下，以太坊花了太多精力折腾智能合约，使其过于复杂，导致各种问题，影响了最重要的货币功能的接受。

说到这里，可能很多人会觉得我对数字货币不屑一顾，但其实恰恰相反：）我打心底里对区块链技术感兴趣，只是觉得智能合约是多余的麻烦。 虽然被一些人炒作过头了，拿它来胡闹的人也不少，但比特币的技术确实有相当大的价值。 比特币巧妙地解决了分布式计算领域的几个重要且有趣的问题（如拜占庭将军问题）。 他们的解决方案给了我很多启发，我觉得这些想法可以有很多应用场景。 所以我感谢 Satoshi 发明了这个东西 :)

来源：