NEST 社区开发者 YolkLi 分享 DeFi 开发中需要注意的安全问题，安比实验室郭宇聊到智能合约安全的形式化验证。

原文标题：《Math Show #007 - 深入浅出，如何确保你的 DeFi 资金安全》
整理：Math Show

6 月 23 日晚 7 点，麦子钱包举办了 Math Show 的第 7 期，有幸邀请了 NEST 社区开发者 YolkLi 和 安比实验室 郭宇，特邀主持人链闻研究总监 潘致雄，带大家「深入浅出，如何确保你的 DeFi 资金安全」，以下是当晚的精彩撰录。

主持人：想必大家对最近 DeFi 最近的火热程度有目共睹，除了带了的财富效应之外，大家其实最核心还是最关注「DeFi 资金」的安全性，那么我们先请第一位嘉宾 NEST 社区开发者 YolkLi 给我们带来的分享。

YolkLi：今晚和大家分享一下日常开发中的一些经验。

代码安全

智能合约的开发和传统的开发不同，因为区块链的操作消耗和去中心化特点，代码的质量和安全显得更为突出。大概有三点建议：

1、DeFi 是建立在区块链上的应用，公链（联盟链）底层逻辑或者机制的改变会对 DeFi 应用产生影响，比如 Gas 消耗由于某次改动上升了，导致某个 DeFi 的套利空间不存在了。我们需要关注区块链的发展，尤其是底层的升级对 DeFi 安全性的影响。

2、区块链上的操作是以交易的方式进行的，要保证交易的原子性，交易中所有的操作和影响都要在代码逻辑的覆盖范围内。

3、安全审计，DeFi 面向市场前必须要经过安全审计这步，这是对用户和投资者负责。NEST 目前也在和安比实验室进行 NEST3.0 的审计工作。

跨合约安全

很多业务场景需要用到其他的合约接口，前段时间也出现了很多问题，比如 ERC20 的假充值，ERC 777 重入攻击等。

合约的组合会破坏一笔交易的原子性。举个例子：

一张「竞猜」合约：转入 1 ETH 参与竞猜，正确返回 2 ETH ，错误 1 ETH 就损失掉了。假设竞猜过程公平公正，代码也是安全的。我们理想的逻辑是调用者转入 1 ETH 并且返回结果，赚 1 ETH 或者损失 1 ETH。正常调用没有问题，但是如果用另一张合约调用，并且在合约中实现「没有返回 2 ETH 就交易失败」的逻辑，成本只有一点 gas 费，但是永远不会输。在一段正常逻辑外加了一段新的逻辑，游戏就变得不公平了。

当自己的合约内部用到多张合约组合的结构，需要明确整个交易逻辑的闭环，确保没有额外的方法或者权限可以影响交易逻辑。

需要使用外部合约时，我们假设对方是安全的，两张安全的合约组合后交易的安全性会发生变化，可能会变得不安全，我们需要对组合后的安全性进行分析。或者假设对方是不安全的，我们需要对调用后的逻辑进行限制，对特殊的结果特殊处理，确保自己的业务逻辑不受影响。

风险控制

DeFi 安全是个长期的工程，代码安全是个大前提，同时为了应对未来的安全问题，DeFi 需要有应急流程。我们需要明确知道业务中的风险点在哪，确保在紧急情况最大程度的保证所有人的资金安全。在处理紧急状况依然需要坚持去中心化，这对去中心化的治理是个挑战。

安全最终并不是靠某个项目方或者安全审计团队完成的，应该是一个去中心化的方式。让社区成员或者黑客参与到 DeFi 安全的建设中，并且给予相应的激励。参与的人越来越多，DeFi 的发展才能越来越健壮。

主持人：感谢 YolkLi 的分享，收获颇丰，大家可以慢慢消化，接下来有请我们安比实验室的郭宇继续围绕这个话题分享。

郭宇：DeFi 是由智能合约来构建的，它的安全性包含了以下关键因素：

A. 底层链的安全型：矿工 / 黑客作恶成本与收益，当合约上的资产在不断膨胀后，矿工作恶的动机会逐步加大，多方博弈带来的纳什均衡的转移。

B. 合约平台的安全性：智能合约语言是在动态变化的，编译器也在发展，eth2 还会引入 wasm，这个动态变化过程会引入新的安全不稳定因素，并且带来更大的攻击面。特别是当编译器变复杂之后，也许会有黑客攻击编译器的事件发生，编译器引入的安全漏洞会更加隐蔽，更加难排查。

C. 业务本身的安全性：DeFi 跟外部金融世界是紧密联系的，比如外部没有经过验证的价格，外部的套利行为，DeFi 和 CeFi 之间的互相关联性而带来的攻击手法。

D. 第三方服务的安全性：可组合式的 DeFi 合约的可靠性，接口是否兼容，合约标准的制定比较随意。

单纯从技术角度，区块链安全是前所未有的。区块链项目是「全开放式」的，用户不需要 KYC 就能任意接入，这在传统金融中是完全不可想象的，并且系统的每一个细节都对外暴露。

安全审计是必须要做的，但这并不能从根本上解决问题，问题就是：「审计结果无法量化」。

如果审计报告上列出的 bug 越多，能证明剩下的 bug 越少吗？这有可能是代码质量较差，发现的 bug 多，所以隐藏的 bug 会更多。

可是，如果审计报告上列出的 bug 很少呢？也许是审计不够深入。

其实，我认为这都不是智能合约的终极难题，终极难题是：智能合约到底怎么样算是安全？

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

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

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

我想谈谈形式化验证。

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

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

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

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

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

定理 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 定义在不同的领域是完全不同的，而且是最困难的。

定义好安全性之后，我们验证的对象是什么？这里可以分为模型级别验证和代码级别验证。但是不管怎么验证，我们需要对验证的代码写出「规范」，从上面的例子延伸：

Solidity 开发语言里面有一个 方法 A(i)，输入 i，输出 B;

形式化验证就是，根据方法 A(i) 产生另一个方法，也输入 i，得到 B。这就证明了方法 A 是 OK 的。

这就是在验证一个行为满足规范。

那么这个验证过程，可以是自动化的，半自动化的，也可以是人工的。但是形式化验证很快会面临一个很困难的新问题：如果代码量很大怎么办？如果代码会频繁改动怎么办？

这是过去二十年，形式化验证领域的研究热点，就是如何把代码拆成很多的模块，然后实现验证的模块化，这里面的理论难度深不见底。

这里我来谈谈最后一个形式化验证的难题，这就是工具悖论。假如，我们把代码验证完了，借助了一个工具。那么问题来了，这个工具的安全性怎么来保证？为了验证这个工具，我们又需要一个新工具。

有一类形式化验证，会产生「Proof Term」，也就是具体的验证过程的表达。

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

证明：

…「Proof Term」（略）

证毕。

也就是中间那个非常庞大的证明过程，它可以摆脱对验证工具的信任依赖，类似于区块链中我们不需要信任矿工一样。我们可以借助各种先进的验证证明产生工具，只要他们能产生对的证明，他们本身是否安全不重要，这是一种很本质的新的去中心化技术。

形式化验证是银弹吗？

并不是。

挑战一：成本很高，需要很多的智力投入。

挑战二：需要理论上的重大突破，提高逻辑的自动推理能力。

挑战三：一方面我们需要更复杂的 DeFi 功能！另一方面，复杂理论的验证方法更难。

验证技术与技术创新存在一个赛跑，目前来看，验证技术远远落后于技术的发展，Fuzzing，符号执行，人工审计，动态监控，应急预案，这些传统的技术需要和先进形式化验证技术一起使用。

主持人：在未来的 3-5 年内，我们有没有可能通过 Etherscan 等区块链浏览器上一个通过形式化验证的标记来确认该智能合约的安全性？

郭宇：对于简单的智能合约是很有希望的，比如 ERC20 的 token 合约 。但是对于超过 2000 行的智能合约，难度就会加大很多。其实我们不能仅关注「打勾」，而是需要看形式化验证的那个最终定理是否是有意义的，或者说是否 sound。并且可能出现今天打了勾，明天就发现问题，需要取消，所以其实需要制定标准。这个未来需要一个社区，有专家，有用户，有黑客，大家一起来建设，3 年有点短，5 年也许有希望，建议采取学术界的同行评议机制。

智能合约非常特殊，难度更大，传统软件的形式化验证开源工具是有的，智能合约这边其实进展很小。但是，其实目前形式化验证的自动化能力非常弱，大家能看到的只能做到「找 bug」 这种程度，不能保证「无 bug」。

主持人：请问 NEST 预言机与 Chainlink 预言机有什么不同？

YolkLi：NEST 价格预言机是「直接」预言机方案：通过矿工双边报价、验证者吃单套利的方式在链上直接生成价格。通俗来讲，NEST 预言机报价矿工在用真金白银证明自己的报价，如果验证者觉得该价格与市场价格之间有偏差，那就可以吃单套利。最终，NEST 预言机在链上生成的价格都是能够代表市场公允价格的。

这种机制的亮点在于价格在链上可以被市场验证。或者是分布式验证，任何一个人都可以成为价格的验证者。

Chainlink 的预言机方案需要相信 Chainlink 的节点。使用 NEST 预言机需要相信市场的验证（共识）。

主持人：DeFi 领域的多起安全事件给整个区块链行业敲响了安全的警钟。现阶段的 DeFi 不光有安全问题，还有很多其他的痛点，能否从公链和应用的角度，谈一下对于 DeFi 迫切需要解决的有哪些问题？面对日益严峻的安全挑战安比将怎样应对？

郭宇：我觉得有两点需要做，

第一个是：可组合性的 DeFi 的接口需要进行更细致的分析和行为披露，可组合性的风险还是比较大；

第二个是：智能合约安全需要一个更广泛更积极的社区参与，可以参考 DAO。

安比的使命是探索新的技术，来提升区块链系统的安全性，实现基于数学而不是基于专家权威的安全性。

主持人：2019 年以来 DeFi 市场发展火热，据 DeFipulse 统计，当前 DeFi 市场整体锁仓规模已突破 10 亿美元，较去年同期增长 362%。那么请问您怎么看待 DeFi 这一热门领域？NEST 是否有布局去中心化金融的打算呢？

YolkLi：我非常看好 DeFi 的未来发展，这是一个数以万亿计规模的开放式金融市场。我们希望 NEST 预言机能够给下游 DeFi 提供高度确定性的链上价格数据。

就 NEST 开发者小组来说，更多的是以分布式的方式去维护好 NEST 预言机。有关 DeFi 的研发，我们也在做，而且投入了很多的精力。NEST 是个开放的预言机网络，更重要的是吸引更多的开发者和项目方使用 NEST。

主持人：非常感谢参与今晚 Math Show #007 活动的「show」友们， 也感谢两位嘉宾带来的分享，想必大家对「 DeFi 资金安全」有一定的认知和了解。