Security Analysis of Smart Contracts in Datalog

  • Petar TsankovEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11247)


Smart contracts enable mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts. To address this issue, we have developed Securify, a scalable and fully automated security analyzer for Ethereum smart contracts. A key technical insight behind the design of Securify is that whenever a smart contract violates a security property, it often also violates a simpler property that can be expressed on the contract’s data-flow graph. To leverage this insight, Securify symbolically encodes relevant control- and data-flow dependencies in stratified Datalog and uses scalable Datalog solvers to derive key semantic facts about the contract. Then, it inspects the inferred semantic facts to checks a set of compliance and violation patterns, which capture sufficient conditions for proving if a given security property holds or not.


Smart contracts Security analysis Datalog 


  1. 1.
    Etherdice (2016).
  2. 2.
  3. 3.
  4. 4.
    Accidental bug may have frozen \$280 million worth of digital coin ether in a cryptocurrency wallet (2017).
  5. 5.
    An in-depth look at the parity multisig bug (2017).
  6. 6.
  7. 7.
    Solidity, high-level language for writing smart contracts (2018).
  8. 8.
    Abiteboul, S., Hull, R., Vianu, V. (eds.): Foundations of Databases: The Logical Level, 1st edn. Addison-Wesley Longman Publishing Co. Inc., Boston (1995)Google Scholar
  9. 9.
    Buterin, V.: Ethereum: a next generation smart contract and decentralized application platform (2013).
  10. 10.
    Bylica, P.: How to find \$10 m just by reading the blockchain, April 2017.
  11. 11.
    Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)CrossRefGoogle Scholar
  12. 12.
    Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of ethereum smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243–269. Springer, Cham (2018). Scholar
  13. 13.
    Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254–269. ACM (2016)Google Scholar
  14. 14.
    Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., Bünzli, F., Vechev, M.: Securify: practical security analysis of smart contracts. In: CCS. ACM (2018)Google Scholar
  15. 15.
    Ullman, J.D.: Principles of Database and Knowledge-Base Systems, vol. 1 (1988)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Secure, Reliable, and Intelligent Systems LabETH ZurichZurichSwitzerland

Personalised recommendations