Intelligent contract formal verification and error correction method based on oracle machine

Abstract

The invention discloses an intelligent contract formal verification and error correction method based on an oracle machine. The method comprises the following steps: (1) a plurality of participants formulate an electronic intelligent contract; (2) formulating a consensus protocol, deploying an intelligent contract corresponding to the consensus protocol, and transmitting the signed intelligent contract into a block chain network; (3) performing formalized verification on the intelligent contract; (4) after formal verification, the smart contract proved to be executable continues to be triggered and executed; and (5) after formal verification, the intelligent contract of the discovered problem triggers the intelligent contract of the consensus protocol, and error correction is performed onthe problem through an oracle machine. According to the formal verification method, the verification efficiency of the intelligent contract can be improved, the transaction security of the blockchaincan be ensured, error correction of the intelligent contract with a problem is realized by utilizing the oracle machine, and only an error target intelligent contract can be ensured to be corrected byformulating a consensus protocol.

Description

technical field [0001] The invention belongs to the technical field of blockchain smart contract formal verification, and in particular relates to an oracle-based smart contract formal verification and error correction method. Background technique [0002] In 1995, cryptographer Nick Szabo defined a smart contract, arguing that a smart contract is a computable transaction agreement that executes contract terms, and is a computer-executed program. And the smart contract theory proposed by Nick Szabo appeared almost at the same time as the Internet, but there are mainly two reasons why the application seriously lags behind the theory: [0003] 1) How smart contracts control physical assets to ensure the effective execution of contracts, it is difficult for computer programs to control assets such as cash and shares in the real world; [0004] 2) It is difficult for a computer to ensure the execution of these terms to gain the trust of the contracting party. The contracting pa...

AI Technical Summary

Problems solved by technology

And the smart contract theory proposed by Nick Szabo appeared almost at the same time as the Internet, but there are mainly two reasons why the application seriously lags behind the theory:

[0003] 1) How smart contracts control physical assets to ensure the effective execution of contracts, it is difficult for computer programs to control assets such as cash and shares in the real world;

[0004] 2) It is difficult for a computer to ensure the execution of these terms to gain the trust of the contracting party. The contracting party needs a computer that can reliably interpret and execute the code. It cannot personally check the problematic computer, nor can it directly observe and verify the execution actions of other contracting parties. Only Let the third party review the records of contract execution by all parties

However, smart contracts based on the blockchain execution platform are usually in a decentralized and non-tamperable network environment. Smart contracts are distributed and stored in the blockchain network and automatically execute transactions and other activities according to trigger conditions. It cannot be modified. This is to ensure the absoluteness of the consensus agreement involving transactions and other events on the blockchain network. However, there are problems such as difficult control, difficult repair, and the inability to flexibly correct errors in smart contracts according to scenarios. It cannot satisfy the intelligence of errors. The limitation of contract error correction also limits the application of smart contracts

Moreover, smart contracts as execution programs are prone to loopholes. If you encounter a smart contract that is obviously beneficial to a certain contracting party, how to repair it, how to verify the logic of the smart contract and eliminate loopholes, has always been an issue. Key Issues Facing Smart Contracts

Images