一句话：提出基于摘要的符号求值，使智能合约对抗性漏洞利用合约的自动合成更高效且精确。
本文研究如何自动合成对抗性合约，以利用受害智能合约中的漏洞。由于直接符号求值需处理的指令过多，合成难以扩展。作者提出 Solar 系统，并引入一种查询语言与基于摘要的符号求值方法，在不牺牲漏洞查询精确性的前提下显著减少合成器需要符号执行的指令数量。作者将常见智能合约漏洞编码为查询，并在 Etherscan 的完整数据集上评估 Solar。实验表明，基于摘要的符号求值带来明显收益，且 Solar 在运行时间和精度上均优于当前先进的智能合约分析器 teether、Mythril 和 ContractFuzzer。
This paper presents Solar, a system for automatic synthesis of adversarial contracts that exploit vulnerabilities in a victim smart contract. To make the synthesis tractable, we introduce a query language as well as summary-based symbolic evaluation, which significantly reduces the number of instructions that our synthesizer needs to evaluate symbolically, without compromising the precision of the vulnerability query. We encoded common vulnerabilities of smart contracts and evaluated Solar on the entire data set from Etherscan. Our experiments demonstrate the benefits of summary-based symbolic evaluation and show that Solar outperforms state-of-the-art smart contracts analyzers, teether, Mythril, and ContractFuzzer, in terms of running time and precision.