Analyzing information flow in solidity smart contracts

Protecting confidentiality and integrity of sensitive information in blockchain software systems is an important security aspect, which may be compromised due to unrestricted information flow along the control structures of smart contracts during their execution. Language-based information flow security analysis is a promising technique, which aims to detect possible unauthorized leakage of sensitive information or corruption of data values in critical computations of software systems. In this chapter, we extend traditional language-based information flow analysis to the case of Ethereum Solidity smart contracts in order to identify possible undesirable information flow in the contract codes that may be the source of the aforementioned software vulnerabilities. In particular, we apply data-flow analysis which accumulates (direct/indirect) dependency information among the smart contract variables, indicating possible information flow along all possible paths in the smart contract. To this end, we define concrete semantics of Solidity language and we design its abstraction in the domain of positive propositional formula Pos, which encodes variables’ dependencies in the form of logical formula. Insecure information flow is then detected based on their satisfiability using truth value assignments according to the variables’ security levels. We discuss precision improvement by combining Pos with other numerical abstract domains and various challenges in this research direction.