作为全球最早专门从事区块链安全的公司,成都链安创始人是全球最早将形式化验证技术应用于智能合约安全审计的专家之一,有着二十多年的形式化验证经验。成都链安团队采用形式化验证、模糊测试等多重技术作为核心技术,研发了面向智能合约的高度自动化的安全检测工具“链必验”,其工具的自动化检测精度高达97%,可以“一键式”自动检测智能合约的几百种安全问题。
由于Uniswap 这类DEX的实际的兑换转账操作在Pair的swap()函数中实现,为了防止攻击者越过Router合约直接调用Pair合约进行swap()转账,需要在Pair合约的swap()函数中进行K值校验,即swap之后pair中的K值仍然守恒。如果K值检验相关代码存在安全漏洞,那么攻击者能够以极少量的代币兑换出Pair中大部分代币。下面我们通过一个案例为大家讲解一下:
Uniswap的核心是恒定乘积模型K=x*y,其中的K值是该pair合约持有代币数量的乘积,且要求之后的每一笔交易完成后K值必须增加(考虑手续费)。因此如果不进行K值校验,将很容易成为攻击点。
以Impossible Finance事件为例,该项目是Uniswap的仿盘,实现了两种兑换代币的函数:cheapSwap和swap。其中cheapSwap函数少了K值校验(如下图所示),但是项目方知道缺少K值校验的后果,专门为cheapSwap函数增加了onlyIFRouter做修饰,来限制cheapSwap函数只能被指定的Router合约调用。
合约未检查k值的cheapSwap函数
正常情况下,当用户使用Router合约兑换代币时,首先会使用getAmountsOut函数来计算正确的代币数量amounts;然后调用safeTransferFrom将用户的兑换消耗代币转入目标pair合约;最后,通过内部调用_swap函数来执行cheapSwap函数将兑换代币转至目标地址。
Router01合约的swapExactTokensForTokens函数
但是,由于cheapSwap函数缺少了K值检验,如果攻击者部署恶意代币合约,在Router合约调用safeTransferFrom函数时,回调正常的pair合约进行同种兑换,由于,回调后的兑换使用的amounts仍是未更新之前的数据,已不符合改变账本状态之后的校验,那么攻击会导致以错误的价格兑换出目标代币,以此获利。
我们通过对K值校验问题的研究,总结了该问题的特点,提取出了该问题的通用属性供“链必验”自动化检测工具使用。在此之后,我们通过节点信息的分析,提取了ETH和BSC上共14W个地址的合约信息。这些地址合约全部都是相似的业务合约,均可能存在K值校验问题。“链必验”对这些地址进行了该漏洞的检测,最终发现两个合约具有此类漏洞。
*已对具体项目名字做了模糊处理
两个合约均为K值校验时左右比例不匹配,一边是10000,一边是1000。这样就会存在安全漏洞。
开篇我们提到的形式化验证工具“链必验”,为本次漏洞找寻提供了很大的帮助。
针对此类安全问题,成都链安安全团队的建议是:在关键的兑换函数中必须做正确的K值校验,不要为了节省gas和代码量就将K值校验和安全验证依赖外部验证,做到自身功能完善。
对于项目方而言,像K值校验问题这类漏洞还是建议找区块链安全公司处理。
因为和传统安全不同,智能合约不存在程序随机“跑崩”的概念,所以无论正向形式化证明还是测试攻击都离不开与业务场景相关的安全属性不变量,因此经多年大量合约安全审计实战积累出的智能合约安全问题库和可重用的智能合约安全属性不变量以及高路径覆盖率的自动化检测、测试、验证混合机器引擎是保证安全审计质量的关键。
成都链安形式化验证专家会将安全审计专家凝练出的安全问题利用严格的数理逻辑抽象成可重用的安全属性不变量,并交给混合机器引擎进行自动化检测、测试、验证,实践证明这些可重用的安全属性不变量可有效发现智能合约中新的微妙漏洞。
作为一家致力于区块链安全生态建设的全球领先区块链安全公司,成都链安目前已与国内外头部区块链企业建立了深度合作;为全球2000多份智能合约、100多个区块链平台和落地应用系统提供了安全审计与防御部署服务。自主研发的“链必安”一站式区块链安全服务平台可为执法监管机构、金融机构、区块链企业等提供安全审计、安全防护、安全监管、安全预警、安全咨询等全生命周期安全保障解决方案。欢迎点击公众号留言框,与我们联系。
扩展阅读:
1 科普 | 如何为你的智能合约“上保险”,形式化验证了解一下?
2 智能合约自动检测工具『链必验』,如何带你解锁Web3.0世界
链必验
智能合约形式化验证工具
链必验针对每个用户模拟了一条单独的测试链,用户可以自主配置块高、时间戳等区块链参数,并在测试链上对智能合约进行部署、测试和验证,是集智能合约开发、测试、验证于一体的综合平台。
在验证的过程中,平台采用形式化验证等技术,对执行环境进行建模,通过数学推理等方法对安全属性进行验证,发现合约在运行时可能出现的安全问题,协助合约开发者发现合约中的潜在安全隐患,定位漏洞产生的位置,增强合约的安全性。主要包含三大方面的检测:
(1)代码规范性检测。此项针对合约编写时的一些代码规范进行检测,包括全局变量使用错误、未接收返回值、格式化字符串错误、冗余的条件判断等问题。不规范的代码编写引发安全问题的可能性会大大提高。
(2)常规安全问题检测。此项针对合约中常见的安全问题进行检测,包括循环变量使用错误、随机遍历使用错误、整数溢出、系统接口使用错误等问题。常规安全问题是所有合约都可能出现的安全问题,与业务逻辑无关。
(1)支持多个区块链平台合约:同时支持Fabric、FISCO BCOS、蚂蚁链等,并可按需适配其他链平台;
(2)支持三大类超过100条安全检测项;
(3)可“一键式”精确自动定位代码漏洞和bug,检测准确度高达97%;
(4)支持主流的go、solidity等多种合约语言;
(5)支持SaaS接入方式以及vscode插件版的本地部署接入方式,同时提供第三方调用的rest/http安全检测接口。
目前,产品已开放免费试用,如果您想更深入了解和体验产品,可以直接点开试用链接:https://vaas.lianantech.com/#/main
原文始发于微信公众号(成都链安):Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?
- 左青龙
- 微信扫一扫
- 右白虎
- 微信扫一扫
评论