Runtime Verification and Vulnerability Testing of Smart Contracts

  • Misha AbrahamEmail author
  • K. P. Jevitha
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 1046)


Smart contracts are programs that help in automating agreement between multiple parties involving no external trusted authority. Since smart contracts deal with millions of dollars worth of virtual coins, it is important to ensure that they execute correctly and are free from vulnerabilities. This work focuses on smart contracts in Ethereum blockchain, the most utilized platform for smart contracts so far. Our emphasis is mainly on two core areas. One involves the runtime verification of ERC20 tokens using K framework and the other involves the comparison of tools available for detecting the vulnerabilities in smart contract. The six core functions of ERC20, namely allowance(), approve(), total-supply(), balanceof(), transferfrom() and transfer() were considered for runtime verification. ERC20 contracts were tested with ERC20 standard and the results showed that only 30% in allowance() function, 50% in transferfrom() function, and 90% in transfer() function, were compliant to the standard. The other focus area involves the comparison of existing tool that could identify vulnerabilities in smart contract. Five tools were taken for the comparison, namely Oyente, Securify, Remix, Smartcheck and Mythril and were tested against 15 different vulnerabilities. Out of the 5 tools taken, Smartcheck was found to detect the highest number of vulnerabilities.


Blockchain Smart contract Vulnerabilities Runtime verification ERC20 token K framework 


  1. 1.
    Zheng, Z., et al.: An overview of blockchain technology: architecture, consensus, and future trends. In: 2017 IEEE International Congress on Big Data (BigData Congress). IEEE (2017)Google Scholar
  2. 2.
    Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)Google Scholar
  3. 3.
    K Framework - An Overview. Accessed 22 Sept 2018
  4. 4.
    Rosu, G.: ERC20-K: Formal Executable Specification of ERC20. Accessed 21 Sept 2018
  5. 5.
    Formal verification of ERC-20 contracts. Accessed 21 Sept 2018
  6. 6.
    How Formal Verification of Smart Contracts Works. Accessed 21 Sept 2018
  7. 7.
    Sajana, P., Sindhu, M., Sethumadhavan, M.: On blockchain applications: hyperledger fabric and ethereum. Int. J. Pure Appl. Math. 118, 2965–2970 (2018)Google Scholar
  8. 8.
    Alharby, M., van Moorsel, A.: Blockchain-based smart contracts: a systematic mapping study. arXiv preprint arXiv:1710.06372 (2017)
  9. 9.
  10. 10.
  11. 11.
    Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017). Scholar
  12. 12.
    Egbertsen, W., et al.: Replacing paper contracts with Ethereum smart contracts (2016)Google Scholar
  13. 13.
    Kosba, A., et al.: Hawk: the blockchain model of cryptography and privacy-preserving smart contracts. In: 2016 IEEE Symposium on Security and Privacy (SP). IEEE (2016)Google Scholar
  14. 14.
    del Castillo, M.: The dao attacked: code issue leads to $60 million ether theft. Saatavissa (viitattu 13.2.2017). Accessed 15 Sept 2018
  15. 15.
    Reentrancy Woes in Smart Contracts. Accessed 22 Aug 2018
  16. 16.
    Luu, L., et al.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. ACM (2016)Google Scholar
  17. 17.
    Kalra, S., et al.: ZEUS: analyzing safety of smart contracts. In: NDSS (2018)Google Scholar
  18. 18.
    Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 79–94. Springer, Heidelberg (2016). Scholar
  19. 19.
    Hildenbrandt, E., et al.: KEVM: a complete semantics of the ethereum virtual machine (2017)Google Scholar
  20. 20.
    Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. ACM (2016)Google Scholar
  21. 21.
    Nikolic, I., et al.: Finding the greedy, prodigal, and suicidal contracts at scale. arXiv preprint arXiv:1802.06038 (2018)
  22. 22. Accessed 13 Sept 2018
  23. 23.
  24. 24.
  25. 25.

Copyright information

© Springer Nature Singapore Pte Ltd. 2019

Authors and Affiliations

  1. 1.Amrita School of EngineeringAmrita Vishwa VidyapeethamCoimbatoreIndia

Personalised recommendations