Static analysis of low-level code

Abstract

The Android platform is undoubtedly the most popular platform for smartphones, with thousands of new applications becoming available daily and billions of app installations each year. Ethereum is the most popular smart contract platform, with thousands of applications on the blockchain serving as trading platforms and providing other functionalities. Due to these platforms’ popularity, security issues in their applications may reach a catastrophic scale with ease. Several prominent automated techniques help to reveal security problems in applications at the early stages of expansion. One such technique is static analysis. This thesis focuses on the design of static analysis techniques for Android apps and smart contracts distributed in the form of low-level code (bytecode). After installation, an Android app may get access to a set of sensitive information sources (e.g., location data). Unfortunately, exposure of such information to third parties has led in the past to several cases of privacy breach, and continues to be a serious threat. In this thesis, we tackle information flow propagation in the bytecode of Android applications by sound Horn-clause based abstraction techniques. This work will be the first to use Horn-clause based techniques in the context of security analysis. Moreover, we prove that our approach is sound, that is, our approach provides guarantees for its results. As a consequence, it can be used to show the absence of explicit data leaks in an app. Furthermore, Horn-clause based abstraction techniques are not limited to information propagation tasks, that is, our techniques can be used to show any kind of program property expressed as a reachability property. In addition, our Horn-clause based techniques scale to large codebases, benefit from the advancements in Satisfiability Modulo Theory solving, and allow for favorable performance with respect to the state-of-the-art. We instantiate the principles that were obtained while developing the analysis techniques for Android applications in the context of Ethereum smart contracts distributed in the form of Ethereum Virtual Machine (EVM) bytecode. Smart contracts are programs mainly used to perform financial operations (e.g., auctions) on cryptocurrency blockchains (e.g., Ethereum). Recent attacks demonstrate that certain vulnerabilities in smart contracts might cause severe money loss and an overall decrease of trust in the technology. Therefore, security analysis of EVM bytecode is in the focus of the research community. This thesis presents two results which establish the foundations for sound security analysis of EVM bytecode. First, the semantics of EVM bytecode is mechanized for the first time and tested against the official Ethereum test suite. This result facilitates both the design of analysis techniques and establishing their correctness properties. Second, this thesis provides the first sound Control Flow Graph reconstruction solution for EVM bytecode, that is, our analysis guarantees that reachable parts of the code are never pruned. This guarantee is required by a number of security properties for smart contracts. We also develop a tool implementing our analysis and successfully evaluate it on a big collection of real-world contracts.