Web3安全系列 | 智能合约安全审计利器链必验,如何检测出14W个地址合约存在的K值校验问题?

admin 2022年7月21日18:24:38评论200 views字数 3477阅读11分35秒阅读模式

Web3安全系列 | 智能合约安全审计利器链必验,如何检测出14W个地址合约存在的K值校验问题?


Web3安全系列 | 智能合约安全审计利器链必验,如何检测出14W个地址合约存在的K值校验问题?
写在前面:
Web3智能合约安全系列文章,我们将为大家分享用形式化验证工具“链必验”检测出的各类漏洞,并给出专业的修复建议,帮助开发者提高智能合约的安全。

Web3的世界,你以为是通往一个重新定义游戏规则的世界,却不知道这里面其实布满了风险。

越来越多的安全问题不断的影响着行业的发展,比如一些智能合约代码的错误,导致被盗的案例比比皆是。

一个简单的漏洞,在Web3行业往往会带来巨大的损失。今天我们就来为大家解读Web3智能合约不可忽视的一个问题:K值校验。


PART 01
智能合约安全审计利器链必验,巡视Web3安全

作为全球最早专门从事区块链安全的公司,成都链安创始人是全球最早将形式化验证技术应用于智能合约安全审计的专家之一,有着二十多年的形式化验证经验。成都链安团队采用形式化验证、模糊测试等多重技术作为核心技术,研发了面向智能合约的高度自动化的安全检测工具“链必验”,其工具的自动化检测精度高达97%,可以“一键式”自动检测智能合约的几百种安全问题。


Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?
链必验免费版界面截图


近日成都链安安全审计专家通过对大量不同业务场景智能合约安全问题进行深入分析总结,分类凝练出丰富的智能合约安全问题库,而我们也通过形式化验证工具“链必验”提取了ETH和BSC上共14W个地址的合约信息,发现这些地址合约全部都是相似的业务合约,其中一些可能存在K值校验问题。这个必须要引起重视。今天,我们就为大家来解读K值校验,并给出专业的修复建议。



PART 02
什么是K值校验问题?

由于Uniswap 这类DEX的实际的兑换转账操作在Pair的swap()函数中实现,为了防止攻击者越过Router合约直接调用Pair合约进行swap()转账,需要在Pair合约的swap()函数中进行K值校验,即swap之后pair中的K值仍然守恒。如果K值检验相关代码存在安全漏洞,那么攻击者能够以极少量的代币兑换出Pair中大部分代币。下面我们通过一个案例为大家讲解一下:


案例:swap函数未对K值进行校验安全问题


Uniswap的核心是恒定乘积模型K=x*y,其中的K值是该pair合约持有代币数量的乘积,且要求之后的每一笔交易完成后K值必须增加(考虑手续费)。因此如果不进行K值校验,将很容易成为攻击点。

 

Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?
 Uniswap的价格波动


以Impossible Finance事件为例,该项目是Uniswap的仿盘,实现了两种兑换代币的函数:cheapSwap和swap。其中cheapSwap函数少了K值校验(如下图所示),但是项目方知道缺少K值校验的后果,专门为cheapSwap函数增加了onlyIFRouter做修饰,来限制cheapSwap函数只能被指定的Router合约调用。


Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

合约未检查k值的cheapSwap函数


正常情况下,当用户使用Router合约兑换代币时,首先会使用getAmountsOut函数来计算正确的代币数量amounts;然后调用safeTransferFrom将用户的兑换消耗代币转入目标pair合约;最后,通过内部调用_swap函数来执行cheapSwap函数将兑换代币转至目标地址。


Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

 Router01合约的swapExactTokensForTokens函数


但是,由于cheapSwap函数缺少了K值检验,如果攻击者部署恶意代币合约,在Router合约调用safeTransferFrom函数时,回调正常的pair合约进行同种兑换,由于,回调后的兑换使用的amounts仍是未更新之前的数据,已不符合改变账本状态之后的校验,那么攻击会导致以错误的价格兑换出目标代币,以此获利。


PART 03
链必验检测出14W个地址合约存在K值校验问题


我们通过对K值校验问题的研究,总结了该问题的特点,提取出了该问题的通用属性供“链必验”自动化检测工具使用。在此之后,我们通过节点信息的分析,提取了ETH和BSC上共14W个地址的合约信息。这些地址合约全部都是相似的业务合约,均可能存在K值校验问题。“链必验”对这些地址进行了该漏洞的检测,最终发现两个合约具有此类漏洞。

 

Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?


Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

 *已对具体项目名字做了模糊处理

 

两个合约均为K值校验时左右比例不匹配,一边是10000,一边是1000。这样就会存在安全漏洞。


PART 04
形式化验证技术再出鞘,让黑客无处藏身


开篇我们提到的形式化验证工具“链必验”,为本次漏洞找寻提供了很大的帮助。


针对此类安全问题,成都链安安全团队的建议是:在关键的兑换函数中必须做正确的K值校验,不要为了节省gas和代码量就将K值校验和安全验证依赖外部验证,做到自身功能完善。


Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?


对于项目方而言,像K值校验问题这类漏洞还是建议找区块链安全公司处理。


因为和传统安全不同,智能合约不存在程序随机“跑崩”的概念,所以无论正向形式化证明还是测试攻击都离不开与业务场景相关的安全属性不变量,因此经多年大量合约安全审计实战积累出的智能合约安全问题库和可重用的智能合约安全属性不变量以及高路径覆盖率的自动化检测、测试、验证混合机器引擎是保证安全审计质量的关键。


成都链安形式化验证专家会将安全审计专家凝练出的安全问题利用严格的数理逻辑抽象成可重用的安全属性不变量,并交给混合机器引擎进行自动化检测、测试、验证,实践证明这些可重用的安全属性不变量可有效发现智能合约中新的微妙漏洞。


Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?


作为一家致力于区块链安全生态建设的全球领先区块链安全公司,成都链安目前已与国内外头部区块链企业建立了深度合作;为全球2000多份智能合约、100多个区块链平台和落地应用系统提供了安全审计与防御部署服务。自主研发的“链必安”一站式区块链安全服务平台可为执法监管机构、金融机构、区块链企业等提供安全审计、安全防护、安全监管、安全预警、安全咨询等全生命周期安全保障解决方案。欢迎点击公众号留言框,与我们联系。


扩展阅读:

科普 | 如何为你的智能合约“上保险”,形式化验证了解一下?

2 智能合约自动检测工具『链必验』,如何带你解锁Web3.0世界

3 玩转Web3智能合约开发,有它就够了

链必验

智能合约形式化验证工具




Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

链必验是一款全球领先的“一键式”智能合约形式化验证平台。检测准确率高达97%以上,精确定位风险代码位置并给出修改建议,自动检测智能合约80余项的常规安全漏洞及功能逻辑缺陷。现已拥有生态用户10万+,是全球首套同时支持蚂蚁链、腾讯区块链、FISCO-BCOS、Fabric等的智能合约形式化验证平台。可以极大提高智能合约的人工审计效率,有效降低安全隐患遗漏风险。 
检测内容

链必验针对每个用户模拟了一条单独的测试链,用户可以自主配置块高、时间戳等区块链参数,并在测试链上对智能合约进行部署、测试和验证,是集智能合约开发、测试、验证于一体的综合平台。

在验证的过程中,平台采用形式化验证等技术,对执行环境进行建模,通过数学推理等方法对安全属性进行验证,发现合约在运行时可能出现的安全问题,协助合约开发者发现合约中的潜在安全隐患,定位漏洞产生的位置,增强合约的安全性。主要包含三大方面的检测:

Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

(1)代码规范性检测。此项针对合约编写时的一些代码规范进行检测,包括全局变量使用错误、未接收返回值、格式化字符串错误、冗余的条件判断等问题。不规范的代码编写引发安全问题的可能性会大大提高。

(2)常规安全问题检测。此项针对合约中常见的安全问题进行检测,包括循环变量使用错误、随机遍历使用错误、整数溢出、系统接口使用错误等问题。常规安全问题是所有合约都可能出现的安全问题,与业务逻辑无关。

(3)业务逻辑安全检测。此项针对合约中的业务逻辑安全进行检测,包括数据库读写问题、业务逻辑实现正确性等问题。业务逻辑安全问题与合约功能密切相关,也是风险最高的安全问题。
检测优势

(1)支持多个区块链平台合约:同时支持Fabric、FISCO BCOS、蚂蚁链等,并可按需适配其他链平台;

(2)支持三大类超过100条安全检测项;

(3)可“一键式”精确自动定位代码漏洞和bug,检测准确度高达97%;

(4)支持主流的go、solidity等多种合约语言;

(5)支持SaaS接入方式以及vscode插件版的本地部署接入方式,同时提供第三方调用的rest/http安全检测接口。

Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

目前,产品已开放免费试用,如果您想更深入了解和体验产品,可以直接点开试用链接:https://vaas.lianantech.com/#/main

Web3安全系列 | 智能合约安全审计利器链必验,如何检测出14W个地址合约存在的K值校验问题?
点个关注了再走吧~


Web3安全系列 | 智能合约安全审计利器链必验,如何检测出14W个地址合约存在的K值校验问题?



Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

原文始发于微信公众号(成都链安):Web3安全系列 | 智能合约安全审计利器“链必验”,如何检测出14W个地址合约存在的K值校验问题?

  • 左青龙
  • 微信扫一扫
  • weinxin
  • 右白虎
  • 微信扫一扫
  • weinxin
admin
  • 本文由 发表于 2022年7月21日18:24:38
  • 转载请保留本文链接(CN-SEC中文网:感谢原作者辛苦付出):
                   Web3安全系列 | 智能合约安全审计利器链必验,如何检测出14W个地址合约存在的K值校验问题?https://cn-sec.com/archives/1191637.html

发表评论

匿名网友 填写信息