预言机 [AMA] 深入浅出,如何确保您的 DeFi 资金安全

very599 · 2020年06月24日 · 96 次阅读
本帖已被设为精华帖!

6月23号 19:00 Math Show#007将带你”深入浅出,如何确保您的DeFi资金安全
本期主咖:安比实验室 郭宇
NEST社区开发者 YolkLi
本期特邀主持人:链闻研究总监 潘致雄
以下为AMA分享内容:


Nest社区开发者 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 的发展才能越来越健壮。


链闻研究总监 潘致雄:
看起来智能合约的安全和审计是一个复杂的系统化工程,非常厉害。

链闻研究总监 潘致雄:
接下来有请我们安比实验室的郭宇继续围绕这个话题给我们带来的分享

安比实验室 郭宇:
我今天分享几个关于 DeFi 安全的观点,都是自己的思考,请大家指正。
我们知道,DeFi 是由智能合约来构建的。智能合约是个新生事物,但是已经展现出巨大的威力,短短几行代码就操控了天价的资产。智能合约给大家的印象可能是各种漏洞,各种bug。不过这是任何一个新生事物都要走的过程,从会爬到会走路,需要时间来成长。
而 DeFi 是一个更新的事物,他的安全性从一出现就得到了大家的重视。DeFi 的安全因素特别多,不仅仅包括一些常见的安全漏洞,比如整数溢出啊,代码重入啊。这只是冰山一角。
DeFi 的安全性其实还依赖了很多大家可能没有关注到的地方。

第一个就是底层链的安全性
这两天有个比较热的说法,就是当以太坊上的合约资产金额大于原生资产之后,也许安全性就会受到威胁。这确实是一个问题,矿工与黑客的作恶成本与收益的比,永远是一个关键点,当合约上的资产在不断膨胀后,矿工作恶的动机会逐步加大,这种博弈关系的均衡态会变化。

第二个是合约平台本身的安全性
智能合约语言是在动态变化的,编译器也在发展,eth2还会引入wasm,这个动态变化过程会引入新的安全不稳定因素,并且带来更大的攻击面,特别是当编译器变复杂之后,也许会有黑客攻击编译器的事件发生,编译器引入的安全漏洞,会更加隐蔽,更加难排查,图灵奖得主 Ken Thompson 很早就演示了编译器漏洞的可怕性。

第三个因素是 业务本身的安全性
这个主要是 DeFi 跟外部金融世界是紧密联系的,比如外部没有经过验证的价格,外部的套利行为,DeFi 和 CeFi 之间的互相关联性而带来的攻击手法。

这三个因素可能是很多 DeFi 项目没有考虑过,但是未来风险比较高的几点。

接下来,我沿着[ 有审计了 ,足够安全了吗] 的问题,讨论下如何保障安全性。单纯从技术角度,区块链安全是前所未有的,「前所未有的挑战」。
为什么这么说,因为区块链项目是「全开放式」的,用户不需要 KYC 就能任意接入,这在传统金融中,是完全不可想象的,并且系统的每一个细节都对外暴露,安全审计是必须要做的,但是安全审计并不能从根本上解决问题,这个问题就是:「审计结果无法量化」。
大家想想,如果审计报告上列出的bug越多,能证明剩下的bug越少吗?
这有可能是发现的bug多,所以代码质量较差,所以隐藏的bug会更多。可是,如果审计报告上列出的bug很少呢?也许是审计不够深入。其实,我认为,这都不是智能合约的终极难题,终极难题是:智能合约到底怎么样算是安全?从用户和合约开发者的角度有时候是对立的。比如有些合约有管理员权限,那么从开发者的角度看,有管理员利于后续做一些高权限操作。
但是,从用户角度来看,管理员权限过高就意味着更大的风险。
所以,当我们把「公平性」 也纳入到「安全性」的范畴后,那么,这个问题会变得更加复杂。可能跟到这里,大家有点绝望啊。
于是,一部分区块链信仰者走了一条路,那就是「治理」。
「治理」能解决问题吗?我不确定,但是直觉上,它不能解决安全的根本问题,而且代价很高很高,远超出「治理派」的估算。而我坚信的是:我们需要基于数学的信任与安全。


链闻研究总监 潘致雄:
从这个角度来说,DeFi还是有些好处的,就是DeFi的规则是公开的,你觉得有问题可以不来玩嘛

安比实验室 郭宇:
嗯,这里其实有个信息不对称的问题,这是个哲学问题 。
我想谈谈形式化验证。怎么算是形式化验证,网上的科普文章非常非常少,而且大家也都很好奇。
首先,说明一下,在形式化验证之前,需要给「安全」下一个数学定义。请注意,是数学定义,用严格的形式化逻辑语言来定义的定义。凡是遇到声称在做形式化验证,或者经过形式化验证的项目,我们需要追问一句, 形式化验证了什么。形式化验证的结果是一个确定性的结果,是一个数学定理!之前看过一些项目,包括一些大厂,声称做形式化验证,但是闭口不谈验证了什么性质,不谈验证的定理就是耍 。
这个定理长什么样子呢?
我胡乱写一个,便于大家理解。定理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 定义在不同的领域是完全不同的,而且是最困难的。

nestFans_拾二:
是不是可以理解为:Solidity 开发语言里面有一个 方法A(i),输入i,输出 B;形式化验证就是,用另一种方法,也输入i,得到 B。这就证明了方法 A 是 OK 的。可以这么理解吗?

安比实验室 郭宇:
可以啊,我正好讲到这里了,定义好安全性之后,我们验证的对象是什么? 这里可以分为 模型级别验证和代码级别验证。但是不管怎么验证,我们需要对验证的代码写出「规范」,刚才的例子就是在验证一个行为满足规范。那么这个验证过程,可以是自动化的,半自动化的,也可以是人工的。但是很快,形式化验证会面临一个很困难的新问题:如果代码量很大怎么办,如果代码会频繁改动怎么办。这是过去二十年,形式化验证领域的研究热点,就是如何把代码拆成很多的模块,然后实现验证的模块化。
ok,我来谈谈最后一个形式化验证的难题,这就是工具悖论。假如,我们把代码验证完了,借助了一个工具。那么问题来了。这个工具的安全性怎么来保证?
为了验证这个工具,我们又需要一个新工具,所以,这是很多初次接触形式化验证的人的一个问题,这个问题非常好。有一类形式化验证,会产生「Proof Term」,也就是具体的验证过程的表达。
定理1:
对任意的环境 Env,对所有的输入 I,程序 Env |- P(I) 运行得到一个执行行为序列[B0, B1, B2 ..... Bn],forall i, Safe(Bi)。
证明:
。。。「Proof Term」(略)
证毕。
就是中间那个非常非常庞大的证明过程,然后可以摆脱对验证工具的信任依赖。好比,区块链中我们不需要信任矿工一样。我们可以借助各种先进的验证证明产生工具,只要他们能产生对的证明,他们本身是否安全不重要。这是一种很本质的新的去中心化技术。

最后总结一下
形式化验证是银弹吗?并不是

挑战一:成本很高,需要很多的智力投入。
挑战二:需要理论上的重大突破,提高逻辑的自动推理能力。
挑战三:一方面我们需要更复杂的DeFi功能!另一方面,复杂理论的验证方法更难!
验证技术与技术创新存在一个赛跑。目前来看,验证技术远远落后于 技术的发展。Fuzzing,符号执行,人工审计,动态监控,应急预案,这些传统的技术需要和先进形式化验证技术一起使用。


nestFans_拾二:
这个好像也符合事务发展的逻辑吧,只有新技术出现了,才会有验证技术跟上来。

安比实验室 郭宇:
还有一点是,只要资源足够多,验证技术是能赶上来的。

链闻研究总监 潘致雄:
在未来的3-5年内,我们有没有可能通过Etherscan等区块链浏览器上一个通过形式化验证的标记来确认该智能合约的安全性?

安比实验室 郭宇:
对于简单的智能合约是很有希望的,比如 ERC20 的token合约。但是对于超过2000行的智能合约,难度就会加大很多。其实我们不能仅关注「打勾」,而是需要看形式化验证的那个最终定理是否是有意义的,或者说是否 sound。
这个未来需要一个社区,有专家,有用户,有黑客,大家一起来建设。3年有点短,5年也许有希望,建议采取学术界的 同行评议机制。授「权」都会是有问题的,而且可能出现今天打了勾,明天就发现问题,需要取消,这就需要制定标准。其实目前形式化验证的自动化能力非常弱,大家能看到的只能做 到「找bug」 这种程度,不能保证「无bug」。

链闻研究总监 潘致雄:
请问NEST预言机与Chainlink预言机有什么不同?

Nest社区开发者 YolkLi:
NEST 价格预言机算是直接预言机方案。通过矿工双边报价、验证者吃单套利的方式在链上直接生成价格。通俗来讲,NEST 预言机报价矿工在用真金白银证明自己的报价,如果验证者觉得该价格与市场价格之间有偏差,那就可以吃单套利。最终,NEST预言机在链上生成的价格都是能够代表市场公允价格的。
这种机制的亮点在于价格在链上可以被市场验证。或者是分布式验证,任何一个人都可以成为价格的验证者。
这点很重要,Chainlink的预言机方案需要相信Chainlink的节点,使用NEST预言机需要相信市场的验证(共识),这个是最核心的区别。

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

安比实验室 郭宇:
第一个是:可组合性的DeFi的接口需要进行更细致的分析和行为披露,可组合性的风险还是比较大。
第二个是:智能合约安全需要一个更广泛更积极的社区参与,可以参考DAO。
安比的使命是探索新的技术,来提升区块链系统的安全性,实现基于数学而不是基于专家权威的安全性。

链闻研究总监 潘致雄:
最后一个问题,2019年以来DeFi市场发展火热,据DeFipulse统计,当前DeFi市场整体锁仓规模已突破10亿美元,较去年同期增长362%。那么请问您怎么看待DeFi这一热门领域?NEST是否有布局去中心化金融的打算呢?

Nest社区开发者 YolkLi:
我非常看好 DEFI 的未来发展,未来会是以万亿计规模的开放式金融市场。我们希望 NEST 预言机能够给下游 DEFI 提供高度确定性的链上价格数据。就 NEST 开发者小组来说,更多的是以分布式的方式去维护好 NEST 预言机。有关 DEFI 的研发,我们也在做,而且投入了很多的精力。NEST是个开放的预言机网络,更重要的是吸引更多的开发者和项目方使用NEST。
共收到 0 条回复
molingye 将本帖设为了精华贴 06月24日 11:24
需要 登录 后方可回复, 如果你还没有账号请点击这里 注册