Submitted: December 2021

Abstract

Smart contracts are security-critical programs that run on the Ethereum blockchain. In the last years, a multitude of static analysis tools has been developed to assess the security of smart contracts, some of them (like the Securify tool) aiming to give security guarantees. This thesis investigates the security guarantees of the smart contract dependency analysis tool Securify.1 To this end, we recover the logical specification from the source code2 and present counterexamples for the soundness claims. We found that the Securify specification misses rules to propagate dependencies and propose a fixed version of the logical specification. The consequent analysis is built on top of a program slicing proof framework.3 To show its correctness, we instantiate the framework with a smart contract intermediate representation equivalent to the EVM semantics.4 For the instantiation of the proof framework, we develop a novel abstraction leveraging preprocessing information on memory locations. We use the instantiated correctness statement of the proof framework to show that the analysis’ output implies for this purpose developed independence definitions. These notions are strong enough to show that the analysis can soundly label smart contracts to be free of timestamp dependencies.4 Finally, we present HoRStify, a static dependency analysis tool based on the HoRSt framework,5 which works on an intermediate representation for smart contracts with annotated preprocessing information. HoRStify’s implementation follows the instantiation of the slicing framework and is evaluated on a small benchmark to demonstrate that it detects dependencies that Securify failed to discover.

  1. P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Buenzli, and M. Vechev, “Securify: Practical security analysis of smart contracts,” in Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018, pp. 67–82. ↩

  2. “[DEPRECATED] Securify scanner for ethereum smart contracts,” https://github.com/eth-sri/securify, accessed: 2021-07-29. ↩

  3. D. Wasserrab, D. Lohner, and G. Snelting, “On pdg-based noninterference and its modular proof,” in Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, 2009, pp. 31–44. ↩

  4. I. Grishchenko, M. Maffei, and C. Schneidewind, “A semantic framework for the security analysis of ethereum smart contracts,” in International Conference on Principles of Security and Trust. Springer, 2018, pp. 243–269. ↩ ↩2

  5. C. Schneidewind, I. Grishchenko, M. Scherer, and M. Maffei, “ethor: Practical and provably sound static analysis of ethereum smart contracts,” in Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020, pp. 621–640. ↩