PRO｜MEV 新形式：EV_Intent、Nethermind 推出形式化验证框架 Clear
通过声誉系统改进 Optimistic Rollups，以及五篇论文
欢迎阅读 ChainFeeds PRO #61 。本次内容将包含 MEV 新形式：EV_Intent、Nethermind 推出形式化验证框架 Clear，以及每周更新内容：比特币协议进展、以太坊治理相关、最新研究和进展，和最新论文。
重点
EVIntent - Darkmatter in MEV
求解器构建商 PropellerHeads 介绍了基于链上交易的 MEV 策略中的一种新形式：EV_Intent。EV_Intent 不同于传统的 MEV 策略，它需要机器人承担一定的风险来预测并利用交易意图。这是一种概率性的 MEV 策略，风险较高回报也可能更高。这种攻击利用了交易者的交易意图，而不是交易本身，目前的 MEV 解决方案反而容易成为 EV_Intent 的目标。
现有的 MEV 保护措施，如隐私 RPC 和 MEVBlocker 等，主要是通过信任链来传递交易，从而隐藏交易签名。但是，这些措施并未考虑交易意图的暴露问题。即使交易签名被隐藏，交易意图仍然可以通过拍卖、请求报价、代币批准等操作暴露。机器人可以通过监测这些操作来推断用户的交易意图，例如，代币批准操作通常表明用户即将进行相关代币的交易。通过推断交易意图，机器人可以在交易者之前进行卖出操作，再在交易者卖出后买回代币，从中获利。这种攻击被称为 EV_Intent。
Clear–Prove Anything About Your Solidity Smart Contracts
区块链研究和软件工程公司 Nethermind 介绍了一个名为 Clear 的形式化验证框架，专门用于验证 Solidity 或任何编译到 Yul 的编程语言编写的程序，帮助开发者确保其智能合约代码的正确性和安全性。
在使用 Clear 框架时，开发者首先需要定义其智能合约或程序的预期行为。这通常涉及到编写形式化的技术规范（specifications），它们详细描述了程序在各种输入和环境条件下应该如何表现。这些规格说明是用一种数学语言来描述的，可以非常精确地指定函数的每个操作、期望的输出以及错误处理机制。一旦程序的预期行为被定义，Clear 框架会将程序代码转换为一个抽象的表示形式，这种表示更适合于进行数学分析和证明。转换为抽象表示后，接下来的步骤是验证这个转换的一致性，Clear 通过自动化的证明检查器来确保抽象表示与原始代码的行为完全一致，没有引入任何错误或偏差。
通过以上步骤，Clear 帮助开发者验证智能合约或程序的代码确实符合其预期的行为规格。
比特币协议进展
2100 万比特币全部都已问世（原文发表于2019年）
Unchained 产品营销经理 Phil Geiger 通过对比黄金和比特币的供给方式，强调了比特币的稀缺性和不可增加性。与传统货币和其他资产如黄金不同，比特币的供给量是严格限制的，并且这一限制是通过全球比特币网络的共识以及代码规定实现的。作者讨论了比特币网络中的矿工如何通过解决数学问题来「挖矿」，以及这些活动如何受到代码和网络共识的规范。解释了如何通过电力和算力转换成比特币的挖矿过程，并强调这一过程的激励机制确保了网络的安全性和持续运作。
便利性与安全性的取舍光谱
Giacomo Zucco 在推特上对批评 ecash 的意见作出回复。他将不同的方案视为在用户的便利性和自主保管安全性之间取舍，并且这种取舍不是非此即彼的，允许作出不同程度的微调。Giacomo Zucco 用一系列的技术方案来阐释这种权衡是一个连续的光谱，而不是一个简单的黑白二分。他列举了从托管式交易所到通过更复杂的技术如 Statechain、Ark、Poon-Drijia 通道等方式来增强安全性，同时每一步向上的提升在安全性上都需要付出更多的成本和面对更大的挑战。
以太坊
研究和进展
Reputation-Centric Light Client Framework for Optimistic Rollups
Herodotus 开发者 Marcello Bardus 介绍了一个旨在通过声誉系统改进 Optimistic Rollups（ORUs）终结时间和数据验证效率的新框架。该框架利用 Herodotus 数据处理器，根据定序器的历史行为（如提交有效输出根和没有被质疑的记录）计算其声誉评分。这样，轻客户端可以信任声誉良好的定序器的输出根，无需等待完整的争议期，从而显著减少终结时间。如果某定序器提交的输出根被他人成功质疑并证实为无效，该定序器的声誉将立即重置为零，以确保系统的诚信和可靠性。此外，在发生未解决的冲突或检测到不规则情况时，系统会回退到标准的七天争议期，以确保系统的安全性。
Maximum Viable Security: A New Framing for Ethereum Issuance
研究员 Artem 介绍了最大可行安全（Maximum Viable Security，MVS）框架来评估以太坊的货币政策，并与最小可行发行（Minimum Viable Issuance，MVI）框架进行了对比。MVS 通过适当的发行量，确保足够的质押激励，最大化网络的去中心化程度，同时尽量保持 ETH 的稀缺性。MVI 框架旨在通过减少质押支出优化短期效益，但这种方法会导致质押的 ETH 集中在中心化交易所，削弱以太坊的安全性和中立性。MVS 框架优先考虑安全性和中立性，比最 MVI 框架更适合以太坊的长期发展。
Deep Diving Attestations - A quantitative analysis
以太坊基金会研究员 Toni Wahrstätter 分析了以太坊网络中的共识中验证（attestations）过程。平均每个 slot 有 500 个错误或遗漏的头部投票（占比 1.56%），150 个错误或遗漏的目标投票（占比 0.48%），以及 100 个遗漏的源投票。验证的作用是通过验证过去的检查点，确保区块链状态不可逆转，验证者通过验证来决定链的最新区块。每次验证包含三个部分：源投票（source vote）、目标投票（target vote）和头部投票（head vote）。
95.85% 的验证在下一个 slot 包含，小部分验证会在延迟多个 slot 后包含，这与验证器的性能有关。并且包含多个 blobs 的大区块更可能导致验证失败，因为验证器需要更多时间来下载和验证这些区块。此外，提议者延迟发布区块虽然可以增加 MEV 收益，但也会增加验证失败的风险，尤其是当区块发布时间超过 1.7 秒时。
MEV resistant dynamic pricing auction of execution proposal rights
以太坊基金会研究员 Anders Elowsson 提出了一种动态定价机制来销售执行提议权，通过市场动态来调整执行提议权的价格，以此来抵抗 MEV。价格的动态调整基于订单的数量、当前票池的饱和度（即当前未处理的订单数与理想状态下的差值），以及订单的变动速率。这些因素共同决定了每个 slot 的订单价格。这样订单输入和定价之间便建立一种平衡，使得潜在的 MEV 操纵者难以通过预测或操控市场来获得不当利益。为了进一步抵抗 MEV，该机制设计了一种方法，使得所有在同一时隙内的订单都有相同的预期销售价格，而无论具体的订单是在时隙的哪个时间点被添加的，有助于防止某些参与者利用时间优势操纵市场。
对于采用执行票据拍卖（ETA）的设计，来自同一时隙的订单可以直接通过 RANDAO 序列化，而不需要经过票池。这意味着买家会得到一个预估的订单到达时间，但具体时间无法提前确知，增加了市场的不确定性和公平性。对于采用执行票（ET）的设计，同一时间段接收的订单会被集体铸造成票据。这种方法允许多个订单共同形成一个执行票，这些票后续将被用于选择执行提案者。
L2 Asset Interoperability via Two-way Canonical Bridges
1kx 研究员 Wei Dai 提出了双向规范桥接的概念，允许 L2 铸造的资产可以规范地桥接回 L1。解决在 L2 上原生铸造的资产只能在其发行的 L2 上使用，而不能不借助外部桥梁直接桥接回第一层（L1）或其他 L2 的限制。操作流程：
L2 的结算合约将记录所有在其上发行的原生资产（已经通过双向规范桥接的资产）。
L2 的用户可以将本地资产发送到预设的系统地址，随后 L1 上的 L2 结算合约会发行 ERC-1155 代币（允许在单一合约中定义和管理多种类型的代币）。
使用 L2 到 L1 的调用机制，可以将新发行的资产移动到任何想要的目的地。
如果要将资产从 L1 反向桥接回其原始的 L2，可以调用 L2 结算合约上的特殊函数 burnAndDeposit。
MEV 相关
The MEV Letter #46
Flashbots 团队推出垂直于 MEV 研究领域的 Newsletter，以下是一些重点摘录：
Flahbots 宣布 rbuilder 为开源的，rbuilder 是使用Rust编写的速度极快的区块构建器。
文章《Preconfirmations under the NO lens》分析了在以太坊的 PBS 框架中实现预确认的复杂性及其对构建者和搜索者的影响。
文章《Leaderless and Leader-Based Preconfirmations》探讨了基于领导者的和无领导者的预确认，它们的优缺点以及潜在的组合。
文章《Intel TDX Security and Side Channels》详细介绍了 TDX 的一些安全问题及其影响。
视频《ePBS Breakout room #4》讨论了 EIP-7732、作为执行有效载荷一部分的提款处理、PTC 双区块攻击等问题。
视频《The Rollup: The C.A.K.E Framework, Credible Accounts, and Resource Locks》邀请 Stephane Gosselin 讨论链抽象、可信拍卖、共享排序器、MEV 和 OneBalance。
📑论文
Gradual Verification for Smart Contracts
作者来自：Shanghai Jiao Tong University、Carnegie Mellon University
作者的研究重点是解决区块链智能合约在与外部合约交互时容易出现漏洞，尤其是重入攻击问题。传统的验证技术在面对这些挑战时，无法提供全面的安全保证，因为外部合约的实现通常是不可用的。为此，本文提出了一种增量验证方法：逐步验证。通过结合静态和动态验证技术，增强智能合约的安全性，保证其正确性和灵活性，并优化资源使用。作者还通过使用 pyTEAL 语言为 Algorand 智能合约实现了一个原型系统，证明了这种方法的有效性。
Maximizing Blockchain Performance: Mitigating Conflicting Transactions through Parallelism and Dependency Management
作者来自：Syracuse University、Towson University
多个待处理交易在区块链中发生冲突时，会导致网络延迟加剧、系统资源浪费，最终导致吞吐量降低和交易失败率增加。为了解决这个问题，作者提出了一种新的区块链方案，该方案集成了交易并行处理和智能依赖管理器，旨在减少区块链网络中的冲突交易。实验结果表明，该方案在有效性和效率方面不仅减轻了冲突交易带来的挑战，而且在交易成功率、吞吐量和延迟方面优于现有的并行和非并行的Hyperledger Fabric区块链网络。
SoK: What don't we know? Understanding Security Vulnerabilities in SNARKs
作者来自：Imperial College London、Ethereum Foundation
作者对实际 SNARK（简洁非交互式知识论证）实现的端到端安全特性进行评估。首先建立了系统模型，确定了威胁模型并定义了使用 SNARK 系统的对抗角色。然后对 141 个实际 SNARK 实现漏洞的广泛分析，并提供了详细的分类法，以帮助开发人员和安全研究人员理解使用 SNARK 系统的安全威胁。作者还评估了现有的防御机制，并提出了增强 SNARK 系统安全性的建议。
FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols
作者来自：UC Santa Barbara、University of Illinois
现有智能合约漏洞检测工具难以有效处理多个智能合约之间复杂的金融交互，作者提出了一种名为 Foray 的综合框架，通过设计领域特定语言（DSL）和代币流图（TFG），将低层智能合约提升到高层次的金融操作，有效地解决了D eFi 协议中的深层逻辑漏洞检测问题，提高了效率和准确性。
The Dark Side of NFTs: A Large-Scale Empirical Study of Wash Trading
作者来自：Sun Yat-sen University、Monash University
作者对 NFT 洗售交易进行全面分析。洗售交易通常指涉及同一人或两个串通个体之间的交易，进行虚假交易，以制造出交易活跃的假象。此前的研究仅从财务角度检测 NFT 洗售交易，而现实中的洗售交易更加复杂（例如，并不以抬高市场价值为目的）。因此，作者对 NFT 洗售交易进行了最全面的研究，分析了 8,717,031 次转移事件和 3,830,141 次销售事件，涉及 2,701,883 个 NFT。从市场设计、盈利能力、NFT项目设计、支付代币、用户行为和 NFT 生态系统六个方面提出了见解。（本文最早发表于 2023 年 12 月 19 日，在 2024 年 7 月 10 日更新了 V2 版）