苏州营销型网站制作,用html网站登录界面怎么做,化妆所有步骤,个人品牌网站设计智能合约安全新范式#xff0c;超越 require_assert
摘要
不要只为特定的函数写 require 语句#xff1b;为你的协议写 require 语句。函数遵循检查(requirements)-生效(Effects)-交互(INteractions)协议不变性(Invariants)或 FREI-PI 模式可以帮助你的合约更加安全#x…智能合约安全新范式超越 require_assert
摘要
不要只为特定的函数写 require 语句为你的协议写 require 语句。函数遵循检查(requirements)-生效(Effects)-交互(INteractions)协议不变性(Invariants)或 FREI-PI 模式可以帮助你的合约更加安全因为它迫使开发人员除了关注函数级别的安全之外还要关注协议级别的不变性。
动机
2023 年 3 月Euler Finance 被黑客攻击损失 2 亿美元。Euler Finance 是一个借贷市场用户可以存入抵押品并以其为抵押进行借款。它有一些独特的功能实际上他们是一个可与 Compound Finance 和 Aave 媲美的借贷市场。 你可以阅读关于这个黑客的事后总结这里。它的主要内容是在一个特定的函数中缺少健康检查允许用户打破借贷市场的基础不变性。
基础不变性Fundamental Invariants
大多数 DeFi 协议的核心都有一个不变性即程序状态的一个属性它被期望永远是真的。也可能有多个不变性但一般来说它们是围绕着一个核心思想建立的。这里是一些例子
如在借贷市场中用户不能采取任何行动使任何账户处于不安全或更不安全的抵押品仓位更不安全意味着它已经低于最低安全阈值因此不能进一步提取。AMM DEX 中x * y kx y k等等。流动性挖矿抵押中 用户应该只能提取他们存入的抵押代币数量。
Euler Finance 出错的地方不一定是他们增加了功能没有写测试或者没有遵循传统的最佳实践。他们对升级进行了审计并有测试但还是被漏掉了。核心问题是他们忘记了借贷市场的核心不变性审计人员也是如此。 注我不是要挑刺 Euler他们是一个有才华的团队但这是一个最近的案例。
问题的核心
你可能在想 “嗯没错。这就是他们被黑的原因他们忘了一个 require 语句”。是也不是。 但为什么他们会忘记 require 语句呢
检查-生效-交互 不够好
推荐给 solidity 开发者使用的一个常见模式是 Checks-Effects-Interactions检查-生效-交互模式。它对于消除与重入有关的错误非常有用而且通常会增加开发人员去执行输入验证的的数量。但是它容易出现只见树木不见森林的问题。 它教给开发人员的是“首先我写我的 require 语句然后我做生效然后也许我做任何交互然后我就安全了”。问题是通常情况下它变成了检查和效果的混合体–不错吧交互仍然是最后的所以重入性不是一个问题。但它迫使用户关注更具体的功能和个别的状态转换而不是全局的、更广泛的背景。这就是说 仅仅是检查-生效-交互模式就会使开发者忘记他们协议的核心不变性。 对于开发者来说它仍然是一个出色的模式但总是应该确保服务于协议的不变性说真的你还是应该使用 CEI。
正确做法FREI-PI 模式
以 dYdX 的 SoloMargin 合约源码中的这个片段为例它是借贷市场和杠杆交易合约。这是一个很好的例子我称之为 功能检查-生效-交互协议不变性Function Requirements-Effects-Interactions Protocol Invariants 模式或 FREI-PI 模式。 因此我相信这是早期借贷市场中唯一没有任何市场相关漏洞的借贷市场。Compound 和 Aave 没有直接出现问题但他们的分叉代码有关于过问题。而 bZx 则被黑了多次。 检查下面的代码注意以下的抽象概念
检查输入参数_verifyInputs。动作数据转换状态操作检查最终状态_verifyFinalState。
function operate(Storage.State storage state,Account.Info[] memory accounts,Actions.ActionArgs[] memory actions)public{Events.logOperation();_verifyInputs(accounts, actions);(bool[] memory primaryAccounts,Cache.MarketCache memory cache) _runPreprocessing(state,accounts,actions);_runActions(state,accounts,actions,cache);_verifyFinalState(state,accounts,primaryAccounts,cache);}仍然执行常用的 Checks-Effects-Interactions。值得注意的是带有额外 检查 的 检查-生效-交互 并不等同于 FREI-PI–它们是相似的但服务于根本不同的目标。因此开发者应该认为它们是不同的FREI-PI 作为一个更高的抽象旨在实现协议安全而 CEI 旨在实现功能安全。 这个合约的结构真的很有趣–用户可以在一连串的行动中执行他们想要的行动存款、借款、交易、转让、清算等。想存入 3 个不同的代币提取第 4 个并清算一个账户这是一个单一的调用。 这就是 FREI-PI 的力量用户可以在协议内做任何他们想做的事情只要核心借贷市场的不变性在调用结束时成立一个用户不能采取任何行动将任何账户置于不安全或更不安全的抵押品仓位。对于这个合约这是在verifyFinalState 中执行的检查每个受影响账户的抵押情况确保协议比交易开始时更好。 该函数中包括一些额外的不变性这些不变性是对核心不变性的补充有助于实现关闭市场等附属功能但真正_保持协议安全的是核心检查。
以实体为中心的 FREI-PI
FREI-PI 的另一个问题是以实体为中心的概念。以一个借贷市场和假定的核心不变性为例
一个用户不能采取任何行动将任何账户置于不安全或更不安全的抵押品仓位从技术上讲这不是唯一的不变性但它是针对用户实体的它仍然是核心协议不变性通常用户不变性是核心协议不变性。借贷市场通常也会有 2 个额外的实体
预言机管理/治理
每一个额外的不变性都会使协议更加难以保障因此越少越好。
预言机
对于预言机以 1.3 亿美元的Cream Finance 漏洞为例。预言机实体的核心不变性
预言机提供准确且(相对)实时的信息事实证明用 FREI-PI 在运行时验证预言机是很棘手的但是可以做到需要一些预先考虑。一般来说Chainlink 是一个很好的选择可以主要依靠满足大部分的不变性。在极少数的操纵或意外情况下有一些保障措施可能是有益的这些保障措施可以减少灵活性而有利于准确性比如检查最后知道的值是否比当前值大百分数百。同样dYdX 的 SoloMargin 系统在他们的 DAI 预言机方面做得很好 这里是代码如果你看不出来我认为这是历史上写得最好的复杂智能合约系统。 关于预言机评估的更多内容以及突出 Euler 团队的能力他们写了一篇关于计算操纵 Uniswap V3 TWAP 预言机价格的好文章。
管理/治理
为管理实体创建不变性是最棘手。这主要是由于他们的大部分作用是去改变现有的其他不变性。也就是说如果你能避免使用管理角色你应该这样做。 从根本上说一个管理实体的核心不变性可能是
管理员应该在当且仅当在其他的不变性或需要特意移除或修改不变性时才采取行动。解读管理员可以做一些应该结果不会破坏不变性的事情除非他们为了保护用户的资金而大幅改变事情例如将资产转移到救援合约中是对不变性的移除。管理员也应该被认为是一个用户所以核心借贷市场的用户不变性也应该对他们成立意味着他们不能对其他用户或协议进行攻击。目前一些管理员的行为不可能在运行时通过 FREI-PI 进行验证但如果在其他地方有足够强大的不变性希望大多数问题可以得到缓解。我说目前因为人们可以想象使用 zk 证明系统可能会检查合约的整个状态每个用户、每个预言机等。 作为一个管理员破坏不变性的例子以发生在 2022 年 8 月的borked the cETH market的 Compound 治理行动为例。从根本上说这次升级破坏了 Oracle 的不变性Oracle 提供准确和(相对)实时的信息。由于功能的缺失Oracle 可以提供不对的信息。一个运行时的 FREI-PI 验证检查受影响的 Oracle 能否提供实时信息可以防止升级的发生这样的情况。这可以纳入_setPriceOracle检查所有资产是否收到实时信息。FREI-PI 对管理角色的好处是管理角色对价格相对不敏感(或者至少应该是这样)所以更多的 Gas 使用量不应该是个大问题。
复杂是危险的
因此虽然最重要的不变性是协议的核心不变性但也可以有一些以实体为中心的不变性这些不变性必须为核心不变性所持有。但是最简单和最小的不变性集可能是最安全的。简单就是好的一个光辉榜样是 Uniswap …
为什么 Uniswap 从来没有被黑过大概
AMMs 可以有任何 DeFi 原语中最简单的基本不变性tokenBalanceX * tokenBalanceY k例如常量乘积模型。Uniswap V2 中的每个函数都是围绕这个简单的不变性
Mint添加到 k 中Burn从 k 中减去Swap转移 x 和 y不动 k。Skim重新调整 tokenBalanceX * tokenBalanceY使其等于 k移除多余的部分。
Uniswap V2 的安全秘诀核心是一个简单的不变性所有功能都是为它服务的。唯一可以争论的其他实体是治理它可以打开一个收费开关这并不触及核心不变性只是代币余额所有权的分配。他们的安全声明中的这种简单性是 Uniswap 从未被黑过的原因。简单其实并不是对 Uniswap 的智能合约的优秀开发者的轻视相反需要出色的工程师来找到简单性。
Gas 问题
我的 Twitter 上已经充满了优化论者关于这些检查是不必要的和低效的恐怖和痛苦的尖叫声。关于这个问题有两点
你知道还有什么是低效的吗不得不通过 etherscan 向Laurence朝鲜黑客发送信息使用 ETH 转账并威胁说 FBI 会介入。你可能已经从存储中加载了所有需要的数据所以在调用结束时只是对这些热数据加一点点 require 检查。你想让你的协议贵那么一点忽略不计的费用还是让它死于非命
如果成本过高请重新考虑核心变量并尝试简化。
这对我来说意味着什么
作为一个开发者要在开发过程中尽早地定义并表达出核心不变性。作为一个具体的建议让自己写的第一个函数是_verifyAfter在每次调用你的合约后验证你的不变性。把它放在你的合约中并在那里进行部署。用更广泛的不变性测试来补充这个不变性以及其他以实体为中心的不变性这些测试在部署前就被检查过了Foundry guide。 瞬时存储开启了一些有趣的优化和改进Nascent 将对此进行实验–我建议你考虑如何将瞬时存储作为一种工具以实现更好的跨调用上下文更安全。 在这篇文章中没有花太多时间在 FREI-PI 模式的介绍输入验证但这也是非常重要的。定义输入的边界是一项具有挑战性的任务以避免溢出和类似情况。可以考虑查看并关注我们的工具的进展pyrometer目前处于测试阶段请给我们一个星星。它可以深入了解并帮助找到你可能没有进行输入验证的地方。
结论
在任何朗朗上口的缩写FREI-PI或模式名称之上真正重要的一点是 在你的协议的核心不变性中找到简单性。并拼命工作以确保它永远不会被破坏或在它被破坏之前就被捕获。
