Finding Unchecked Low-Level Calls with Zero False Positives and Negatives in Ethereum Smart Contracts.

Smart contracts are a relatively new class of computer programs that are intended to run on a blockchain. Checking a smart contract for security vulnerabilities is recognized as an important problem in both research and practice. Motivated by recent empirical work that suggests that existing tools suffer high numbers of false positives and negatives for vulnerabilities that belong to commonly-occurring classes, we ask: for even one such class of vulnerabilities, can there exist a tool that is highly effective? We answer in the affirmative by construction: for the class of unchecked low-level calls, checking for which is undecidable in general and PSPACE-complete under finitizing assumptions we adopt, we propose an approach for Ethereum smart contracts that comprises a reduction to model-checking, encoding the property in Linear Temporal Logic (LTL) and use of an off-the-shelf model checker. We find that across almost 200 smart contracts drawn from curated and "wild" datasets from the publicly available benchmark that underlies the prior empirical work that points out that existing tools suffer high numbers of false positives and negatives, our approach is highly effective in that we see zero false positives and negatives.