迈向真正的去中心化——Uniswap V2认证版

经数据统计，2021年初以来DeFi项目连续遭到黑客攻击，总损失已超过5亿美元。

DeFi项目频频遭受攻击，损失惨重，这足以向DeFi，乃至整个区块链生态敲响警钟。

而这也是类似于Uniswap V2这样的独立的、可证明正确的代码结构组成的认证合约存在的意义。

尽管目前这种严格的验证流程较为困难且费时，且此类重要引擎代码中哪怕发生极其微小的错误，也可能会产生巨大的负面连锁影响，但这对于DeFi的安全性来说仍旧是必不可少的。

在下文中，CertiK将以Uniswap V2为例，为大家分享其认证版本。

让我们来看看这一版本是如何做到维护了区块链的安全性与稳定性并实现真正的去中心化飞跃。

Uniswap V2的认证版本

Uniswap V2通过密码学，形式化驱动的程序结构以及博弈论的激励机制替代了其他的可信赖第三方。

它的函数和语句已通过严格数学的证明，其正确性可接受独立验证（即去中心化验证）。

在Uniswap V2中有两条准则：

第一，要确保在AMM中操纵代币价格的高成本，这可以使恶意操纵者难以迅速耗尽资金。

其次，由于AMM往往被用作链上价格预测，操纵现货市场标记价格（mark price）的消耗比从衍生品市场交易可获得的利润小。

一般认证合约的典型pen-and-paper statement存在多个问题：

此证明公式因使用了令人望而生畏的符号、数学函数和一些分析定理导致难以被理解，其包含的漏洞和错误往往也难以被发现。

即便该陈述公式被理解且纸质证明被信任，代码也准确无误，但也无法保证该协议实际运行后的代码实现真正遵循了代码的设计意图。

更重要的是，在这个公式中存在有实数，而合约执行中有界整数，因此在这一点上陈述和证明二者也许会出现不匹配的情况。

由上述pen-and-paper statement和纸质证明，可以得出——即使是经过必要的推理、传统的代码审计、甚至是初步的形式化验证，也无法说明并判定其准确性。

然而，在在经过验证的Uniswap V2协议中：

这个公式显而易见更容易理解，此外?

在实际过程中，完全可以使用“机器可理解并可验证”的精确术语来证明Uniswap V2的安全性。

这就可以证明Uniswap V2是完全安全的吗？

当然。

与纸质证明相比，上文对于Uniswap的安全证明在实现中更严格地考虑了整数近似（例如，舍入误差等）的问题。

此外，Uniswap V2可以消除当前DeFi安全领域中的人为干扰，以机械化、去中心化的可证明安全性取代了人工审计可能导致的风险，做到了真正的去中心化。

而相比于总出现故障的Solidity编译器，Uniswap V2的安全证明是根据经过认证的智能合约编译器生成的字节码进行检查的，这显然会更加具备可信力。

写在结尾

DeFi从广义上来说，仍然处于初步发展的路途中。

通过使用可验证的合约与安全证明，也将促使DeFi建立其生态的安全秩序。

目前，Uniswap V2合约及其安全证明已部署于CertiK Chain，可通过以下链接进行查看：

▣ https://explorer.certik.foundation/transactions/5BC3861DE7D786FF64153A4AD1EBB34E58B695450F82BC4AC819D9216B2B1A08?net=shentu-1

▣ https://github.com/CertiKProject/Certified-DeFi