作为全球最早专门从事区块链安全的公司，成都链安创始人是全球最早将形式化验证技术应用于智能合约安全审计的专家之一，有着二十多年的形式化验证经验。成都链安团队采用形式化验证、模糊测试等多重技术作为核心技术，研发了面向智能合约的高度自动化的安全检测工具“链必验”，其工具的自动化检测精度高达 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 世界

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

链必验

智能合约形式化验证工具

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

检测内容

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

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

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

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

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

检测优势

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

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

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

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

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

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