《Formal Analysis of Composable DeFi Protocols》组合型DeFi项目的形式化验证
2021-05-29

前言

Palina Tolmach的《组合型Defi项目的形式化验证》(Formal Analysis of Composable DeFi Protocols)论文原文链接如下https://arxiv.org/pdf/2103.00540.pdf

论文尝试使用形式化验证的方法,分析Defi智能合约项目应符合的安全约束。 帮助项目开发人员进行自动化的安全审计。

  • 会翻译得口语一些;
  • 部分术语将不会翻译,比如Protocol、token、pool啥的;
  • CSP#Process会翻译成动作而非行为过程,因为我觉得动作更口语一些。
  • requirement 翻译成约束。表1中的property也翻译为约束

3 方法论

3.1 Protocol形式化建模

在这一部分,我们定义Dex和Loaning的关键模块token和pool。
通过关注状态改变,token和pool的行为可以被形式化的建模。
本小节主要记录一下如何建模。

我们用CSP#中的全局变量global varibles来描述用户状态、外部合约状态、链环境变量(如block.number)。
用CSP#中的process来描述token或pool的函数。
为什么这么表示可以参考Bartoletti, M., Chiang, J.H., Lluch-Lafuente, A.: Sok: Lending pools in decentralizedfinance (2020)
假设有一组用户 UU,一组Token TT.
除了链原生代币ETH外,Defi项目中使用到的大部分Token是按照ERC20标准实现的。ERC20代币通过特定接口完成铸币等行为,这些行为均会触发相应的Event。我们将依据这些Event来进行形式化建模。
比方说token的定义如下:

Definition 1 (Token):
有token t ∈ TT, t是一个tuple(U,TS,B,A,F)tuple(U,TS,B,A,F)
其中
UU是用户的集合,
TSZ>0TS∈Z>0 是 token的总发行量totalSupply
B:UZ>0B:U→Z>0 是 保存了 {user:balance} 的 mapping
A:U×UZ>0A:U×U→Z>0 是 allowances,user1 允许 user2 transferFrom的额度。
FF 是 可以修改AABBTSTS的所有函数的集合,如approve(),transfer(),transferFrom(),mint(),burn()

当给出 token t ∈ TT, 我们可以用t.TSTS表示总发行量。其他参数也是一样。综上我们可以得到等式:

t.TS=uUt.B(u)t.TS=\sum_{u∈U}t.B(u)

Definition 2 (Pool):
有pool p P\in P, p是一个tuple(TP,TPR,FP)tuple(T_P,T_P^R,F_P)
其中
TPTT_P \subset T 是 p中包含的token集合。
TPRTT_P^R \subset T 是 p中包含的所有流动性凭证LPToken的集合。
FPF_P 是 所有能改变TPT_PTRPT_R^P的函数的集合。f FP\in F_P可以表示为

{(TP×TPR)(TP×TPR)}i\{(T_P×T_P^R) → (T_P×T_P^R)\}_i

在这里插入图片描述

Defi项目中的TPRT_P^R 一般被用来刺激交易、投资、借贷行为。
有些Defi项目的TPRT_P^R一般表示所有者拥有一定量的两三种Token,
也有些项目允许用户只抵押一种Token,即可获得TPRT_P^R
但总的来说,所有项目中的TPRT_P^R都意味着,流动性提供者可以赎回抵押的Token并获得一定奖励。

同时,为了模拟ethereum中的原子性交易,我们规定上文中提到的所有FF均为原子性操作。不可逆、不可并发、不可交错。

3.2 如何处理Protocol的组合

这一小节将介绍如何形式化描述Protocol和user之间 和 Protocol和Protocol之间的交互。
这两个情景,都限定是sender支付一些token到Protocol中,同时从Protocol中转出来一些token。
Protocol和user之间这个场景为例,
我们在描述一连串有序执行的动作(process)时,用;间隔。每一个动作都对应一个被用户调用的FF
如下图,我们来描述Curve中用户deposit的动作。
在这里插入图片描述

有些动作之间没有严格的执行顺序,完全取决于用户本人想按照什么顺序来执行。对于这些可交错进行的动作,我们用 ||| 间隔,如下图:
在这里插入图片描述

另一方面,我们以相同的思路来描述 Protocol和Protocol之间的交互。
我们把Protocol与Token合约,Protocol与Protocol合约之间的外部调用函数定义为原子动作。

译者注: 比如MasterChef 中 有函数deposit调用unsiwap.addLiquidity,那这一步deposit被认为有原子性,类似于上文中Curve_Depositor()这种不可拆分的动作。

4 评估

本小节将通过实际的项目(Curve和Compound.Finance)来测试评估一下我们的理论模型是否正确。
本次评估的工具是PAT(Process Analysis Toolkit)和合约过程的最终执行结果。
PAT运行环境如下:

  • Windows10虚拟机: 8G内存、1核CPU、PAT版本3.5.0
  • 宿主机: MacOS Catalina v.10.15.7、 32GB RAM、 2GHz quad-coreIntel Core i5 processor

Curve下的Compound Pool提供USDC和DAI代币的即时交易。
Curve交易池添加流动性的过程如下图所示:
在这里插入图片描述

  • ① 用户将USDC和DAI投入Curve Compound Pool中
  • ② ③ ④ ⑤ Curve Compound Pool再把这写USDC和DAI质押到Compound Protocol中,并获得cUSDC和cDAI。
  • ⑥ Curve Compound Pool保留cUSDC和cDAI,并给用户一定量的cCrv代币作为流动性凭证。

这个过程中包含的状态改变动作包括: 在Curve和Compound中添加、删除流动性;在Curve中进行交易;在Compound中借钱和赎回。
在Curve的流动性提供者抵押或赎回代币时FcurveF_{curve},Compound的放贷人和借钱人也在进行着借贷操作FcompoundF_{compound}
为了描述Curve中可能遇到的滑点、Front-Running等问题,我们在描述USDC和DAI的swap时要标明方向(是USDC->DAI还是DAI->USDC)。
最后,我们使用PAT工具将solidity或Vyper这种高级语言的合约翻译成C#或CSP#。在PAT中,高级语言的翻译,数据结构和操作实现的翻译都很方便。如果需要PAT的实现方式,可以查看项目代码https://github.com/polinatolmach/DeFi-csp-models/

基于上述验证模型,我们来研究一下Defi项目中那些独立交易所项目、金融借贷项目、代币合约以及这三者的任意组合。下表是形式化验证的结果,即所有组合型Defi项目需要满足的约束(requirement)。
在这里插入图片描述

  • 约束1: 所有Token拥有者的余额总和等于Token的总发行量。
  • 约束2:用户质押的Token应和获得的凭证数量成比例。且项目任何时候不应mint(0)。
  • 约束3:Compound.ExchangeRate 保持递增
  • 约束4:Compound用户赎回质押时产生的收益非负。
  • 约束5:用户无法赎回资产时,损失不应超过本金的20%。

译者注: 这篇论文研究的是Curve的Compound池 和 Compound本身。Compound存在一点点supplier Token无法赎回的风险(对原理感兴趣的读者可以学习一下Guantlet团队的金融风险分析文章)。再加上Exchange可能存在的滑点、套利等安全问题,最终使得约束5:资产无法赎回成为一个不可忽视的安全风险点。

最终,我们使用PAT工具的可达性分析,得到上述结论。
任何部署在以太坊上的Defi智能合约项目,均需要满足这5个约束。否则一定存在可以利用的安全漏洞。
我们的实验证明了,形式化验证语言CSP,可以很好的检验智能合约的安全性。它可以自动化地挖掘组合型Defi智能合约项目中存在的安全漏洞。

5 相关工作

Defi合约分析是一个比较新的领域,现有的Defi分析大多关于在野漏洞和实际攻击事件。
例如,Liu和Szalachowski探讨了4个主要DeFi平台Oracle使用不当导致的安全问题 Liu, B., Szalachowski, P.: A first look into DeFi oracles (2020)

也有很多文章讨论了闪电贷Flashloan的安全风险。
例如Wang, D., Wu, S., Lin, Z., Wu, L., Yuan, X., Zhou, Y., Wang, H., Ren, K.: Towardsunderstanding flash loan and its applications in DeFi ecosystem (2020)分析了如何发现基于闪电贷的套利机会。

还有几篇文章从Defi项目本身状态的变化来研究安全风险。
例如

最近还有两篇文章,使用形式化验证来探讨Defi Protocol的安全性。

其中Perez的研究中,提出了更为通解的形式化验证模型。Bartoletti则是研究了更多的Defi项目。
相比于上述研究,本文的做出的贡献主要是提出了更为通解的Pool模型。

6 后期工作

本文中,我们使用形式化验证的方法,总结出了Defi Protocol应满足的5个约束。在未来的工作中,我们将致力于丰富约束内容,并将模型的使用场景向加密金融和其他Defi项目进行适配。