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 \emph{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 \toolname on the entire data set from \etherscan. Our experiments demonstrate the benefits of summary-based symbolic evaluation and show that \toolname outperforms state-of-the-art smart contracts analyzers, \teether, \mythril, and \contractfuzz, in terms of running time, precision, and soundness.
Thu 24 Sep Times are displayed in time zone: (UTC) Coordinated Universal Time
16:00 - 16:20 Talk | Prober: Practically Defending Overflows with Page Protection Research Papers Hongyu LiuPurdue University, Ruiqin TianCollege of William and Mary, Bin RenCollege of William and Mary, Tongping LiuUniversity of Massachusetts Amherst | ||
16:20 - 16:40 Talk | MinerRay: Semantics-Aware Analysis for Ever-Evolving Cryptojacking Detection Research Papers Alan RomanoUniversity at Buffalo, SUNY, Yunhui ZhengIBM T.J. Watson Research Center, Weihang WangUniversity at Buffalo, SUNY | ||
16:40 - 17:00 Talk | Summary-Based Symbolic Evaluation for Smart Contracts![]() Research Papers Yu FengUniversity of California, Santa Barbara, Emina TorlakUniversity of Washington, Rastislav BodikUniversity of Washington |