\n \n \n
\n
\n\n \n \n \n \n \n \n solc-verify: A Modular Verifier for Solidity Smart Contracts.\n \n \n \n \n\n\n \n Hajdu, Á.; and Jovanović, D.\n\n\n \n\n\n\n In
Verified Software. Theories, Tools, and Experiments, volume 12301, of Lecture Notes in Computer Science, pages 161–179. Springer, 2020.\n
\n\n
\n\n
\n\n
\n\n \n \n pdf\n \n \n \n link\n \n \n \n slides\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@incollection{vstte2019,\n author = {Hajdu, {\\'A}kos and Jovanovi{\\'c}, Dejan},\n title = {solc-verify: A Modular Verifier for {S}olidity Smart Contracts},\n year = {2020},\n booktitle = {Verified Software. Theories, Tools, and Experiments},\n pages = {161--179},\n series = {Lecture Notes in Computer Science},\n volume = {12301},\n publisher = {Springer},\n doi = {10.1007/978-3-030-41600-3_11},\n isbn = {978-3-030-41600-3},\n\n type = {Conference},\n\n url_pdf = {https://hajduakos.github.io/publications/vstte2019.pdf},\n url_link = {https://link.springer.com/chapter/10.1007/978-3-030-41600-3_11},\n url_slides = {https://hajduakos.github.io/publications/slides/vstte2019.pdf},\n\n abstract = {We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort.},\n}\n\n
\n
\n\n\n
\n We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Efficient Strategies for CEGAR-based Model Checking.\n \n \n \n \n\n\n \n Hajdu, Á.; and Micskei, Z.\n\n\n \n\n\n\n
Journal of Automated Reasoning, 64(6): 1051–1091. 2020.\n
\n\n
\n\n
\n\n
\n\n \n \n pdf\n \n \n \n link\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 14 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{jar2019,\n author = {{\\'A}kos Hajdu and Zolt{\\'a}n Micskei},\n title = {Efficient Strategies for {CEGAR}-based Model Checking},\n journal = {Journal of Automated Reasoning},\n volume = {64},\n number = {6},\n pages = {1051--1091},\n year = {2020},\n doi = {10.1007/s10817-019-09535-x},\n\n type = {Journal},\n\n url_pdf = {https://link.springer.com/content/pdf/10.1007%2Fs10817-019-09535-x.pdf},\n url_link = {https://link.springer.com/article/10.1007/s10817-019-09535-x},\n\n abstract = {Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for efficient verification. This has lead to generic and configurable CEGAR frameworks, which can incorporate various algorithms. In our paper we propose six novel improvements to different aspects of the CEGAR approach, including both abstraction and refinement. We implement our new contributions in the Theta framework allowing us to compare them with state-of-the-art algorithms. We conduct an experiment on a diverse set of models to address research questions related to the effectiveness and efficiency of our new strategies. Results show that our new contributions perform well in general. Moreover, we highlight certain cases where performance could not be increased or where a remarkable improvement is achieved.},\n}\n\n
\n
\n\n\n
\n Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for efficient verification. This has lead to generic and configurable CEGAR frameworks, which can incorporate various algorithms. In our paper we propose six novel improvements to different aspects of the CEGAR approach, including both abstraction and refinement. We implement our new contributions in the Theta framework allowing us to compare them with state-of-the-art algorithms. We conduct an experiment on a diverse set of models to address research questions related to the effectiveness and efficiency of our new strategies. Results show that our new contributions perform well in general. Moreover, we highlight certain cases where performance could not be increased or where a remarkable improvement is achieved.\n
\n\n\n
\n\n\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n MIDDLEWARE TO AUTOMATICALLY VERIFY SMART CONTRACTS ON BLOCKCHAINS.\n \n \n \n \n\n\n \n Ciocarlie, G.; Eldefrawy, K.; Lepoint, T.; Navas, J.; Hajdu, Á.; and Jovanović, D.\n\n\n \n\n\n\n June 2020.\n
US Patent App. 16/227,728\n\n
\n\n
\n\n
\n\n \n \n link\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 11 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@misc{patent2020,\n title = {MIDDLEWARE TO AUTOMATICALLY VERIFY SMART CONTRACTS ON BLOCKCHAINS},\n author = {Ciocarlie, Gabriela and Eldefrawy, Karim and Lepoint, Tancrede and Navas, Jorge and Hajdu, {\\'A}kos and Jovanovi{\\'c}, Dejan},\n year = {2020},\n month = {June},\n note = {US Patent App. 16/227,728},\n\n type = {Patent application},\n\n url_link = {http://www.freepatentsonline.com/y2020/0201838.html},\n abstract = {A method, apparatus and system for automated verification of a smart contract on a blockchain include translating operating properties of a smart contract annotated with contract specifications at a source code level into verification conditions in an intermediate verification language, discharging the verification conditions using an SMT solver, and reporting results of the discharged verification conditions, such as successes and failures of the discharged verification conditions. The translating can include mapping statements of the smart contract to statements of the intermediate verification language and mapping expressions of the smart contract to expressions of the intermediate verification language. }\n}\n\n
\n
\n\n\n
\n A method, apparatus and system for automated verification of a smart contract on a blockchain include translating operating properties of a smart contract annotated with contract specifications at a source code level into verification conditions in an intermediate verification language, discharging the verification conditions using an SMT solver, and reporting results of the discharged verification conditions, such as successes and failures of the discharged verification conditions. The translating can include mapping statements of the smart contract to statements of the intermediate verification language and mapping expressions of the smart contract to expressions of the intermediate verification language. \n
\n\n\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Using Fault Injection to Assess Blockchain Systems in Presence of Faulty Smart Contracts.\n \n \n \n \n\n\n \n Hajdu, Á.; Ivaki, N.; Kocsis, I.; Klenik, A.; Gönczy, L.; Laranjeiro, N.; Madeira, H.; and Pataricza, A.\n\n\n \n\n\n\n
IEEE Access, 8: 190760–190783. 2020.\n
\n\n
\n\n
\n\n
\n\n \n \n pdf\n \n \n \n link\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{access2020,\n author = {{\\'A}kos Hajdu and Naghmeh Ivaki and Imre Kocsis and Attila Klenik and L{\\'a}szl{\\'o} G{\\"o}nczy and Nuno Laranjeiro and Henrique Madeira and Andr{\\'a}s Pataricza},\n title = {Using Fault Injection to Assess Blockchain Systems in Presence of Faulty Smart Contracts},\n journal = {IEEE Access},\n year = {2020},\n volume = {8},\n pages = {190760--190783},\n doi = {10.1109/ACCESS.2020.3032239},\n\n type = {Journal},\n\n url_pdf = {https://arxiv.org/abs/2006.11597.pdf},\n url_link = {https://ieeexplore.ieee.org/document/9229414},\n abstract = {Blockchain has become particularly popular due to its promise to support businesscritical services in very different domains (e.g., retail, healthcare). Blockchain systems rely on complex middleware, like Ethereum or Hyperledger Fabric, that allow running smart contracts, which specify business logic in cooperative applications. The presence of software defects in these contracts has notably caused failures, including severe security problems. In this paper, we use software-implemented fault injection (SWIFI) to assess the behavior of permissioned blockchain systems in the presence of faulty smart contracts. We emulate the occurrence of general software faults and also blockchain-specific software faults (e.g., missing require on transaction sender) in smart contracts code and observe the impact on the overall system dependability in terms of reliability and integrity. We also analyze the effectiveness of formal verification and runtime protection mechanisms in detecting the injected faults. Results indicate that formal verification and runtime protections have to complement built-in platform checks to guarantee proper dependability of blockchain systems. The work presented in this paper allows smart contract developers to become aware of possible faults in smart contracts and to understand the impact of their presence. It also provides valuable information for middleware developers to improve the overall fault tolerance of their systems.},\n}\n\n
\n
\n\n\n
\n Blockchain has become particularly popular due to its promise to support businesscritical services in very different domains (e.g., retail, healthcare). Blockchain systems rely on complex middleware, like Ethereum or Hyperledger Fabric, that allow running smart contracts, which specify business logic in cooperative applications. The presence of software defects in these contracts has notably caused failures, including severe security problems. In this paper, we use software-implemented fault injection (SWIFI) to assess the behavior of permissioned blockchain systems in the presence of faulty smart contracts. We emulate the occurrence of general software faults and also blockchain-specific software faults (e.g., missing require on transaction sender) in smart contracts code and observe the impact on the overall system dependability in terms of reliability and integrity. We also analyze the effectiveness of formal verification and runtime protection mechanisms in detecting the injected faults. Results indicate that formal verification and runtime protections have to complement built-in platform checks to guarantee proper dependability of blockchain systems. The work presented in this paper allows smart contract developers to become aware of possible faults in smart contracts and to understand the impact of their presence. It also provides valuable information for middleware developers to improve the overall fault tolerance of their systems.\n
\n\n\n
\n\n\n\n\n\n