WO2021032192A1 - 存证智能合约的形式验证方法、系统、计算机设备和可读存储介质 - Google Patents

存证智能合约的形式验证方法、系统、计算机设备和可读存储介质 Download PDF

Info

Publication number
WO2021032192A1
WO2021032192A1 PCT/CN2020/110512 CN2020110512W WO2021032192A1 WO 2021032192 A1 WO2021032192 A1 WO 2021032192A1 CN 2020110512 W CN2020110512 W CN 2020110512W WO 2021032192 A1 WO2021032192 A1 WO 2021032192A1
Authority
WO
WIPO (PCT)
Prior art keywords
smart contract
formal verification
verification
contract
evidence
Prior art date
Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
Ceased
Application number
PCT/CN2020/110512
Other languages
English (en)
French (fr)
Inventor
邱炜伟
李伟
蔡亮
张帅
匡立中
Current Assignee (The listed assignees may be inaccurate. Google has not performed a legal analysis and makes no representation or warranty as to the accuracy of the list.)
Hangzhou Qulian Technology Co Ltd
Original Assignee
Hangzhou Qulian Technology Co Ltd
Priority date (The priority date is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the date listed.)
Filing date
Publication date
Application filed by Hangzhou Qulian Technology Co Ltd filed Critical Hangzhou Qulian Technology Co Ltd
Priority to JP2022510096A priority Critical patent/JP7309306B2/ja
Priority to US17/636,139 priority patent/US12028331B2/en
Priority to EP20853855.3A priority patent/EP4020294A4/en
Publication of WO2021032192A1 publication Critical patent/WO2021032192A1/zh
Anticipated expiration legal-status Critical
Ceased legal-status Critical Current

Links

Images

Classifications

    • H—ELECTRICITY
    • H04—ELECTRIC COMMUNICATION TECHNIQUE
    • H04L—TRANSMISSION OF DIGITAL INFORMATION, e.g. TELEGRAPHIC COMMUNICATION
    • H04L63/00—Network architectures or network communication protocols for network security
    • H04L63/08—Network architectures or network communication protocols for network security for authentication of entities
    • H04L63/0823—Network architectures or network communication protocols for network security for authentication of entities using certificates
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F21/00—Security arrangements for protecting computers, components thereof, programs or data against unauthorised activity
    • G06F21/60—Protecting data
    • G06F21/64—Protecting data integrity, e.g. using checksums, certificates or signatures
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06Q—INFORMATION AND COMMUNICATION TECHNOLOGY [ICT] SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q40/00—Finance; Insurance; Tax strategies; Processing of corporate or income taxes
    • G06Q40/04—Trading; Exchange, e.g. stocks, commodities, derivatives or currency exchange
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06Q—INFORMATION AND COMMUNICATION TECHNOLOGY [ICT] SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q50/00—Information and communication technology [ICT] specially adapted for implementation of business processes of specific business sectors, e.g. utilities or tourism
    • G06Q50/10—Services
    • G06Q50/18—Legal services
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06Q—INFORMATION AND COMMUNICATION TECHNOLOGY [ICT] SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q50/00—Information and communication technology [ICT] specially adapted for implementation of business processes of specific business sectors, e.g. utilities or tourism
    • G06Q50/10—Services
    • G06Q50/26—Government or public services
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06Q—INFORMATION AND COMMUNICATION TECHNOLOGY [ICT] SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES; SYSTEMS OR METHODS SPECIALLY ADAPTED FOR ADMINISTRATIVE, COMMERCIAL, FINANCIAL, MANAGERIAL OR SUPERVISORY PURPOSES, NOT OTHERWISE PROVIDED FOR
    • G06Q2220/00—Business processing using cryptography

Definitions

  • This application relates to the technical fields of smart contracts and formal verification, in particular to a formal verification method, system, computer equipment and readable storage medium for depositing smart contracts.
  • Blockchain is a distributed data management technology based on data encryption, time stamping, and distributed consensus mechanism to achieve decentralization. It has the characteristics of traceability, non-tampering, and high availability.
  • smart contracts promise to control digital assets and include the rights and obligations agreed by contract participants, which are automatically executed by a computer system.
  • Formal verification is an effective method in the current smart contract security audit scheme. It compares the functional description with the actual code through mathematical logic to check whether the code meets the expected result.
  • the security of the certificated smart contract is the prerequisite for the authenticity and traceability of the certificated result through formal verification and audit.
  • a formal verification method based on a blockchain storage smart contract includes the following steps: (1) Compile a storage smart contract and perform storage verification according to different production environments and permissions , Forensics, and access authorization authorization.
  • Add contract form specification add the storage smart contract described in step (1) to describe the abnormality of the smart contract function, the incoming parameters, the outgoing parameters, the state transfer of persistent variables, and the formal verification of invariants The specification statement.
  • Contract model verification Perform model verification on the smart contract after adding formal verification specifications and obtain verification results. If the formal verification specifications are met, the formal verification is passed, and if the formal verification specifications are not met, the formal verification is located. Verify the location of the unsatisfied statement and the specific location of the smart contract for evidence.
  • the storage smart contract in step (1) satisfies the following conditions:
  • Permission control the modifier is used to control the permission of the method involving the authorization of the storage of evidence, forensic, and access permission.
  • the addition of the contract form specification in step (2) includes:
  • the contract method adds an exception capture specification, including: the sufficient and necessary condition for the exception of the specification requirements in the evidence storage scenario is that the depositor does not have the qualifications for evidence storage and the evidence data is invalid; the sufficient and necessary condition for the exception of the specification requirements in the evidence collection scenario is to obtain evidence The person is not qualified for forensics and the forensic token does not exist; in the event of an exception, all the persistent variables cannot be changed;
  • the contract model verification in step (3) is to use a theorem prover to prove the theorem of the smart contract for which the formal specification is written, and provide the result of the formal verification.
  • This application is a formal verification method based on the blockchain smart contract for attestation, providing blockchain smart contract developers with a process and formal verification for writing attestation smart contracts
  • the method provides a security reference for the development of evidence storage projects equipped with smart contracts on the blockchain.
  • This application adopts the method of formal verification, defines the formal specification in the front of the deposit smart contract method body, transforms it into a mathematical model that can be recognized by the theorem prover, and uses mathematical deduction to obtain the formal verification result, which improves the security of the deposit smart contract And reliability, reducing the testing cost of traditional contract testing, and wide logical coverage.
  • This method has the versatility of writing deposit smart contracts, provides the most basic deposit contract model and its formal verification method, provides relevant references for the expansion and optimization of deposit contracts, and has good applicability.
  • a formal verification method for a deposited smart contract including the following steps:
  • the obtaining of the smart contract for storage of evidence, and granting of the storage of evidence, forensic evidence, and access to the license according to different production environments and permissions include the following steps:
  • mapping type persistent variables to record the identity information of witnesses and forensics, and use array type persistent variables to record the identity information of administrators;
  • Persistent variable records with multiple sets of mapping types conform to the deposit information under multiple deposit modes
  • the modifier is used to control the authorization of the method involving the authorization of the storage of evidence, forensic, and access authorization.
  • the adding a formal specification to the storage smart contract includes the following steps:
  • Add exception capture specifications including: the sufficient and necessary condition for the exception of the specification requirements in the evidence storage scenario is that the depositor is not qualified for evidence and the evidence data is invalid; the sufficient and necessary condition for the exception of the specification requirements in the forensics scenario is that the witness is not qualified to obtain evidence and The forensic token does not exist; in the event of an exception, all the persistent variables cannot be changed;
  • Adding formal verification of incoming and outgoing parameters includes: performing format verification on the parameters passed in by the smart contract function, and performing expected verification on the parameters passed out by the function;
  • the model verification of the attestation smart contract after the formal verification specification statement is added and obtaining the verification result includes the following steps:
  • the theorem prover is used to prove the theorem of the smart contract after the formal verification is added, and the result of the formal verification is given.
  • a formal verification system for depositing smart contracts includes a contract acquisition module, a specification adding module, and a formal verification module.
  • the contract acquisition module is used to obtain the storage certificate smart contract, and grant the storage certificate, obtain the certificate and access the certificate according to different production environments and permissions.
  • the specification adding module is used to add formal verification specification statements to the deposited smart contract, and is used to specify the abnormality of the smart contract function, the input parameter, the output parameter, the state transfer of the persistent variable and the form of the invariant verification.
  • the formal verification module is used to perform model verification on the attestation smart contract after adding formal verification specifications and obtain verification results. If it meets the formal verification specifications, the formal verification passes; if it does not comply with the formal verification specifications, then Locate the position of the sentence that is not satisfied by the formal verification and the position of the deposit smart contract.
  • the contract acquisition module is also used to record the identity information of witnesses and forensics by using persistent variables of mapping type, and record the identity information of administrators by using persistent variables of array type; using multiple sets of mappings Types of persistent variable records conform to the attestation information in multiple attestation modes; the modifier is used to control the authorization of the method involving the authorization of the attestation, forensics, and access authorization.
  • the specification adding module is also used to add an exception capture specification, including: a sufficient and necessary condition for an abnormality in the specification requirements in the evidence storage scenario is that the witness is not qualified for evidence storage and the evidence data is invalid; in the evidence collection scenario The specification requires that the necessary and sufficient condition for the occurrence of an abnormality is that the forensic person has no forensic qualifications and the forensic token does not exist; in the event of an abnormality, all the persistent variables cannot be changed.
  • the specification adding module is also used to add formal verification of incoming and outgoing parameters, including: format verification of the parameters passed in by the smart contract function, and expected verification of the parameters passed out of the function.
  • the specification adding module is also used to add specification instructions for the state transition of persistent data, including: in various types of attestation methods, clearly attested mapping type persistent variables are appended to attested data; in the forensics method In, it is clear that all persistent variables will not be changed; in the method of granting access authorization authority, it is clear that the data in the witness information table is changed.
  • the formal verification module is further configured to use the theorem prover to prove the theorem of the smart contract added with the formal verification specification sentence, and provide the result of the formal verification.
  • a computer device including a memory and a processor, the memory stores a computer program, and the processor implements the above-mentioned formal verification method for a deposited smart contract when the computer program is executed A step of.
  • a computer-readable storage medium on which a computer program is stored, and when the computer program is executed by a processor, the steps of the above-mentioned formal verification method of a deposited smart contract are realized.
  • Fig. 1 is a flowchart of a formal verification of a smart contract based on a blockchain deposit certificate in an embodiment of the application.
  • Fig. 2 is a flowchart of a method for formal verification of a deposited smart contract in an embodiment of the present application.
  • Fig. 3 is a schematic structural diagram of a formal verification system for a deposit smart contract according to an embodiment of the present application.
  • Fig. 4 is an internal structure diagram of a computer device according to an embodiment of the present application.
  • first and second are only used for descriptive purposes, and cannot be understood as indicating or implying relative importance or implicitly indicating the number of indicated technical features. Therefore, the features defined with “first” and “second” may explicitly or implicitly include at least one of the features.
  • a plurality of means at least two, such as two, three, etc., unless specifically defined otherwise.
  • everal means at least one, such as one, two, etc., unless otherwise specifically defined.
  • Fig. 1 is a flow chart of the formal verification of a smart contract based on a blockchain depository certificate provided by an embodiment. As shown in Fig. 1, the process of formal verification of a smart contract based on a blockchain deposit certificate is as follows:
  • Compile a smart contract for evidence storage according to specific production environment and permissions to grant evidence, obtain evidence, and access evidence permissions, it is necessary to standardize the access permissions of the contract method, and the method access can be limited by adding a modifier to the method header Permissions. Limiting the identity of the function caller can improve the overall security and reliability of the system.
  • the deposit certificate function is for users with deposit certificate authority. The user can select the corresponding deposit function according to the deposit type, and persist the deposit data on the blockchain node. The deposit data cannot be tampered with and can be traced back to the administrator.
  • the depositor's certificate authority module the depositor can only perform the deposit operation after obtaining the depositary permission of the administrator. The formal specification should be described.
  • the administrator should be a member of the administrator's persistent data.
  • the depositor information will be Recorded in the persistent data of the witness information, other persistent variables will not change.
  • the forensic function is for users with forensic permission. The user can hold a forensic token to obtain evidence. The forensic function returns the forensic result. The administrator grants the forensic authority to the forensic module. The forensic person can perform the forensic operation only after obtaining the permission of the administrator.
  • the formal specification should be described.
  • the administrator should be a member of the administrator's persistent data.
  • the forensic information will be recorded in the persistent data of the forensic information, and other persistent variables will not change.
  • the authorization of access certificate is for the administrator with the highest authority, and the administrator can manage the authority of the personnel who deposit and obtain evidence.
  • the said storage smart contract meets the following conditions:
  • Permission control encoding to generate persistent variables and contract methods requires adding formal specifications to the contract method, and using modifiers to control the methods involving the authorization of the storage, forensics, and access authorization.
  • the contract method adds an exception capture specification, including: the sufficient and necessary condition for the exception of the specification requirements in the evidence storage scenario is that the depositor does not have the qualifications for evidence storage and the evidence data is invalid; the sufficient and necessary condition for the exception of the specification requirements in the evidence collection scenario is to obtain evidence The person is not qualified for forensics and the forensic token does not exist; in the event of an exception, all the persistent variables cannot be changed;
  • Verification of the smart contract model after adding formal verification specifications refers to the use of theorem prover to prove the theorem of the smart contract written with the formal specifications, and the verification results are obtained. If the formal specifications are met, then The formal verification is passed, and if the formal specification is not met, the sentence location and the specific contract code location that the formal verification does not meet are located.
  • the depositor chooses the appropriate deposit mode for blockchain deposit, and the following conditions must be met to deposit the certificate successfully: the formal specification should be described, the depositor has the qualification to deposit, otherwise throw Exception, the formal verification fails; the data attested is a valid parameter in the attestation mode, otherwise an exception is thrown, and the formal verification fails; the persistent variable of the attestation result in the specific attestation mode is available, otherwise it is thrown If an exception occurs, the formal verification fails; after the deposit is successful, the function returns the format requirements that the forensic token meets, otherwise the formal verification fails; during the deposit process, the deposit result will be recorded in the persistent variable of the deposit result, and others None of the persistent variables are changed.
  • the forensics must meet the following conditions to obtain the forensics successfully: the formal specification should be described, and the forensics are qualified to obtain evidence, otherwise an exception will be thrown and the formal verification fails; the forensic token format conforms The format is required, otherwise an exception will be thrown and the formal verification fails; the forensic token exists in the persistent variable of the attestation, otherwise an exception is thrown, and the formal verification fails; the result of the forensic is the result of the attestation of the corresponding forensic token, otherwise The formal verification fails; during the forensic process, all persistent variables remain unchanged.
  • S110 Obtain a smart contract for evidence storage, and grant evidence storage, forensics, and access permissions according to different production environments and permissions;
  • S120 Add a formal specification statement to the storage smart contract, which is used to describe the abnormality of the smart contract function, the incoming parameters, the outgoing parameters, the state transition of persistent variables, and the formal verification of invariants;
  • S130 Perform model verification on the attestation smart contract after adding formal verification specifications and obtain verification results. If it meets the formal verification specifications, the formal verification is passed; if the formal verification specifications are not met, the formal verification is not satisfied. The location of the statement and the location of the storage smart contract.
  • a method for formal verification of the attestation smart contract is provided for blockchain smart contract developers, which provides a security reference for the development of attestation projects equipped with smart contracts on the blockchain.
  • the formal specification is defined in the front of the deposit smart contract method body, which is transformed into a mathematical model that can be recognized by the theorem prover, and the result of formal verification is obtained by mathematical deduction, which improves the security and reliability of the deposit smart contract and reduces the traditional contract
  • the test cost of the test has a wide range of logic. Provides the most basic deposit contract model and its formal verification method, provides relevant reference for the expansion and optimization of deposit contract, and has good applicability.
  • the obtaining of the storage certificate smart contract, the storage of the evidence, the forensics, and the authorization of the access certificate according to different production environments and permissions include the following steps:
  • mapping type persistent variables to record the identity information of witnesses and forensics, and use array type persistent variables to record the identity information of administrators;
  • Persistent variable records with multiple sets of mapping types conform to the deposit information under multiple deposit modes
  • the modifier is used to control the authorization of the method involving the authorization of the storage of evidence, forensic, and access authorization.
  • the access authority of the contract method needs to be regulated, and the access authority of the method can be limited by adding a modifier to the method header. Limiting the identity of the function caller can improve the overall security and reliability of the system.
  • the deposit certificate function is for users with deposit certificate authority. The user can select the corresponding deposit function according to the deposit type, and persist the deposit data on the blockchain node. The deposit data cannot be tampered with and can be traced back to the administrator.
  • the depositor's certificate authority module the depositor can only perform the deposit operation after obtaining the depositary permission of the administrator.
  • the formal specification should be described.
  • the administrator should be a member of the administrator's persistent data. The depositor information will be Recorded in the persistent data of the witness information, other persistent variables will not change.
  • the forensic function is for users with forensic permission.
  • the user can hold a forensic token to obtain evidence.
  • the forensic function returns the forensic result.
  • the administrator grants the forensic authority to the forensic module.
  • the forensic person can perform the forensic operation only after obtaining the permission of the administrator.
  • the formal specification should be described.
  • the administrator should be a member of the administrator's persistent data.
  • the forensic information will be recorded in the persistent data of the forensic information, and other persistent variables will not change.
  • the authorization of access certificate is for the administrator with the highest authority, and the administrator can manage the authority of the personnel who deposit and obtain evidence.
  • the adding of formal normative sentences to the deposit smart contract includes the following steps:
  • Add exception capture specifications including: the sufficient and necessary condition for the exception of the specification requirements in the evidence storage scenario is that the depositor is not qualified for evidence and the evidence data is invalid; the sufficient and necessary condition for the exception of the specification requirements in the forensics scenario is that the witness is not qualified to obtain evidence and The forensic token does not exist; in the event of an exception, all the persistent variables cannot be changed;
  • Adding formal verification of incoming and outgoing parameters includes: performing format verification on the parameters passed in by the smart contract function, and performing expected verification on the parameters passed out by the function;
  • the depositor chooses a suitable deposit model for blockchain deposit, and the following conditions must be met for the deposit to be successful: the formal specification should be described, and the depositor has the qualification to deposit, Otherwise, an exception is thrown, and the formal verification fails; the data attested is a valid parameter in the attestation mode; otherwise, an exception is thrown, and the formal verification fails; the persistent variables of the attestation result in the specific attestation mode are available , Otherwise an exception is thrown and the formal verification fails; after the deposit is successful, the function returns the format requirements of the forensic token, otherwise the formal verification fails; during the deposit process, the deposit result will be recorded in the persistent variable of the deposit result , Other persistent variables will not change.
  • the forensics must meet the following conditions to obtain the forensics successfully: the formal specification should be described, and the forensics are qualified to obtain evidence, otherwise an exception will be thrown and the formal verification fails; the forensic token format conforms The format is required, otherwise an exception will be thrown and the formal verification fails; the forensic token exists in the persistent variable of the attestation, otherwise an exception is thrown, and the formal verification fails; the result of the forensic is the result of the attestation of the corresponding forensic token, otherwise The formal verification fails; during the forensic process, all persistent variables remain unchanged.
  • the model verification of the attestation smart contract after the formal verification specification statement is added and obtaining the verification result includes the following steps:
  • the theorem prover is used to prove the theorem of the smart contract after the formal verification is added, and the result of the formal verification is given.
  • a formal verification system for depositing smart contracts including: contract acquisition module 210, specification addition module 220, and formal verification module 230.
  • the contract acquisition module 210 is used to acquire a smart contract for depositing evidence, and granting permission for depositing evidence, obtaining evidence, and accessing evidence according to different production environments and permissions.
  • the specification adding module 220 is used to add formal verification specification statements to the deposited smart contract, and is used to specify the abnormality of the smart contract function, the incoming parameters, the outgoing parameters, the state transfer of the persistent variables, and the invariants. Formal verification.
  • the formal verification module 230 is used to perform model verification on the attestation smart contract after adding formal verification specifications and obtain verification results. If it meets the formal verification specifications, the formal verification passes; if it does not comply with the formal verification specifications, Then locate the position of the sentence that is not satisfied by the formal verification and the position of the deposited smart contract.
  • the contract acquisition module 210 is also used to record the identity information of the witness and the forensic by using persistent variables of the mapping type, and record the identity information of the administrator by using the persistent variables of the array type; using multiple sets of mappings Types of persistent variable records conform to the attestation information in multiple attestation modes; the modifier is used to control the authorization of the method involving the authorization of the attestation, forensics, and access authorization.
  • the specification adding module 220 is also used to add an exception capture specification, including: a sufficient and necessary condition for an exception in the specification requirement in the evidence deposit scenario is that the depositor does not have the certification qualification and the deposit data is invalid; in the evidence collection scenario The specification requires that the necessary and sufficient condition for the occurrence of an abnormality is that the forensic person has no forensic qualifications and the forensic token does not exist; in the event of an abnormality, all the persistent variables cannot be changed.
  • the specification adding module 220 is also used to add formal verification of incoming and outgoing parameters, including: performing format verification on the parameters passed in by the smart contract function, and performing expected verification on the parameters passed out by the function.
  • the specification adding module 220 is also used to add specification instructions for the state transition of persistent data, including: in various types of attestation methods, the mapping type persistent variables that are clearly attested are appended to attestation data; in forensics In the method, it is clear that all persistent variables will not be changed; in the method of granting access forensic authority, it is clear that the data in the witness information table is changed.
  • the formal verification module 230 is further configured to use a theorem prover to prove the theorem of the smart contract after the formal verification specification sentence is added, and provide the result of the formal verification.
  • the various modules in the formal verification system of the above-mentioned storage smart contract can be implemented in whole or in part by software, hardware, and combinations thereof.
  • the foregoing modules may be embedded in the form of hardware or independent of the processor in the computer device, or may be stored in the memory of the computer device in the form of software, so that the processor can call and execute the operations corresponding to the foregoing modules.
  • a computer device is provided.
  • the computer device may be a terminal, and its internal structure diagram may be as shown in FIG. 4.
  • the computer equipment includes a processor, a memory, a network interface, a display screen and an input device connected through a system bus.
  • the processor of the computer device is used to provide calculation and control capabilities.
  • the memory of the computer device includes a non-volatile storage medium and an internal memory.
  • the non-volatile storage medium stores an operating system and a computer program.
  • the internal memory provides an environment for the operation of the operating system and computer programs in the non-volatile storage medium.
  • the network interface of the computer device is used to communicate with an external terminal through a network connection.
  • the computer program is executed by the processor to realize a formal verification method for depositing smart contracts.
  • the display screen of the computer equipment can be a liquid crystal display screen or an electronic ink display screen
  • the input device of the computer equipment can be a touch layer covered on the display screen, or it can be a button, a trackball or a touchpad set on the housing of the computer equipment , It can also be an external keyboard, touchpad, or mouse.
  • FIG. 4 is only a block diagram of a part of the structure related to the solution of the present application, and does not constitute a limitation on the computer device to which the solution of the present application is applied.
  • the specific computer device may Including more or fewer parts than shown in the figure, or combining some parts, or having a different arrangement of parts.
  • a computer device including a memory and a processor, and a computer program is stored in the memory.
  • the processor implements the steps of the above-mentioned formal verification method for a deposited smart contract when the processor executes the computer program.
  • a computer-readable storage medium on which a computer program is stored, and when the computer program is executed by a processor, the steps of the formal verification method for the above-mentioned deposited smart contract are realized.
  • Non-volatile memory may include read only memory (ROM), programmable ROM (PROM), electrically programmable ROM (EPROM), electrically erasable programmable ROM (EEPROM), or flash memory.
  • Volatile memory may include random access memory (RAM) or external cache memory.
  • RAM is available in many forms, such as static RAM (SRAM), dynamic RAM (DRAM), synchronous DRAM (SDRAM), double data rate SDRAM (DDRSDRAM), enhanced SDRAM (ESDRAM), synchronous chain Channel (Synchlink) DRAM (SLDRAM), memory bus (Rambus) direct RAM (RDRAM), direct memory bus dynamic RAM
  • DRAM memory bus dynamic RAM
  • RDRAM memory bus dynamic RAM

Landscapes

  • Engineering & Computer Science (AREA)
  • Business, Economics & Management (AREA)
  • Theoretical Computer Science (AREA)
  • Computer Security & Cryptography (AREA)
  • Physics & Mathematics (AREA)
  • General Physics & Mathematics (AREA)
  • Health & Medical Sciences (AREA)
  • General Health & Medical Sciences (AREA)
  • General Engineering & Computer Science (AREA)
  • Computer Hardware Design (AREA)
  • Tourism & Hospitality (AREA)
  • Software Systems (AREA)
  • Bioethics (AREA)
  • Economics (AREA)
  • General Business, Economics & Management (AREA)
  • Strategic Management (AREA)
  • Marketing (AREA)
  • Finance (AREA)
  • Technology Law (AREA)
  • Human Resources & Organizations (AREA)
  • Development Economics (AREA)
  • Accounting & Taxation (AREA)
  • Primary Health Care (AREA)
  • Computing Systems (AREA)
  • Computer Networks & Wireless Communication (AREA)
  • Signal Processing (AREA)
  • Educational Administration (AREA)
  • Storage Device Security (AREA)
  • Debugging And Monitoring (AREA)
  • Management, Administration, Business Operations System, And Electronic Commerce (AREA)

Abstract

一种存证智能合约的形式验证方法、系统、计算机设备和可读存储介质，该方法包括获取存证智能合约、添加合约形式规范并进行合约模型验证。该方法为区块链智能合约开发者提供了存证智能合约的形式验证方法，为区块链搭载智能合约开发存证项目提供了安全方面的参考。通过形式验证的方法，在存证智能合约方法体前部定义形式规范，转化为定理证明器能够识别的数学模型，利用数学推演得出形式验证结果，提高了存证智能合约的安全性和可靠性，降低了传统合约测试的测试成本，逻辑覆盖面广。上述方法具有针对存证智能合约的通用性，提供了最基本的存证合约模型及其形式验证方法，为存证合约的扩展和优化提供了相关参考，具有很好的适用性。

Description

存证智能合约的形式验证方法、系统、计算机设备和可读存储介质
相关申请
本申请要求2019年8月21日申请的，申请号为201910772491.4，发明名称为“一种基于区块链存证智能合约的形式验证方法”的中国专利申请的优先权，其全部内容通过引用结合在本申请中。
技术领域
本申请涉及智能合约和形式验证技术领域，特别是涉及一种存证智能合约的形式验证方法、系统、计算机设备和可读存储介质。
背景技术
区块链是一种基于数据加密、时间戳、分布式共识机制实现去中心化的分布式数据管理技术，具有可追溯、不可篡改、高可用的特点。智能合约作为一套以数字形式定义的承诺，承诺控制着数字资产并包含了合约参与者约定的权利和义务，由计算机系统自动执行。区块链技术的出现为智能合约提供了一套能够支持可编程的数字系统。形式验证是目前智能合约安全审计方案中行之有效的方法，其通过数学逻辑将功能描述与实际代码进行比较，从而检查代码是否符合预期结果。存证智能合约作为常见的合约应用领域，通过形式验证审计其安全性是存证结果真实可信、可追溯的前提。但是目前智能合约开发社区并没有针对存证业务相应的安全规范，使得开发存证智能合约容易出现安全漏洞，需要一套针对存证智能合约的开发流程规范以及基于形式验证的存证智能合约模板，为存证智能合约的设计和开发提供安全方面的重要参考。
发明内容
根据本申请的各种实施例，提供一种基于区块链存证智能合约的形式验证方法，所述方法包括以下步骤：(1)编写存证智能合约，根据不同生产环境和权限进行存证、取证、存取证权限授予。
(2)添加合约形式规范：将步骤(1)所述存证智能合约添加用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移、不变量的形式验证的规范语句。
(3)合约模型验证：对添加形式验证规范后的智能合约进行模型验证并得出验证结 果，若符合所述形式验证规范则形式验证通过，若不符合所述形式验证规范则定位所述形式验证不满足的语句位置以及具体的存证证智能合约位置。
在其中一个实施例中，步骤(1)所述存证智能合约满足以下条件：
(a)存证人、取证人、管理员的数据结构：利用映射类型的持久化变量来记录存证、取证人的身份信息，利用数组类型的持久化变量来记录管理员的身份信息；
(b)存储存证信息的数据结构：利用多组映射类型的持久化变量来记录符合多种存证模式下的存证信息；
(c)权限控制：利用修饰器对涉及所述存证、取证、存取证权限授予的方法进行权限控制。
在其中一个实施例中，步骤(2)所述合约形式规范的添加包括：
(a)合约方法添加异常捕捉规范，包括：存证场景下规范要求发生异常的充分必要条件是存证人没有存证资格且存证数据无效；取证场景下规范要求发生异常的充分必要条件是取证人没有取证资格且取证令牌不存在；在发生异常的情况下，所有所述持久化变量不能被改变；
(b)合约方法传入、传出参数的形式校验，规范要求对函数传入的参数进行格式校验，对函数传出的参数进行期望校验；
(c)合约方法对持久化数据状态转移的规范说明，规范要求在各种类型的存证方法中，明确存证的映射类型持久化变量得到存证数据的追加；在取证方法中，明确所有的持久化变量不被改变；在存取证权限授予方法中，明确存取证人信息表数据的改变。
在其中一个实施例中，步骤(3)所述合约模型验证是利用定理证明器对编写所述形式规范的智能合约进行定理证明，并给出形式验证的结果。
与现有技术相比，本申请的有益效果如下：本申请是基于区块链存证智能合约的形式验证方法，为区块链智能合约开发者提供了编写存证智能合约的流程和形式验证方法，为区块链搭载智能合约开发存证项目提供了安全方面的参考。本申请通过形式验证的方法，在存证智能合约方法体前部定义形式规范，转化为定理证明器能够识别的数学模型，利用数学推演得出形式验证结果，提高了存证智能合约的安全性和可靠性，降低了传统合约测试的测试成本，逻辑覆盖面广。本方法具有编写存证智能合约的通用性，提供了最基本的存证合约模型及其形式验证方法，为存证合约的扩展和优化提供了相关参考，具有很好的适用性。
根据本申请的各种实施例，还提供一种存证智能合约的形式验证方法，所述方法包括以下步骤：
获取存证智能合约，根据不同生产环境和权限进行存证、取证和存取证权限授予；
对所述存证智能合约添加形式规范的规范语句，用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移和不变量的形式验证；
对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果，若符合形式验证规范，则形式验证通过；若不符合所述形式验证规范，则定位形式验证不满足的语句位置以及存证智能合约的位置。
在其中一个实施例中，所述获取存证智能合约，根据不同生产环境和权限进行存证、取证和存取证权限授予包括以下步骤：
采用映射类型的持久化变量记录存证人和取证人的身份信息，采用数组类型的持久化变量记录管理员的身份信息；
采用多组映射类型的持久化变量记录符合多种存证模式下的存证信息；
采用修饰器对涉及所述存证、取证、存取证权限授予的方法进行权限控制。
在其中一个实施例中，所述对所述存证智能合约添加形式规范的规范语句包括以下步骤：
添加异常捕捉规范，包括：存证场景下规范要求发生异常的充分必要条件是存证人没有存证资格且存证数据无效；取证场景下规范要求发生异常的充分必要条件是取证人没有取证资格且取证令牌不存在；在发生异常的情况下，所有所述持久化变量不能被改变；
添加传入、传出参数的形式校验，包括：对所述智能合约函数传入的参数进行格式校验，对函数传出的参数进行期望校验；
添加对持久化数据状态转移的规范说明，包括：在各种类型的存证方法中，明确存证的映射类型持久化变量得到存证数据的追加；在取证方法中，明确所有的持久化变量不被改变；在存取证权限授予方法中，明确存取证人信息表数据的改变。
在其中一个实施例中，所述对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果包括以下步骤：
采用定理证明器对所述添加形式验证的规范语句后的智能合约进行定理证明，并给出形式验证的结果。
根据本申请的各种实施例，还提供一种存证智能合约的形式验证系统，所述系统包括：合约获取模块、规范添加模块和形式验证模块。
所述合约获取模块用于获取存证智能合约，根据不同生产环境和权限进行存证、取证和存取证权限授予。
所述规范添加模块用于对所述存证智能合约添加形式验证的规范语句，用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移和不变量的形式验证。
所述形式验证模块用于对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果，若符合形式验证规范，则形式验证通过；若不符合所述形式验证规范，则定位形式验证不满足的语句位置以及存证智能合约的位置。
在其中一个实施例中，所述合约获取模块还用于采用映射类型的持久化变量记录存证人和取证人的身份信息，采用数组类型的持久化变量记录管理员的身份信息；采用多组映射类型的持久化变量记录符合多种存证模式下的存证信息；采用修饰器对涉及所述存证、取证、存取证权限授予的方法进行权限控制。
在其中一个实施例中，所述规范添加模块还用于添加异常捕捉规范，包括：存证场景下规范要求发生异常的充分必要条件是存证人没有存证资格且存证数据无效；取证场景下规范要求发生异常的充分必要条件是取证人没有取证资格且取证令牌不存在；在发生异常的情况下，所有所述持久化变量不能被改变。
所述规范添加模块还用于添加传入、传出参数的形式校验，包括：对所述智能合约函数传入的参数进行格式校验，对函数传出的参数进行期望校验。
所述规范添加模块还用于添加对持久化数据状态转移的规范说明，包括：在各种类型的存证方法中，明确存证的映射类型持久化变量得到存证数据的追加；在取证方法中，明确所有的持久化变量不被改变；在存取证权限授予方法中，明确存取证人信息表数据的改变。
在其中一个实施例中，所述形式验证模块还用于采用定理证明器对所述添加形式验证的规范语句后的智能合约进行定理证明，并给出形式验证的结果。
根据本申请的各种实施例，还提供一种计算机设备，包括存储器和处理器，所述存储器存储有计算机程序，所述处理器执行所述计算机程序时实现上述存证智能合约的形式验证方法的步骤。
根据本申请的各种实施例，还提供一种计算机可读存储介质，其上存储有计算机程序，所述计算机程序被处理器执行时实现上述存证智能合约的形式验证方法的步骤。
附图说明
为了更好地描述和说明这里公开的那些发明的实施例和/或示例，可以参考一幅或多幅附图。用于描述附图的附加细节或示例不应当被认为是对所公开的发明、目前描述的实施例和/或示例以及目前理解的这些发明的最佳模式中的任何一者的范围的限制。
图1是本申请实施例的基于区块链存证智能合约形式验证的流程图。
图2是本申请实施例的存证智能合约的形式验证方法的流程图。
图3是本申请实施例的存证智能合约的形式验证系统的结构示意图。
图4是本申请实施例的计算机设备的内部结构图。
具体实施方式
为了便于理解本申请，为使本申请的上述目的、特征和优点能够更加明显易懂，下面结合附图对本申请的具体实施方式做详细的说明。在下面的描述中阐述了很多具体细节以便于充分理解本申请，附图中给出了本申请的较佳实施方式。但是，本申请可以以许多不同的形式来实现，并不限于本文所描述的实施方式。相反地，提供这些实施方式的目的是使对本申请的公开内容理解的更加透彻全面。本申请能够以很多不同于在此描述的其它方式来实施，本领域技术人员可以在不违背本申请内涵的情况下做类似改进，因此本申请不受下面公开的具体实施例的限制。
此外，术语“第一”、“第二”仅用于描述目的，而不能理解为指示或暗示相对重要性或者隐含指明所指示的技术特征的数量。由此，限定有“第一”、“第二”的特征可以明示或者隐含地包括至少一个该特征。在本申请的描述中，“多个”的含义是至少两个，例如两个，三个等，除非另有明确具体的限定。在本申请的描述中，“若干”的含义是至少一个，例如一个，两个等，除非另有明确具体的限定。
除非另有定义，本文所使用的所有的技术和科学术语与属于本申请的技术领域的技术人员通常理解的含义相同。本文中所使用的术语只是为了描述具体的实施方式的目的，不是旨在于限制本申请。本文所使用的术语“及/或”包括一个或多个相关的所列项目的任意的和所有的组合。
图1为一实施例提供的基于区块链存证智能合约形式验证的流程图，如图1所示，基于区块链存证智能合约形式验证的流程如下：
(1)编写存证智能合约：根据特定生产环境和权限进行存证、取证、存取证权限授予，需要规范合约方法的访问权限，可以通过在方法头部添加修饰器的方式限定方法的访问权限。限定函数调用者的身份，可以提高系统整体的安全性和可靠性。存证功能是面向具有存证权限的用户，用户可以根据存证类型选择对应的存证函数，将存证数据持久化至区块链节点上，存证数据不可篡改且可追溯，管理员授予存证者存证权限模块，存证者得到管理员的存证允许后才可以进行存证操作，形式规范应描述，管理员应是管理员持久化数据中的一员，存证人信息将被记录到存证人信息的持久化数据中，其他持久化变量均不发生改变。取证函数是面向具有取证权限的用户，用户可以持有取证令牌进行取证，取证函数返回取证结果，管理员授予取证者取证权限模块，取证者得到管理员的取证允许后才可以进行取证操作，形式规范应描述，管理员应是管理员持久化数据中的一员，取证人信息将被记录到取证人信息的持 久化数据中，其他持久化变量均不发生改变。存取证权限授予是面向最高权限的管理员，管理员可以对存证、取证的人员进行权限管理。
所述存证智能合约满足以下条件：
(a)存证人、取证人、管理员的数据结构：利用映射类型的持久化变量来记录存证、取证人的身份信息，利用数组类型的持久化变量来记录管理员的身份信息；
(b)存储存证信息的数据结构：利用多组映射类型的持久化变量来记录符合多种存证模式下的存证信息；
(c)权限控制：编码生成持久化变量和合约方法，需要为合约方法添加形式规范，利用修饰器对涉及所述存证、取证、存取证权限授予的方法进行权限控制。
(2)添加合约形式规范：将步骤(1)所述存证智能合约添加用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移、不变量的形式验证的规范语句。所述形式规范语句必须能够清晰、无歧义地描述方法的期望运作流程，保证形式验证结果的正确性。
所述合约形式规范的添加包括：
(a)合约方法添加异常捕捉规范，包括：存证场景下规范要求发生异常的充分必要条件是存证人没有存证资格且存证数据无效；取证场景下规范要求发生异常的充分必要条件是取证人没有取证资格且取证令牌不存在；在发生异常的情况下，所有所述持久化变量不能被改变；
(b)合约方法传入、传出参数的形式校验，规范要求对函数传入的参数进行格式校验，对函数传出的参数进行期望校验；
(c)合约方法对持久化数据状态转移的规范说明，规范要求在各种类型的存证方法中，明确存证的映射类型持久化变量得到了存证数据的追加；在取证方法中，明确所有的持久化变量不被改变；在存取证权限授予方法中，明确存取证人信息表数据的改变。
(3)合约模型验证：对添加形式验证规范后的智能合约模型验证是指利用定理证明器对编写所述形式规范的智能合约进行定理证明，并得出验证结果，若符合所述形式规范则形式验证通过，若不符合所述形式规范则定位所述形式验证不满足的语句位置以及具体的合约代码位置。
对于存证者存证模块，存证者选择合适的存证模式进行区块链存证，需要满足以下条件才能存证成功：形式规范应描述，存证者具有存证的资格，否则抛出异常，形式验证不通过；存证的数据是该存证模式下的有效参数，否则抛出异常，形式验证不通过；在特定存证模式下的存证结果持久化变量是可用的，否则抛出异常，形式验证不通过；存证成功后函数 返回取证令牌符合的格式要求，否则形式验证不通过；存证过程中，存证结果将被记录到存证结果的持久化变量中，其他持久化变量均不发生改变。
对于取证者取证模块，取证者进行区块链取证，需要满足以下条件才能取证成功：形式规范应描述，取证者具有取证的资格，否则抛出异常，形式验证不通过；取证者令牌格式符合格式要求，否则抛出异常，形式验证不通过；取证令牌存在于存证的持久化变量中，否则抛出异常，形式验证不通过；取证的结果是对应取证令牌的存证结果，否则形式验证不通过；取证过程中，所有的持久化变量都不发生改变。
进一步的，针对存证智能合约，如图2所示，可以采用以下方案实现形式验证：
S110：获取存证智能合约，根据不同生产环境和权限进行存证、取证和存取证权限授予；
S120：对所述存证智能合约添加形式规范的规范语句，用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移和不变量的形式验证；
S130：对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果，若符合形式验证规范，则形式验证通过；若不符合所述形式验证规范，则定位形式验证不满足的语句位置以及存证智能合约的位置。
在本实施例中，为区块链智能合约开发者提供了对存证智能合约进行形式验证的方法，为区块链搭载智能合约开发存证项目提供了安全方面的参考。在存证智能合约方法体前部定义形式规范，转化为定理证明器能够识别的数学模型，利用数学推演得出形式验证结果，提高了存证智能合约的安全性和可靠性，降低了传统合约测试的测试成本，逻辑覆盖面广。提供了最基本的存证合约模型及其形式验证方法，为存证合约的扩展和优化提供了相关参考，具有很好的适用性。
在一个实施例中，所述获取存证智能合约，根据不同生产环境和权限进行存证、取证和存取证权限授予包括以下步骤：
采用映射类型的持久化变量记录存证人和取证人的身份信息，采用数组类型的持久化变量记录管理员的身份信息；
采用多组映射类型的持久化变量记录符合多种存证模式下的存证信息；
采用修饰器对涉及所述存证、取证、存取证权限授予的方法进行权限控制。
在本实施例中，需要规范合约方法的访问权限，可以通过在方法头部添加修饰器的方式限定方法的访问权限。限定函数调用者的身份，可以提高系统整体的安全性和可靠性。存证功能是面向具有存证权限的用户，用户可以根据存证类型选择对应的存证函数，将存证数据持久化至区块链节点上，存证数据不可篡改且可追溯，管理员授予存证者存证权限模块，存证者得到管理员的存证允许后才可以进行存证操作，形式规范应描述，管理员应是管理员 持久化数据中的一员，存证人信息将被记录到存证人信息的持久化数据中，其他持久化变量均不发生改变。取证函数是面向具有取证权限的用户，用户可以持有取证令牌进行取证，取证函数返回取证结果，管理员授予取证者取证权限模块，取证者得到管理员的取证允许后才可以进行取证操作，形式规范应描述，管理员应是管理员持久化数据中的一员，取证人信息将被记录到取证人信息的持久化数据中，其他持久化变量均不发生改变。存取证权限授予是面向最高权限的管理员，管理员可以对存证、取证的人员进行权限管理。
在一个实施例中，所述对所述存证智能合约添加形式规范的规范语句包括以下步骤：
添加异常捕捉规范，包括：存证场景下规范要求发生异常的充分必要条件是存证人没有存证资格且存证数据无效；取证场景下规范要求发生异常的充分必要条件是取证人没有取证资格且取证令牌不存在；在发生异常的情况下，所有所述持久化变量不能被改变；
添加传入、传出参数的形式校验，包括：对所述智能合约函数传入的参数进行格式校验，对函数传出的参数进行期望校验；
添加对持久化数据状态转移的规范说明，包括：在各种类型的存证方法中，明确存证的映射类型持久化变量得到存证数据的追加；在取证方法中，明确所有的持久化变量不被改变；在存取证权限授予方法中，明确存取证人信息表数据的改变。
具体的，对于存证者存证模块，存证者选择合适的存证模式进行区块链存证，需要满足以下条件才能存证成功：形式规范应描述，存证者具有存证的资格，否则抛出异常，形式验证不通过；存证的数据是该存证模式下的有效参数，否则抛出异常，形式验证不通过；在特定存证模式下的存证结果持久化变量是可用的，否则抛出异常，形式验证不通过；存证成功后函数返回取证令牌符合的格式要求，否则形式验证不通过；存证过程中，存证结果将被记录到存证结果的持久化变量中，其他持久化变量均不发生改变。
对于取证者取证模块，取证者进行区块链取证，需要满足以下条件才能取证成功：形式规范应描述，取证者具有取证的资格，否则抛出异常，形式验证不通过；取证者令牌格式符合格式要求，否则抛出异常，形式验证不通过；取证令牌存在于存证的持久化变量中，否则抛出异常，形式验证不通过；取证的结果是对应取证令牌的存证结果，否则形式验证不通过；取证过程中，所有的持久化变量都不发生改变。
在一个实施例中，所述对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果包括以下步骤：
采用定理证明器对所述添加形式验证的规范语句后的智能合约进行定理证明，并给出形式验证的结果。
在一个实施例中，如图3所示，提供了一种存证智能合约的形式验证系统，包括：合 约获取模块210、规范添加模块220和形式验证模块230。
所述合约获取模块210用于获取存证智能合约，根据不同生产环境和权限进行存证、取证和存取证权限授予。
所述规范添加模块220用于对所述存证智能合约添加形式验证的规范语句，用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移和不变量的形式验证。
所述形式验证模块230用于对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果，若符合形式验证规范，则形式验证通过；若不符合所述形式验证规范，则定位形式验证不满足的语句位置以及存证智能合约的位置。
在一个实施例中，所述合约获取模块210还用于采用映射类型的持久化变量记录存证人和取证人的身份信息，采用数组类型的持久化变量记录管理员的身份信息；采用多组映射类型的持久化变量记录符合多种存证模式下的存证信息；采用修饰器对涉及所述存证、取证、存取证权限授予的方法进行权限控制。
在一个实施例中，所述规范添加模块220还用于添加异常捕捉规范，包括：存证场景下规范要求发生异常的充分必要条件是存证人没有存证资格且存证数据无效；取证场景下规范要求发生异常的充分必要条件是取证人没有取证资格且取证令牌不存在；在发生异常的情况下，所有所述持久化变量不能被改变。
所述规范添加模块220还用于添加传入、传出参数的形式校验，包括：对所述智能合约函数传入的参数进行格式校验，对函数传出的参数进行期望校验。
所述规范添加模块220还用于添加对持久化数据状态转移的规范说明，包括：在各种类型的存证方法中，明确存证的映射类型持久化变量得到存证数据的追加；在取证方法中，明确所有的持久化变量不被改变；在存取证权限授予方法中，明确存取证人信息表数据的改变。
在一个实施例中，所述形式验证模块230还用于采用定理证明器对所述添加形式验证的规范语句后的智能合约进行定理证明，并给出形式验证的结果。
关于存证智能合约的形式验证系统的具体限定可以参见上文中对于存证智能合约的形式验证方法的限定，在此不再赘述。上述存证智能合约的形式验证系统中的各个模块可全部或部分通过软件、硬件及其组合来实现。上述各模块可以硬件形式内嵌于或独立于计算机设备中的处理器中，也可以以软件形式存储于计算机设备中的存储器中，以便于处理器调用执行以上各个模块对应的操作。
在一个实施例中，提供了一种计算机设备，该计算机设备可以是终端，其内部结构图 可以如图4所示。该计算机设备包括通过系统总线连接的处理器、存储器、网络接口、显示屏和输入装置。其中，该计算机设备的处理器用于提供计算和控制能力。该计算机设备的存储器包括非易失性存储介质、内存储器。该非易失性存储介质存储有操作系统和计算机程序。该内存储器为非易失性存储介质中的操作系统和计算机程序的运行提供环境。该计算机设备的网络接口用于与外部的终端通过网络连接通信。该计算机程序被处理器执行时以实现一种存证智能合约的形式验证方法。该计算机设备的显示屏可以是液晶显示屏或者电子墨水显示屏，该计算机设备的输入装置可以是显示屏上覆盖的触摸层，也可以是计算机设备外壳上设置的按键、轨迹球或触控板，还可以是外接的键盘、触控板或鼠标等。
本领域技术人员可以理解，图4中示出的结构，仅仅是与本申请方案相关的部分结构的框图，并不构成对本申请方案所应用于其上的计算机设备的限定，具体的计算机设备可以包括比图中所示更多或更少的部件，或者组合某些部件，或者具有不同的部件布置。
在一个实施例中，提供了一种计算机设备，包括存储器和处理器，存储器中存储有计算机程序，该处理器执行计算机程序时实现上述存证智能合约的形式验证方法的步骤。
在一个实施例中，提供了一种计算机可读存储介质，其上存储有计算机程序，计算机程序被处理器执行时实现上述存证智能合约的形式验证方法的步骤。
本领域普通技术人员可以理解实现上述实施例方法中的全部或部分流程，是可以通过计算机程序来指令相关的硬件来完成，所述的计算机程序可存储于一非易失性计算机可读取存储介质中，该计算机程序在执行时，可包括如上述各方法的实施例的流程。其中，本申请所提供的各实施例中所使用的对存储器、存储、数据库或其它介质的任何引用，均可包括非易失性和/或易失性存储器。非易失性存储器可包括只读存储器(ROM)、可编程ROM(PROM)、电可编程ROM(EPROM)、电可擦除可编程ROM(EEPROM)或闪存。易失性存储器可包括随机存取存储器(RAM)或者外部高速缓冲存储器。作为说明而非局限，RAM以多种形式可得，诸如静态RAM(SRAM)、动态RAM(DRAM)、同步DRAM(SDRAM)、双数据率SDRAM(DDRSDRAM)、增强型SDRAM(ESDRAM)、同步链路(Synchlink)DRAM(SLDRAM)、存储器总线(Rambus)直接RAM(RDRAM)、直接存储器总线动态RAM
(DRDRAM)、以及存储器总线动态RAM(RDRAM)等。
以上所述实施例的各技术特征可以进行任意的组合，为使描述简洁，未对上述实施例中的各个技术特征所有可能的组合都进行描述，然而，只要这些技术特征的组合不存在矛盾，都应当认为是本说明书记载的范围。
以上所述实施例仅表达了本发明的几种实施方式，其描述较为具体和详细，但并不能因此而理解为对发明专利范围的限制。应当指出的是，对于本领域的普通技术人员来说，在 不脱离本发明构思的前提下，还可以做出若干变形和改进，这些都属于本发明的保护范围。因此，本发明专利的保护范围应以所附权利要求为准。

Claims (11)

  1. 一种存证智能合约的形式验证方法，其特征在于，所述方法包括以下步骤：
    获取存证智能合约，根据不同生产环境和权限进行存证、取证和存取证权限授予；
    对所述存证智能合约添加形式规范的规范语句，用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移和不变量的形式验证；
    对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果，若符合形式验证规范，则形式验证通过；若不符合所述形式验证规范，则定位形式验证不满足的语句位置以及存证智能合约的位置。
  2. 根据权利要求1所述的存证智能合约的形式验证方法，其特征在于，所述获取存证智能合约，根据不同生产环境和权限进行存证、取证和存取证权限授予包括以下步骤：
    采用映射类型的持久化变量记录存证人和取证人的身份信息，采用数组类型的持久化变量记录管理员的身份信息；
    采用多组映射类型的持久化变量记录符合多种存证模式下的存证信息；
    采用修饰器对涉及所述存证、取证、存取证权限授予的方法进行权限控制。
  3. 根据权利要求1所述的存证智能合约的形式验证方法，其特征在于，所述对所述存证智能合约添加形式规范的规范语句包括以下步骤：
    添加异常捕捉规范，包括：存证场景下规范要求发生异常的充分必要条件是存证人没有存证资格且存证数据无效；取证场景下规范要求发生异常的充分必要条件是取证人没有取证资格且取证令牌不存在；在发生异常的情况下，所有所述持久化变量不能被改变；
    添加传入、传出参数的形式校验，包括：对所述智能合约函数传入的参数进行格式校验，对函数传出的参数进行期望校验；
    添加对持久化数据状态转移的规范说明，包括：在各种类型的存证方法中，明确存证的映射类型持久化变量得到存证数据的追加；在取证方法中，明确所有的持久化变量不被改变；在存取证权限授予方法中，明确存取证人信息表数据的改变。
  4. 根据权利要求1所述的存证智能合约的形式验证方法，其特征在于，所述对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果包括以下步骤：
    采用定理证明器对所述添加形式验证的规范语句后的智能合约进行定理证明，并给出形式验证的结果。
  5. 一种存证智能合约的形式验证系统，其特征在于，所述系统包括合约获取模块、规范添加模块和形式验证模块；
    所述合约获取模块用于获取存证智能合约，根据不同生产环境和权限进行存证、取证和 存取证权限授予；
    所述规范添加模块用于对所述存证智能合约添加形式验证的规范语句，用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移和不变量的形式验证；
    所述形式验证模块用于对添加形式验证的规范语句后的存证智能合约进行模型验证并得出验证结果，若符合形式验证规范，则形式验证通过；若不符合所述形式验证规范，则定位形式验证不满足的语句位置以及存证智能合约的位置。
  6. 一种计算机设备，包括存储器和处理器，所述存储器存储有计算机程序，其特征在于，所述处理器执行所述计算机程序时实现权利要求1至4中任意一项所述存证智能合约的形式验证方法的步骤。
  7. 一种可读存储介质，其上存储有计算机程序，其特征在于，所述计算机程序被处理器执行时实现权利要求1至4中任意一项所述存证智能合约的形式验证方法的步骤。
  8. 一种基于区块链存证智能合约的形式验证方法，其特征在于，所述方法具体包括以下步骤：
    (1)编写存证智能合约，根据不同生产环境和权限进行存证、取证、存取证权限授予；
    (2)添加合约形式规范：将步骤(1)所述存证智能合约添加用于规范描述智能合约函数的异常、传入参数、传出参数、持久化变量的状态转移、不变量的形式验证的规范语句；
    (3)合约模型验证：对添加形式验证规范后的智能合约进行模型验证并得出验证结果，若符合所述形式验证规范则形式验证通过，若不符合所述形式验证规范则定位所述形式验证不满足的语句位置以及具体的存证证智能合约位置。
  9. 根据权利要求8所述的形式验证方法，其特征在于，步骤(1)所述存证智能合约满足以下条件：
    (a)存证人、取证人、管理员的数据结构：利用映射类型的持久化变量来记录存证、取证人的身份信息，利用数组类型的持久化变量来记录管理员的身份信息；
    (b)存储存证信息的数据结构：利用多组映射类型的持久化变量来记录符合多种存证模式下的存证信息；
    (c)权限控制：利用修饰器对涉及所述存证、取证、存取证权限授予的方法进行权限控制。
  10. 根据权利要求8所述的形式验证方法，其特征在于，步骤(2)所述合约形式规范的添加包括：
    (a)合约方法添加异常捕捉规范，包括：存证场景下规范要求发生异常的充分必要条件是存证人没有存证资格且存证数据无效；取证场景下规范要求发生异常的充分必要条件是取 证人没有取证资格且取证令牌不存在；在发生异常的情况下，所有所述持久化变量不能被改变；
    (b)合约方法传入、传出参数的形式校验，规范要求对函数传入的参数进行格式校验，对函数传出的参数进行期望校验；
    (c)合约方法对持久化数据状态转移的规范说明，规范要求在各种类型的存证方法中，明确存证的映射类型持久化变量得到存证数据的追加；在取证方法中，明确所有的持久化变量不被改变；在存取证权限授予方法中，明确存取证人信息表数据的改变。
  11. 根据权利要求8所述形式验证方法，其特征在于，步骤(3)所述合约模型验证是利用定理证明器对编写所述形式规范的智能合约进行定理证明，并给出形式验证的结果。
PCT/CN2020/110512 2019-08-21 2020-08-21 存证智能合约的形式验证方法、系统、计算机设备和可读存储介质 Ceased WO2021032192A1 (zh)

Priority Applications (3)

Application Number Priority Date Filing Date Title
JP2022510096A JP7309306B2 (ja) 2019-08-21 2020-08-21 証明書保存スマートコントラクトの形式検証方法、システム、コンピュータ機器及び可読記憶媒体
US17/636,139 US12028331B2 (en) 2019-08-21 2020-08-21 Formal verification method for certificate storage smart contract, computer device, and non-transitory computer-readable storage medium
EP20853855.3A EP4020294A4 (en) 2019-08-21 2020-08-21 FORMAT VERIFICATION METHOD AND SYSTEM FOR CERTIFICATE STORING INTELLIGENT CONTACT, COMPUTER EQUIPMENT AND READABLE STORAGE MEDIUM

Applications Claiming Priority (2)

Application Number Priority Date Filing Date Title
CN201910772491.4 2019-08-21
CN201910772491.4A CN110555320B (zh) 2019-08-21 2019-08-21 一种基于区块链存证智能合约的形式验证方法

Publications (1)

Publication Number Publication Date
WO2021032192A1 true WO2021032192A1 (zh) 2021-02-25

Family

ID=68737879

Family Applications (1)

Application Number Title Priority Date Filing Date
PCT/CN2020/110512 Ceased WO2021032192A1 (zh) 2019-08-21 2020-08-21 存证智能合约的形式验证方法、系统、计算机设备和可读存储介质

Country Status (5)

Country Link
US (1) US12028331B2 (zh)
EP (1) EP4020294A4 (zh)
JP (1) JP7309306B2 (zh)
CN (1) CN110555320B (zh)
WO (1) WO2021032192A1 (zh)

Cited By (1)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US12256017B2 (en) 2022-11-18 2025-03-18 T-Mobile Usa, Inc. Techniques for correcting anomalous activity caused by smart contracts

Families Citing this family (6)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN110555320B (zh) * 2019-08-21 2021-03-23 杭州趣链科技有限公司 一种基于区块链存证智能合约的形式验证方法
CN110688428B (zh) * 2019-09-24 2021-01-26 北京海益同展信息科技有限公司 用于发布智能合约的方法和装置
CN111179056A (zh) * 2019-12-20 2020-05-19 杭州趣链科技有限公司 一种众筹智能合约的形式验证方法
CN112035897A (zh) * 2020-11-06 2020-12-04 腾讯科技（深圳）有限公司 区块链存证方法和相关装置
CN117155536B (zh) * 2023-09-01 2024-08-20 佛山市康颐福城市服务科技有限公司 智能合约的交易管理方法、装置、设备和可读存储介质
CN117311726B (zh) * 2023-10-26 2024-04-09 中央财经大学 智能法律合约生成方法、装置、电子设备及存储介质

Citations (5)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN107783758A (zh) * 2016-08-25 2018-03-09 北京航空航天大学 一种智能合约工程方法
CN108776936A (zh) * 2018-06-05 2018-11-09 中国平安人寿保险股份有限公司 保险理赔方法、装置、计算机设备和存储介质
CN109375899A (zh) * 2018-09-25 2019-02-22 杭州趣链科技有限公司 一种形式验证Solidity智能合约的方法
WO2019108676A1 (en) * 2017-11-28 2019-06-06 Yale University Systems and methods of formal verification
CN110555320A (zh) * 2019-08-21 2019-12-10 杭州趣链科技有限公司 一种基于区块链存证智能合约的形式验证方法

Family Cites Families (6)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US9734351B2 (en) * 2004-09-24 2017-08-15 Form I-9 Compliance, Llc Electronic signature for and electronic system and method for employment eligibility verification
SG11202009594QA (en) * 2018-03-29 2020-10-29 Dlt Global Inc Updateable smart contracts
CN108985073B (zh) * 2018-07-18 2020-05-22 成都链安科技有限公司 一种高度自动化的智能合约形式化验证系统及方法
US10896195B2 (en) * 2018-07-29 2021-01-19 International Business Machines Corporation Automatic generation of smart contracts
US20200201838A1 (en) * 2018-12-20 2020-06-25 Sri International Middleware to automatically verify smart contracts on blockchains
CN110147942A (zh) 2019-04-29 2019-08-20 阿里巴巴集团控股有限公司 一种基于区块链的业务配置方法、装置以及电子设备

Patent Citations (5)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN107783758A (zh) * 2016-08-25 2018-03-09 北京航空航天大学 一种智能合约工程方法
WO2019108676A1 (en) * 2017-11-28 2019-06-06 Yale University Systems and methods of formal verification
CN108776936A (zh) * 2018-06-05 2018-11-09 中国平安人寿保险股份有限公司 保险理赔方法、装置、计算机设备和存储介质
CN109375899A (zh) * 2018-09-25 2019-02-22 杭州趣链科技有限公司 一种形式验证Solidity智能合约的方法
CN110555320A (zh) * 2019-08-21 2019-12-10 杭州趣链科技有限公司 一种基于区块链存证智能合约的形式验证方法

Non-Patent Citations (1)

* Cited by examiner, † Cited by third party
Title
See also references of EP4020294A4 *

Cited By (1)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
US12256017B2 (en) 2022-11-18 2025-03-18 T-Mobile Usa, Inc. Techniques for correcting anomalous activity caused by smart contracts

Also Published As

Publication number Publication date
JP2022545403A (ja) 2022-10-27
EP4020294A4 (en) 2023-09-27
JP7309306B2 (ja) 2023-07-18
EP4020294A1 (en) 2022-06-29
CN110555320A (zh) 2019-12-10
US12028331B2 (en) 2024-07-02
CN110555320B (zh) 2021-03-23
US20220294776A1 (en) 2022-09-15

Similar Documents

Publication Publication Date Title
WO2021032192A1 (zh) 存证智能合约的形式验证方法、系统、计算机设备和可读存储介质
CN114461610B (zh) 一种数据权限控制方法、装置、电子设备及存储介质
US11425115B2 (en) Identifying revoked credentials
CN110957025A (zh) 一种医疗卫生信息安全管理系统
US8650634B2 (en) Enabling access to a subset of data
US12184787B2 (en) Hardware security module that enforces signature requirements
CN110019422A (zh) 基于区块链处理职业信息的方法、装置及存储介质
CN117971980A (zh) 基于区块链的数据库访问权限管理系统及方法
US20150242570A1 (en) Electronic health record system with customizable compliance policies
CN101398873B (zh) 加载第三方软件的方法及系统
US20080072328A1 (en) Security vulnerability determination in a computer system
WO2022109108A1 (en) Automated control compliance evidence manager using a secure distributed ledger
Sohr et al. Formal specification of role-based security policies for clinical information systems
US20220405195A1 (en) Secured code assignment and review engine
Nagarajan et al. Trust management for trusted computing platforms in web services
Ungan et al. Using FSM patterns to size security non-functional requirements with COSMIC
CN116257824A (zh) 一种越权校验方法、装置及电子设备
Kosiyatrakul et al. A modal logic for role-based access control
CN112084192A (zh) 一种基于区块链技术的电子证照应用方法
ES3002032T3 (en) Information system for the integration of digital certificates and method for operating said information system
Alghathbar Representing access control policies in use case.
CN116910821A (zh) 数据读写方法、装置、设备及存储介质
CN110737464A (zh) 一种代码静态分析方法和装置
Wilk Information security management model for integration platforms
Bhartiya et al. Hierarchy Similarity Analyser: An Approach to Securely Share Electronic Health Records

Legal Events

Date Code Title Description
121 Ep: the epo has been informed by wipo that ep was designated in this application

Ref document number: 20853855

Country of ref document: EP

Kind code of ref document: A1

ENP Entry into the national phase

Ref document number: 2022510096

Country of ref document: JP

Kind code of ref document: A

NENP Non-entry into the national phase

Ref country code: DE

ENP Entry into the national phase

Ref document number: 2020853855

Country of ref document: EP

Effective date: 20220321