Static Detection of Missing Validations in Solidity Smart Contracts

The Solidity smart contract language is deterministic by design. Nevertheless, some instances of nondeterminism (ND) in smart contracts stem from unpredictable inputs received during execution, such as inputs from asynchronous callbacks of Oracles or externally called contracts that halt unexpectedly. Such values must be validated to meet prespecified criteria before they reach critical program parts; otherwise, they can lead to nondeterministic state outcomes in smart contracts, which we refer to as ND-issues. To detect ND-issues, we propose an information flow-based analysis that tracks the unpredictable inputs and return values that are not validated before reaching critical program parts. We have implemented our proposal in FONOVA and evaluated it using 326 frequently used Ethereum smart contracts. The evaluation shows that FONOVA detects five times more exploitable instances of ND-issues with 12 times shorter analysis time than leading tools like Ethainter, Securify, and Mythril.