Automated Runtime Verification of Security for E-Commerce Smart Contracts

Abstract

As a novel decentralized computing paradigm, blockchain is expected to disrupt the existing e-commerce architecture and process. Secure smart contracts are the crucial foundation for e-commerce based on blockchain. However, vulnerabilities in smart contracts occur from time to time and cause significant financial losses in e-commerce. Some static verification methods have been developed to guarantee security for e-commerce smart contracts at design time, but they cannot support complex scenarios at runtime. As a lightweight verification method, runtime verification is a potential method for secure e-commerce smart contracts. The existing runtime verification methods are based on the manual instrument, which leads to additional overheads and gas consumption. To deal with this, we propose a passive learning-based runtime verification framework for e-commerce smart contracts. Firstly, by exploring the Genetic algorithm to evolve state merging and automaton reorganizing in order to simultaneously split time and gas behaviors, we propose a passive learning method to model runtime information for e-commerce smart contracts (PL4ESC). It directly learns P²TA (priced probabilistic timed automaton) from runtime traces without any prior knowledge. Then, we integrate PL4ESC with the open-source PAT (Process Analysis Toolkit) to automatically verify the security of runtime e-commerce smart contracts. The experiments show that PL4ESC is better at accuracy and precision than state-of-the-art passive learning methods. It improves accuracy by 1 to 4 percent compared to TAG and RTI+. As far as we know, it is not only the first learning method that can learn a P²TA from traces, but it is also the first automated runtime verification framework for e-commerce smart contracts. This will provide security guarantees for blockchain-based e-commerce.