从用户和合约开发者的角度有时候是对立的。比如有些合约有管理员权限，那么从开发者的角度看，有管理员利于后续做一些高权限操作。但是，从用户角度来看，管理员权限过高就意味着更大的风险。所以，当我们把「公平性」也纳入到「安全性」的范畴后，这个问题会变得更加复杂。

于是，一部分区块链信仰者走了一条路，那就是「治理」。

「治理」能解决问题吗？我不确定，但是直觉上，它不能解决安全的根本问题，而且代价很高，远超出「治理派」的估算，而我坚信的是：我们需要基于数学的信任与安全。

我想谈谈形式化验证。

在形式化验证之前，需要给「安全」下一个数学定义。请注意，是数学定义，用严格的形式化逻辑语言来定义的定义。

凡是遇到声称在做形式化验证，或者经过形式化验证的项目，我们需要追问一句，形式化验证了什么？

形式化验证的结果是一个确定性的结果，是一个数学定理！

之前看过一些项目，包括一些大厂，声称做形式化验证，但是闭口不谈验证了什么性质。

这个定理长什么样子呢？我举个例子：

定理 1：对任意的环境 Env，对所有的输入 I，程序 Env |- P(I) 运行得到一个执行行为序列 [B0, B1, B2 ..... Bn]，forall i, Safe(Bi)。

这个定理是可以完整地用数理逻辑来定义的，只是这里我用中文，利于大家理解。

接下来，需要证明：

定理 1：对任意的环境 Env，对所有的输入 I，程序 Env |- P(I) 运行得到一个执行行为序列 [B0, B1, B2 ..... Bn]，forall i, Safe(Bi)。

证明：

…（略）

证毕。

是不是眼熟？和我们初中做数学作业有点类似。

任何形式的形式化验证都会得到这一个定理和证明过程，只不过证明过程有时候是「隐式」的，被一些别的定理所蕴含了，不存在一个明确的表达。

上面定理中的 forall i, Safe(Bi) ， 这里 Safe() 函数怎么定义 可是个大学问。

一种最直观的做法是这么定义 Safe(X)：X 不整数溢出，X 不数组越界，X 没有重入，X ……

但是这样大家会有疑问，这个定义包含的规则是完备的吗？当然不可能完备，总有新的安全漏洞出现。

那么这个 Safe() 定义靠谱吗？当然不靠谱，但是不靠谱不等于不正确。目前的安全审计基本停留在这一层面，只是这个定义不 Sound。

主持人：所以是不是需要发展一些对于 DeFi 场景而言的形式化验证的 best practice，以后的审计效率和安全性就能提升？

郭宇：是的。

其实，Safe() 函数的定义需要的是一个基于互模拟的数学定义，而不是规则的罗列。互模拟在「差分隐私」「多方计算」「零知识证明」「操作系统验证」…… 等等各种形式验证领域都有具体的定义。这里我就不展开了，总之，要给出一个 sound 可靠的 Safe 定义在不同的领域是完全不同的，而且是最困难的。 (责任编辑：admin)