该论文研究区块链智能合约中的抢跑（frontrunning）攻击与抗抢跑性质的形式化定义问题。背景上，智能合约通过共识执行，但交易排序本质上是异步的：交易由矿工（或验证者）决定打包、排序与延迟。由于用户必须通过交易与合约交互，掌握排序权的节点可以重排、延迟或插入交易，从而抢在诚实用户之前获利，这类攻击在以太坊等主流链上已造成数百万美元损失。论文指出当前领域存在两个根本性缺陷。第一，缺少对“合约抗抢跑”这一性质本身的严格定义，导致安全目标模糊、无法对工具与审计结论做一致性比较。第二，现有动态检测方法在覆盖面上严重不足：作者对 287 份智能合约审计报告做了大规模研究，审计方共报告 393 个漏洞，其中 55% 落在当前最先进检测标准的判定范围之外，说明主流工具系统性地漏检了一大批被人类审计师认定的抢跑问题。针对这一缺口，作者提出首个面向智能合约抢跑漏洞的形式化定义。其核心洞察是：抗抢跑并非合约代码的固有属性，而强烈依赖于诚实用户如何与该合约交互——同一个合约在不同交互方式下可以是安全的或不安全的。基于该观察，作者设计了一个健全（sound）的算法，用于合成“安全交互条件”，即在什么交互约束下合约能够抵抗抢跑；并实现原型工具，将其应用于真实已审计合约，在两个以太坊合约中发现了此前未被发现的漏洞。工作属于形式化方法与实证研究结合，读者对象为智能合约安全研究者、审计工程师、形式化验证与区块链安全工具开发者。