KR102269174B1 - Appratus and method for verification of smart contracts - Google Patents

Abstract

A smart contract verification apparatus and method, wherein the smart contract verification apparatus obtains an invariant processing unit that generates an invariant candidate group including at least one invariant candidate and at least one verification target of the contract, and uses the invariant candidate and a verification unit generating verification conditions for each of the at least one verification target, wherein the verification unit detects a return target from among the at least one verification target and delivers it to the invariant processing unit, wherein the return target is valid A verification target corresponding to a verification condition that has not been verified may be included.

Description

Smart contract verification apparatus and method

The present invention relates to a smart contract verification apparatus and method.

A smart contract (which can be referred to as a smart contract, etc.) means a digitized contract negotiated between a plurality of contractors or a program code (which can be referred to as a program or software, etc.) that automatically implements the contract contents in such a contract. Recently, with the development of blockchain-based technologies such as virtual currency and security programs, interest in smart contracts is rapidly increasing.

It is important to verify the safety of smart contracts relative to other programs. Because, firstly, smart contracts can directly change an individual's property situation according to the processing result, while anyone can view the source code, so if someone discovers and exploits a defect inside the smart contract, it causes huge property damage because you can For example, such as the SMT (SmartMesh) hacking incident, using an integer overflow vulnerability in the smart contract code to create infinite tokens and inflict financial damage on multiple people may occur. . Second, unlike other programs, smart contracts cannot be modified (immutability) once deployed through blockchain. For these reasons, before the smart contract program is distributed through blockchain, etc., whether there is a problem in the program code should be more strictly checked and verified.

For such verification, code auditing is sometimes requested by security experts before the distribution of the smart contract program, but safety verification by humans has clear limitations. Therefore, tools for automating such verification have been developed and guided, but since these tools only perform verification on a part of the program, there is a limit in which all vulnerabilities in the smart contract program cannot be detected (unsoundness, unsoundness). ). On the other hand, among these tools, there is also a tool for performing verification on all programs, but since they generate too many false positives, there is a disadvantage in that the analysis result for the smart contract is inaccurate.

US Patent Publication US 2018/0183600 A1 (published on June 28, 2018) US registered patent 7,146,352 B2 (registered on Dec. 5, 2006) Japanese Patent Laid-Open No. 2001-142937 (published on May 25, 2001)

An object of the present invention is to provide a smart contract verification apparatus and method capable of accurately verifying the vulnerabilities of a smart contract without omission.

Another task to be solved is to provide a smart contract verification device and method that can accurately verify vulnerabilities by automatically inferring the transaction invariants hidden within the smart contract.

A smart contract verification apparatus and method are provided in order to solve the above problems.

The smart contract verification apparatus obtains an invariant processing unit that generates an invariant candidate group including at least one invariant candidate and at least one verification target of the contract, and uses the invariant candidate to each of the at least one verification target. a verification unit generating a verification condition for the verification unit, wherein the verification unit detects a return target from among the at least one verification target and transmits it to the invariant processing unit, wherein the return target includes a verification target corresponding to an invalid verification condition can do.

The smart contract verification method includes the steps of generating an invariant candidate group including at least one invariant candidate, obtaining at least one verification target of the contract, and using the invariant candidate for each of the at least one verification target The method may include generating a verification condition and detecting a return target from among the at least one verification target, wherein the return target includes a verification target corresponding to an invalid verification condition.

According to the smart contract verification apparatus and method described above, it is possible to obtain the effect of accurately verifying the vulnerabilities of the smart contract without omission.

In addition, it is possible to accurately verify vulnerabilities by automatically inferring the transaction invariants hidden within the smart contract, thereby achieving the effect of overcoming the limitations of the conventional smart contract analysis or verification technology.

In addition, since the safety of the smart contract to be distributed can be further improved, it is also possible to obtain the effect of increasing the safety of various ecosystems in which the smart contract will be used, such as a blockchain ecosystem.

In order to more fully understand the drawings recited in the Detailed Description of the Invention, a detailed description of each drawing is provided.
1 is a block diagram of an embodiment of a smart contract verification apparatus.
2 is a diagram for explaining an example of a contract.
3 is an example of a program code for explaining an invariant expression.
4 is a control block diagram of an embodiment of a smart contract verification apparatus.
5 is a first diagram for explaining an example of the operation of the verification unit.
6 is a second diagram for explaining an example of the operation of the verification unit.
7 is a block diagram of another embodiment of the verification unit.
8 is a diagram illustrating an example in which the operation of the smart contract verification apparatus is expressed in program code.
9 is a first chart showing the results of comparing the performance of the smart contract verification device with other conventional devices.
10 is a second chart showing the results of comparing the performance of the smart contract verification device with other conventional devices.
11 is a flowchart of a first embodiment of a smart contract verification method.
12 is a flowchart of a second embodiment of a smart contract verification method.
13 is a flowchart of a third embodiment of a smart contract verification method.

In the following specification, the same reference numerals refer to the same elements unless otherwise specified. The term added with 'unit' used below may be implemented in software or hardware, and depending on the embodiment, one 'unit' may be implemented as one physical or logical part, or a plurality of 'units' may be implemented as one It may be implemented as a physical or logical part, or one 'unit' may be implemented with a plurality of physical or logical parts.

Throughout the specification, when it is said that a part is connected to another part, this may mean a physical connection or an electrically connected part depending on the part and the other part. In addition, when it is said that a part includes another part, it does not exclude another part other than the other part unless otherwise stated, and it means that another part may be further included according to the designer's choice. do.

Terms such as 'first' or 'second' are used to distinguish one part from another, and unless otherwise specified, they do not mean sequential expressions. Also, the singular expression may include the plural expression unless the context clearly dictates otherwise.

Hereinafter, various embodiments of the smart contract verification apparatus will be described with reference to FIGS. 1 to 8 .

1 is a block diagram of an embodiment of a smart contract verification apparatus.

As shown in FIG. 1 , the smart contract verification apparatus 100 may include a verification unit 110 , a Validator, and an invariant processing unit 170 , and may further include a validity determination unit 180 according to an embodiment. can In addition, it is also possible to further include the input unit 101 and the output unit 102 if necessary. At least two of the verification unit 110 , the invariant processing unit 170 , the validity determination unit 180 , the input unit 101 , and the output unit 102 are electrically connected to each other to transmit and receive information (data) . In this case, they may transmit/receive data based on cables, circuits and/or wired/wireless communication networks.

The smart contract verification apparatus 100 may include at least one device capable of various arithmetic processing and signal generation, and the at least one device may be implemented using a processor, or implemented using a computing device in which the processor is installed. could be Here, the processor is, for example, a central processing unit (CPU, Central Processing Unit), a micro controller unit (MCU), a microcomputer (Micom, Micro Processor), an application processor (AP, Application Processor), electronic control It may include an Electronic Controlling Unit (ECU), a graphic processing unit (GPU), and/or a processing unit capable of processing various calculations and generating control signals. These processing devices may be implemented using, for example, one or more semiconductor chips and related components. Computing devices include, for example, desktop computers, laptop computers, server computers, smart phones, tablet PCs, smart watches, Head Mounted Display (HMD) devices, portable game consoles, robots, home appliances, mechanical devices, and/or Alternatively, it may include at least one electronic device capable of performing other information processing functions.

The verification unit 110 is provided to obtain a contract (contract, which can be expressed as a contract, etc.) from the input unit 101 or through a separate storage medium (not shown), and to verify the safety of the obtained contract. A contract may contain program code that can automatically execute predefined contents according to specific conditions or situations.

According to an embodiment, the verification unit 110 may receive a Group of invariant candidates from the invariant processing unit 170, and verify/confirm the safety of the contract using the received invariant candidate group. have. Here, the invariant candidate group includes at least one set including at least one invariant candidate(s). For example, the verification unit 110 includes the inductiveness of at least one invariant candidate of the received invariant candidate group and all verification objects in the contract (eg, a query or query in the program code, etc.). The safety of the contract can be verified by examining the safety of the default path, etc.).

An invariant refers to a condition, property, property, or state that remains constant and does not change during any series of operations. An invariant expression can be expressed in the form of a function (expression or statement, etc.). The invariant may include, for example, at least one of a transaction invariant and a loop invariant. Transaction invariance refers to a condition, attribute, property, or state that does not change even in the course of transaction processing. Transaction invariants are always satisfied when the constructor function (constructor function) is terminated or before and after execution of an externally callable function (for example, a function other than a constructor whose function access modifier is public or external, etc.). The loop invariant expression refers to a state, property, or condition that does not change while any loop (which can be expressed as a loop, loop, etc.) is executed. The loop invariant is always satisfied before each loop execution (the loop entry point).

Invariants may be explicitly expressed in the program code and/or may not be explicitly expressed in the program code and thus have to be inferred or verified from the code. The invariant candidate means at least one invariant expression(s) that has been previously collected, defined, set or refined to estimate the invariant expression used in the contract. The invariant candidate may be generated so as to prove the safety of at least one verification target in the contract while being inductive.

The verification unit 110 may generate a verification condition ( 113a in FIG. 4 ) for verifying the safety of the contract. The verification condition 113a may be generated corresponding to each of at least one verification target of the contract (eg, a basic path (111a in FIG. 4 ), etc.). According to an embodiment, the verification conditions 113a may be generated for all verification objects 111a of the contract. The above-described invariant candidate group may be used to generate the verification condition 113a.

More specifically, the verification unit 110 configures the verification condition 113a related to the inductance of the invariant candidate generated by the invariant expression processing unit 170 and the safety of the query in a predetermined formula form, and the validity ( It may be designed to test whether or not Here, the predetermined formula may include, for example, a first-order logic (FOL) or first-order formula, but is not limited thereto.

The validity of the generated verification condition 113a may be directly determined by the verification unit 110 or may be determined by the validity determination unit 200 . In the latter case, the verification condition 113a is transmitted to the validity determination unit 200 , and the validity determination unit 200 determines whether the received verification condition 113a is valid or not, and then sends the determination result to the verification unit 110 . can transmit

If the verification unit 110 or the validity determination unit 200 determines that the verification condition 113a is valid (eg, when all queries are proven to be safe, etc.), the verification unit 110 determines that the contract can be considered safe. In this case, the verification unit 110 may determine that the contract is secure if there is no verification condition determined to have no validity or a verification target corresponding thereto (hereinafter referred to as a return target). The determination result may be transmitted to the output unit 102, and in response, the output unit 102 may report to the outside in a predefined way that the contract is secure.

Conversely, if the verification unit 110 or the validity determination unit 200 determines that the verification condition 113a is not valid (eg, when there is a return target such as when there is a query that fails the safety verification), the verification unit 110 may transmit a return target (ie, a verification condition determined to have no validity or a verification target corresponding thereto) to the invariant processing unit 170 .

The invariant processing unit 170 may generate an invariant candidate group, and more specifically, it generates an invariant candidate group that can prove the safety of as many queries as possible while inductively, and uses the generated invariant candidate group as the verification unit 110 . can transmit The invariant processing unit 170 may generate a transaction invariant, a loop invariant, or both.

According to an embodiment, the invariant processing unit 170 may include an initialization unit 171 and a refiner unit 173 as shown in FIG. 1 .

The initialization unit 171 generates the first invariant candidate group and transmits the generated first invariant candidate group to the verification unit 110 so that the verification unit 110 validates the contract using the first invariant candidate group. can do. The initialization unit 171 is operable according to a user's manipulation or a predefined setting. For example, the initialization unit 171 may be provided to generate the first invariant candidate group whenever a new contract is input. If necessary, the initializer 171 may select an invariant candidate having the smallest size from among at least one invariant candidate in the invariant candidate group, and then remove the selected invariant candidate from the invariant candidate group.

When the refining unit 173 receives a return target from the verification unit 110 , based on the return target, the invariant candidate group previously delivered to the verification unit 110 (eg, the first invariant candidate group or a new invariant type candidate group thereafter) A new invariant candidate group can be generated by refining and refining the generated invariant expression candidate group. According to an embodiment, the invariant processing unit 170 may not generate a new invariant candidate group any more when the safety is proven because all of the verification conditions 113a are valid and/or a predefined analysis time has elapsed. .

More details on the operations of the verification unit 110 and the invariant processing unit 170 will be described later.

The validity determination unit 200 receives the verification condition 113a generated by the verification unit 110 and determines whether the received verification condition 113a is valid/invalid, and then returns the determination result to the verification unit ( 110) can be sent. According to an embodiment, the feasibility determination unit 200 may be implemented using a predetermined analysis program or an apparatus for performing the same, wherein the predetermined analysis program is, for example, an SMT solver (Satisfiability Modulo Theories Solver). and the like. According to the designer's choice, the feasibility determination unit 200 may be provided in the smart contract verification device 100 as shown in FIG. 1, and/or physically separated from the smart contract verification device 200 and communicated via wired/wireless communication. It may be provided on one or more other computing devices communicatively connected to each other through a network. Here, the other computing device may include, for example, a desktop computer, a laptop computer, a server computer, and/or other various at least one electronic device.

According to an embodiment, the above-described verification unit 110, invariant processing unit 190, and validity determining unit 200 may be implemented using one processing unit (eg, central processing unit, etc.), or It may be implemented using two or more physically separate processing units. When these are implemented using two or more physically separate processing devices, the verification unit 110 , the invariant processing unit 190 , and the validity determining unit 200 may all be implemented using physically separate processing devices, respectively. Alternatively, only some of them may be implemented using other physically separate processing devices.

The input unit 101 may receive information necessary for the operation of the smart contract verification apparatus 100 from the outside and transmit it directly or indirectly to the verification unit 110 . For example, the input unit 101 may receive a smart contract and transmit it to the verification unit 110 so that the verification unit 110 performs a verification operation on the smart contract. In this case, the smart contract may be written in the Solidity language. The input unit 101 may include a data input/output terminal such as a universal serial bus (USB) terminal, a keyboard device, a mouse device, a trackball, a trackpad, an image pickup device, and/or various sensors according to a user's operation or automatically It may include at least one device capable of receiving data.

The output unit 102 is provided to output the final determination result of the verification unit 110 to the outside. For example, the output unit 102 may output a verification result for the safety or invariability of the invariant expression for each of at least one verification target (ie, the default path) of the contract. According to the designer's selection, the output unit 102 may output the verification result in the form of a predefined electronic document. The output unit 102 may include a data input/output terminal, a monitor device, a printer device, a sound output device (which may include a speaker, etc.) and/or at least one device capable of outputting other information according to an embodiment. can

Although omitted from the drawing, the smart contract verification apparatus 100 may further include a storage medium for temporarily or non-temporarily storing at least one data required for the operation of the smart contract verification apparatus 100 or obtained as a result of the operation. have. For example, the storage medium includes a contract, at least one invariant candidate, a basic path 111a or a verification condition 113a generated by the verification unit 110 , and the determination of the verification unit 110 or the validity determination unit 180 . As a result, the invariant candidate group generated by the invariant processing unit 170 and/or the application (which may be referred to as a program or an app, etc.) related to the operation/function of the smart contract verification apparatus 100 may be stored. Here, the application related to the operation/function of the smart contract verification apparatus 100 may be directly input to the storage medium by the designer, etc., or may be transmitted or updated through the input unit 101 or the communication unit (not shown). . In the case of using the communication unit, the application related to the operation/function of the smart contract verification apparatus 100 may be delivered or updated through an electronic software distribution network. Such a storage medium may include a main memory device such as ROM and/or RAM, and/or a flash memory device, a solid state drive (SSD) and/or a hard disk drive ( It may include an auxiliary storage device such as HDD or Hard Disc Drive).

Hereinafter, contracts and invariants used or processed by the verification unit 110 and the invariant processing unit 170 will be described first.

2 is a diagram for explaining an example of a contract. 2 is a representation of an example of a contract based on the Solidity language. In FIG. 2, c denotes a contract, C denotes a contract set, G ^* denotes a set of global state variable declarations, and F ^* denotes a set of at least one function definition (f). x stands for function name and S stands for statement. a is a base statement, A means a set of base statements containing at least one base statement (a), E means an arithmetic expression (e.g. a+b), and B means a boolean expression (e.g. For example, a ≥ b).

As shown in FIG. 2 , the contract (c) may include at least one global state variable declaration (G ^* ) and at least one set of function definitions (F ^* ). Each function definition (f) in the set (F ^* ) can be defined by a function name (x) and a statement (S). Here, the statement S may include at least one of a set of basic statements (A), a conditional statement (if B S1 S2), a while-loop, and a sequence (S1; S2). Each while-loop may include a loop label (l) indicating a loop header. Each basic statement (a) of the basic statement set (A) is, for example, a variable assignment statement ( x := E ), an array element assignment statement ( x [y] := E ), an assumption statement ( assume (B) )) and/or assert (B)). Here, the variable assignment statement is prepared to assign a value to a variable used in the code. The array element assignment statement models value assignment to elements of an array variable used in a typical programming language, and is provided to model assignment of values to elements of a mapping type variable in, for example, a solidity language. Assume statements enable it to be determined whether a condition is satisfied, and whether or not to execute sequential statements can be determined depending on whether the condition is established. That is, if the condition is met, sequential statements are continuously executed. If the condition is not met, the execution of the current transaction (which can be expressed as a transaction, work or processing, etc.) is canceled and the program returns to the state before the execution of the assumption statement. do. The assertion can express the object to be verified (hereinafter referred to as the verification target, for example, safety against integer overflow vulnerability, safety against integer underflow vulnerability, safety against vulnerability when the divisor is 0, etc.) have. The assertion may include at least one query (query, an expression expressed in the assertion) for expressing the verification target. The query may be automatically inserted into the program, or may be manually inserted according to a programmer's operation. For example, a developer can insert a query into a program by using the assert statement, and more specifically, for all addition operations that exist in the smart contract, for example, to verify the integer overflow vulnerability for the addition operation. Equation 1 below may be inserted.

The verification unit 110 verifies the safety of the contract using such characteristics of the contract and at least one invariant expression transmitted from the invariant processing unit 170 .

3 is an example of a program code for explaining an invariant expression, and represents an example of a contract.

In the case of the contract shown in Fig. 3, when the constructor function is executed (refer to line 5), the total supply is set to 10,000, and the sender's account balance is also designed to be initialized to 10,000. In this case, the balance of the uninitialized account becomes 0, and the total of all accounts becomes equal to the value of 10,000.

Referring to lines 10 to 14 of the contract, a function transfer is the amount to be transferred from the sender’s account balance only when the balance of the sender’s account is equal to or greater than the value to be transferred (line 11). It is designed to deduct (line 12) and add the amount to be remitted to the account balance of the recipient (to) (line 13). In addition, referring to lines 16 to 20, the collection transaction (trasnferFrom) is performed only when the sender's account balance (balance[from]) is the same or greater than the amount to be remitted (value) (line 17), the sender's account balance It is written that the amount to be remitted is subtracted from (line 18) and the amount to be remitted is added to the account balance of the recipient (to) (line 19).

In the code of the contract designed in this way, it can be seen that the operations of lines 12 and 19 are safe because there is a guard statement. However, for the operations of lines 13 and 18, there is no direct protection statement in each function, so it is difficult to intuitively determine whether they are safe or not. However, despite the absence of an explicit guard, the operations in lines 13 and 18 are safe. This is because the characteristic that integer overflow does not occur during the calculation of Equation 2 and Equation 2 below is constantly maintained at the start and end of a transaction. That is, the transaction invariant expression is established.

Specifically, as described in Equation 2, the total account total is maintained at 10,000 the same before and after the transaction. In addition, since remittance is allowed only when the balance of the sender's account is sufficient (refer to lines 11 and 17), an abnormal situation in which an integer overflow occurs does not occur. In other words, since the maximum value of each account is 10,000, when combined with the conditional statements in lines 11 and 17, the arithmetic operations in lines 12, 13, 18, and 19 ^{are all 256-} bit operations (maximum value 2 256 -1). safe. Therefore, the above-described contract can be determined to be safe.

It can be confirmed inductively that such a transaction invariant expression holds.

Hereinafter, the operations of the verification unit 110 and the invariant processing unit 170 will be described in more detail based on the contents of the above-described contract and invariant expression.

4 is a control block diagram of an embodiment of a smart contract verification apparatus.

As shown in FIG. 4 , the verification unit 110 receives at least one contract from the input unit 101 or the storage medium, and simultaneously or sequentially the initialization unit 171 and the refiner unit ( 173) may receive an invariant candidate group from at least one. Specifically, for example, the verification unit 110 may receive and obtain three elements (c, ψ, μ) as input values. Here, c denotes a contract, ψ denotes an invariant expression, and μ(μ: label → FOL) denotes a loop invariant mapping for each loop label. The verification unit 110 may verify the safety of the contract based on the received at least one contract and the invariant candidate group. According to an embodiment, the verification unit 110 determines the inductiveness of the invariant candidates (ψ, μ) received from the invariant processing unit 170 and the safety of at least one statement (query) included in the contract (c). By confirming, the safety of the contract can be verified.

According to an embodiment, the verification unit 110 may include a path set generation unit 111 , a condition generation unit 113 , and a result processing unit 119 .

The path set generator 111 may acquire at least one basic path 111a (basic path)(s) by dividing the program. The default path 111a includes an execution path of at least one statement(s). According to one embodiment, the default path 111a may include a path comprising a function entry, a function exit, and a sequence of at least one statement(s) between the function entry and exit, and , and/or a path including a loop entry and a sequence of at least one statement present within the loop. More specifically, for example, the basic path 111a may be defined as in Equation 3 below.

Here, l ₁ is the starting point (ie, function entrance or loop entrance) of _{the basic path 111a, l 2} is the ending point (ie, function exit or loop entrance) of the basic path 111a, a1; … ;a2 means a sequence of basic statements. φ ₁ is the invariant at the starting point l ₁ of the basic path 111a _{, and φ 2} is the invariant at the _{ending point l 2 of the basic path 111a.} In this case, if the starting point l ₁ is the entrance to the function, then φ ₁ is transaction invariant (ie φ ₁ =ψ), and if the starting point l ₁ is the entrance to the loop, then φ ₁ is the starting point l ₁ ) becomes a loop invariant (ie, φ ₁ =μ(l ₁ )). On the other hand, if the function is a constructor, it must assume an arbitrary state, so it can be given _{as φ 1} = true. Similarly, if the exit point l ₂ is the function exit, then φ ₂ is transaction invariant (ie φ ₂ =ψ), and if the loop entry, φ ₂ is loop invariant (ie φ ₂ =μ(l ₂ ) ).

The basic path 111a generated by the path set generating unit 111 may be transmitted to the condition generating unit 113 . The condition generator 113 may generate a verification condition 113a for each basic path 111a. More specifically, for example, the condition generator 113 generates the verification condition 113a by generating at least one expression for whether the invariant candidate is inductive or not and whether the query is safe for each basic path 111a. can In this case, the condition generator 113 may generate the verification condition 113a using the initial invariant candidate group transmitted from the initializer 171 or the new invariant candidate group transmitted from the refiner 173 .

According to an embodiment, the condition generator 113 may generate the verification condition 113a by using a statement (function) expressed by Equation 4 below.

는 하기의 수학식 5와 같이 정의될 수 있다.Here, ∧ means the logical operator AND. Also,

may be defined as in Equation 5 below.

는 불변식 후보의 귀납성에 관한 조건을 표현한 식이고,

는 기본 경로에 존재하는 쿼리들의 안전성에 관한 조건을 나타낸 식이다. 또한, 수학식 5에서 sp는 후조건 변환기(strongest post-condition predicate transformer)를 의미한다. 후조건 변환기(sp)는 각 기본 경로에서 존재하는 기본 명령문(쿼리)들의 영향을 나타내도록 정의된 것일 수 있으며, 예를 들어, 하기의 수학식 6과 같이 정의될 수 있다.In Equation 4,

is an expression expressing the condition for the inducibility of the invariant candidate,

is an expression representing the condition regarding the safety of queries existing in the default path. Also, in Equation 5, sp denotes a strong post-condition predicate transformer. The post-condition converter sp may be defined to indicate the effect of basic statements (queries) existing in each basic path, and may be defined, for example, as in Equation 6 below.

및 true)을 입력하여 나온 결과를 기반으로 귀납성 여부 및 안전성을 판단할 수 있도록 설계된 것일 수 있다.Here, FOL means a first-order logical expression. In other words, the verification condition generating function (GenVC( )) of Equation 4 is a function (statement) obtained by synthesizing each post-condition converter (sp) with a predefined value (

and true) may be designed to determine whether or not it is inductive and safety based on the result of inputting it.

5 shows an example of a first road and post-condition converter for explaining an example of the operation of the verification unit.

은

에 존재하는 변수 x가 새로운 변수 x'으로 교체된 것을 의미한다.According to an embodiment, the post-condition converter sp may be defined, as shown in FIG. 5 . 5,

silver

It means that the variable x existing in ' is replaced with the new variable x'.

) 및 현재까지 누적된 쿼리 안전성에 대한 식(

)이 주어졌을 때, a에 의한 영향을

에 추가로 반영하도록 설계된 것일 수 있다. 만약 기본 명령문(a)이 단언문(assert())일 경우 쿼리 안전성에 대한 식을 현재까지 누적된 쿼리 안전성에 대한 식(

)에 추가로 부가하여 누적하는 작업을 수행하도록 설계될 수 있다. The post-condition converter sp may be defined for each basic statement (a), and may be defined differently depending on the type of the basic statement (a). For example, the basic statement (a) consists of a variable assignment statement ( x := E ), an array element assignment statement ( x [y] := E ), an assert statement ( assume (B)), and an assert statement ( assert (B)). ) may be at least one, and a different post-condition converter sp may be defined for each statement (a) as shown in FIG. 5 . The postcondition converter (sp) consists of a basic statement (a), a precondition (

) and the expression for query safety accumulated so far (

), given the effect of a

It may be designed to reflect additionally. If the basic statement (a) is an assertion (assert()), the expression for query safety (

) can be designed to perform an accumulating operation in addition to

The condition generator 113 generates a verification condition 113a for at least one basic path 111a in this way, respectively. In this case, the condition generation unit 113 may generate the verification condition 113a only for some basic paths 111a among the basic paths 111a generated by the path set generation unit 111 , or generate a path set. The verification condition 113a may be generated for all basic paths generated by the unit 111 . According to an embodiment, the verification condition 113a generated by the condition generating unit 113 may be transmitted to the validity determining unit 180 . The validity determining unit 180 may determine the validity of the received verification condition 113a.

The result processing unit 119 may check whether the safety of the contract is verified, and may perform a predetermined operation according to the verification result. In this case, the result processing unit 119 receives the determination result on the validity of the verification condition 113a from the validity determination unit 180, and the output unit 102 and/or the refiner 173 based on the received determination result. ) to pass the required data.

For example, when the safety of the contract is not verified (for example, when the invariant candidate is not inductive or there is a query that fails to prove safety), the result processing unit 119 responds to an invalid verification condition. The verification target (ie, return target) may be transmitted to the refiner 173 of the invariant processing unit 170 . Conversely, when the safety of the contract is proven (eg, when the invariant candidate is inductive and there is no query that fails the safety verification), the result processing unit 119 may transmit the verification result to the output unit 102 .

According to the embodiment, the result processing unit 119 determines that the current invariant candidates are inductive even if the safety of each reference path (or the safety of the contract) is not verified by the currently used invariant candidates. By passing the same information to the invariant processing unit 170 , the invariant processing unit 170 may more specifically refine the invariant candidates.

6 is a second diagram for explaining an example of the operation of the verification unit. In FIG. 6, p denotes a basic path 111a, GenVC(p).1 denotes a verification condition for induction, and GenVC(p).2 denotes a verification condition for safety. F∈GenVC(p).2 indicates each clause of GenVC(p).2, and means the safety verification condition for one query (F). In FIG. 6, ∃F∈GenVC(p).2 is invalid means all queries (F) for which the safety verification condition is not valid.

According to an embodiment, the result processing unit 119 may return a data pair of ( inductive, U ) as shown in FIG. 6 to the refiner 117 . In ( inductive, U ), inductive is a boolean variable indicating whether a given invariant candidate is inductive, U is a set of return objects, and at least one verification condition generated by the condition generator 113 . It is a set of verification targets (eg, the basic path 111a for which validity is not confirmed) corresponding to verification conditions in which validity is not confirmed or has no validity among (113a). Here, the validity determination may be performed by the validity determination unit 180 .

As shown in the second line of FIG. 6, if the inductive verification fails for all basic paths (p, 111a) (∃p∈GenVC(p).1 is invalid), as described in the third line , ( inductive, U ) may be assigned and written with a false value and a default path (p, 111a, where p∈P|GenVC(p).1 is invalid), respectively. Accordingly, the basic paths 111a that have failed the inductive verification can be collected as at least one set U. As contrast, according to the fourth line, if all default route if a successful induction validation with respect to (p, 111a), variable inductive has become a true value assignment, set U in the base path, the safety verification fails (p, 111a, Here, p∈P|∃F∈GenVC(p).2 is invalid) is included. Accordingly, the basic paths 111a that have succeeded in the inductive verification but failed in the safety verification can be collected as at least one set U.

7 is a block diagram of another embodiment of the verification unit.

As shown in FIG. 7 , the verification unit 110 includes a condition simplification unit 115 and a preceding validity determination unit 116 in addition to the path set generation unit 111 , the condition generation unit 113 , and the result processing unit 119 . It may further include at least one of Since the path set generating unit 111 , the condition generating unit 113 , and the result processing unit 119 have been described above, detailed descriptions thereof will be omitted.

The condition simplification unit 115 may relatively simply modify/transform the verification condition 113a generated by the condition generation unit 113 . In this case, the condition simplification unit 115 may simplify the verification condition 113a based on a predefined simplification rule. Here, the predefined simplification rule may be defined based on various formulas, laws, and/or axioms previously defined mathematically or logically. For example, the condition simplification unit 113a may simplify the following Equation 7 as Equation 8.

)을 제거함으로써 선행 타당성 판단부(116)의 판단 결과에 오류가 발생하는 것을 방지할 수도 있게 된다.As described above, according to the simplification of the verification condition 113a, the analysis of the verification condition 113a can be processed more quickly and smoothly. In addition, such a simplification of the verification condition 113a is a trivial expression in the verification condition 113a or a simple expression (eg, Equation 13).

), it is also possible to prevent an error from occurring in the determination result of the preceding validity determination unit 116 .

According to an embodiment, the verification condition simplified by the condition simplification unit 115 may be transmitted to the validity determination unit 180 and/or may be transmitted to the prior validity determination unit 116 . The validity determining unit 180 may receive the simplified verification condition and determine whether the simplified verification condition is valid or not valid. When a complex operation exists in the smart contract, the validity/non-validity determination time of the validity determination unit 180 of the verification condition 113a may be relatively increased. However, when the verification condition 113a is simplified by the condition simplification unit 115 as described above, the determination time of the validity determination unit 180 may be relatively shortened, and accordingly, the verification time for the overall smart contract It can also be shortened. As described above, the determination result of the validity determination unit 180 may be transmitted to the result processing unit 119 of the verification unit 110 .

Prior to the validity determination unit 116, before the verification condition 113a is transmitted to the validity determination unit 180 or before the validity determination unit 180 determines whether the validity of the verification condition 113a exists, It may be determined whether the verification condition 113a is valid. According to an embodiment, the prior validity determining unit 116 may determine the validity of the verification condition 113a generated by the condition generating unit 113 in advance and/or simplified verification by the condition simplification unit 115 . The validity of the condition may be judged in advance.

According to an embodiment, the prior validity determining unit 116 may determine the validity of the verification condition 113a and/or the simplified verification condition based on a predefined template. The predefined template may be defined based on a verification condition commonly created/detected in the analysis process of a smart contract or a pattern of such verification condition. For example, if a verification condition of a specific pattern is input, it is determined to be valid. It may include the content that it is determined that it is not valid when the verification condition of a specific pattern is input and/or that the verification condition of a specific pattern is input. More specifically, for example, when the verification condition of the form shown in Equation 9 below is confirmed, the prior validity determination unit 116 may determine that it is valid without the determination of the validity determination unit 180 .

Here, F is an arbitrary formula, and n ₁ and n ₂ are integers having a relationship of n ₁ len _{2 .}

Accordingly, the judgment of the safety of the smart contract can be made more quickly.

Also, the prior validity determining unit 116 may determine the validity of the verification condition 113a and/or the simplified verification condition based on the type of verification condition. Specifically, the verification condition 113a generated by the condition generator 113 may have the form of Equation 10 below.

Therefore, when the verification condition 113a is in the form of Equation 11 below, the prior validity determination unit 116 quickly performs the verification condition (113a) without transmitting the verification condition 113a to the validity determination unit 180. 113a) may be judged to be inappropriate.

Here, FV(x) means a set of free variables for x. That is, the prior validity determining unit 116 may determine the verification condition 113a based on the inclusion relationship between the set of free variables for the condition and the set of free variables for the result in the conditional sentence. In this case, in order for Equation 10 to be true, the prerequisite p must be a more specific concept (sub-concept). More specifically, for example, it may be quickly determined that the verification condition as in Equation 12 below is not valid.

If each operation is performed in 256bit without a sign bit (unsigned-256bit, uint256), Equation 12 can be expressed as Equation 13 below, so it can be seen that Equation 12 is not valid. In addition, if 2 ²⁵⁵ is actually substituted for a and 0 is substituted for b, Equation 12 is obviously not valid.

As such, the prior validity determination unit 116 enables the verification unit 110 to more quickly determine whether the contract is valid without the help of the validity determination unit 180 according to the form of the verification condition 113a.

According to an embodiment, the prior validity determining unit 116 may determine the validity based on the simplified verification condition. As described above, even if the prior validity determining unit 116 determines that the verification condition 113a is not valid, there may be a valid case in reality. For example, in the case of the verification condition 113a expressed by Equation 14 below, when validity is determined using the set of free variables as described above, the result is expressed as Equation 15 below, so the preceding validity The determination unit 116 determines that Equation 14 is not valid.

Such an error may occur when a trivial expression or a simple mathematical expression is included. This can be solved by performing the process of simplifying the verification condition 113a of the condition simplification unit 115 in advance as described above. That is, in the simplification process, the above-mentioned trivial expressions or simple formulas may be removed. For example, if Equation 14 is simplified as Equation 16 below, according to Equation 17, the preceding validity determining unit 116 can make a more accurate determination.

However, since such trivial expressions or simple mathematical expressions are unlikely to appear in actual smart contracts, the condition simplification 115 process is not necessarily preceded. In addition, even if the condition simplification 115 is not performed, a case of missing a vulnerability does not occur. As described above, even if it is determined that the valid verification condition (eg, Equation 15) is not valid, it is not determined that the invalid verification condition is valid.

According to an embodiment, if the validity of the verification condition 113a or the simplified verification condition is not determined by the preceding validity determination unit 116 , the verification condition 113a or the simplified verification condition is transmitted to the validity determination unit 180 . Conversely, when the validity of the verification condition 113a or the simplified verification condition is determined by the preceding validity determination unit 116 , the verification condition 113a or the simplified verification condition is not transmitted to the validity determination unit 180 . may be designed. In addition, according to another embodiment, even when the validity of the verification condition 113a or the simplified verification condition is determined by the preceding validity determination unit 116 for verification accuracy, the verification condition 113a or the simplified verification condition is It is also possible to transmit the information to the validity determination unit 180 . In addition, according to another embodiment, only when the preceding validity determination unit 116 determines that the verification condition 113a or the simplified verification condition is valid, or the preceding validity determination unit 116 determines the verification condition 113a Alternatively, only when it is determined that the simplified verification condition is not valid, the verification unit 110 may transmit the verification condition 113a or the simplified verification condition to the validity determination unit 180 .

As described above, the result processing unit 119 refines the output unit 102 and/or the invariant expression processing unit 170 based on the determination result of the validity determination unit 180 or the determination result of the prior validity determination unit 116 . The return target may be transmitted to the unit 173 .

The refiner 173 of the invariant processing unit 170 refines the invariant candidate (eg, the initial invariant candidate) previously provided to the verification unit 110 based on the return target transmitted from the result processing unit 119 . By generating more specific information, it is possible to generate at least one new invariant candidate group.

According to an embodiment, the refiner 173 uses the information of the set U of the return target received from the verification unit 110 (see FIG. 6 ), and the invariant expression previously provided to the verification unit 110 . We can generate new invariant candidates by refining (ψ, μ). In this case, the refiner 173 uses at least one variable and at least one integer to be used to generate a new invariant expression from the basic statement(s) of each returned basic path using the set U of return objects. You can also extract components.

The refiner 173 is provided to refine only the invariant expression(s) present _{at the start point ( ( l 1} ) and the end point ( l ₂ ) of each of the at least one basic information present in the set U of the return object. Specifically, for example, it may be assumed that two loop labels LL1 and LL2 exist in the contract, but the refiner 173 has received a set of return targets as shown in Equation 18 below.

Here, entry _f means the entrance to the function f. In this case, the refiner 173 may determine two invariants existing at the starting point l1 of the set U of return objects, that is, a transaction invariant expression n ≤ 100, and a loop label corresponding to any one of the loop labels LL1. Although the loop invariant x=y is refined, the refiner 173 is designed not to refine the invariant corresponding to another loop label LL2 that is not defined at the starting point.

The refiner 173 may be implemented to effectively and efficiently generate an invariant candidate group based on an appropriate refinement relation. For example, if a candidate group is generated by searching for an overly general invariant expression, excessive time may be consumed in generating the invariant candidate group due to an excessive increase in the number of search targets. When generating the invariant candidate group, it may not be possible to set the invariant candidate group required for proof. Accordingly, the refiner 173 may generate an invariant candidate group suitable for contract verification by searching for an invariant that is neither overly general nor overly narrow.

For example, the refiner 173 may refine an invariant expression candidate based on an invariant expression including at least one predefined pattern expression. In this case, the refiner 173 may generate an invariant candidate group based only on an invariant formula formed by an atomic formula of a predefined pattern or a conjunctive formula of two or more atomic formulas. Here, the predefined pattern expression may include at least one expression determined according to the designer's arbitrary selection or empirical rule, for example, including the invariant expression(s) of the pattern commonly required for safety verification of smart contracts. can do.

More specifically, for example, the expression of the predefined pattern is at least one of x≥y, x=y, x=n, x≥n, x≤n, sum(x)=n, and sum(x)=y may include. Here, x and y are program variables, and n are program constants. In sum(x)=n or sum(x)=y, x means a type variable that maps an address to an unsigned integer 256bit (uint256) in the Solidity language, where the sum of all account balances in x is n or y indicates the same as The expression including sum(x) may be transformed into a primary logical expression that the validity determining unit 180 can understand. In this case, sum(x) may be expressed for a significant element and summarized and expressed as a whole for an insignificant element. Significant elements can include elements that appear in an equation. Specifically, for example, when an expression such as the following Equation 19 is given, since x is accessible by index variables of i and j, the parts by the residual index access excluding i and j are summarized and integrated into the following It can be expressed as Equation 20 of

Here, F1 indicates that the sum of all elements of x is equal to n, and can be defined as in Equation 21 below, and F2 indicates that integer overflow does not occur in the process of summing the sum of all elements of x. It can be defined as in Equation 22 below.

Here, Rx is a variable expressing the sum of elements other than x[i] and x[j], and Bx is a Boolean variable indicating that integer overflow does not occur during the operation of Rx.

Through the above-described method, the refiner 173 may newly generate an invariant candidate group. More specifically, for example, if the current invariant is (x=10, μ) (where μ is a mapping of any loop invariant), |U|=1, and the variable component extracted from the set (U) for the return target. Assuming {x, y} but no integer component, and the set U for the return target includes only transaction invariants, the refiner 173 generates an invariant candidate group as shown in Equation 23 below. will do

The newly generated invariant candidate group is transmitted to the verification unit 110 as shown in FIGS. 1 and 4 , and the verification unit 110 is the same or partially modified as described above based on the newly received invariant candidate group. The verification condition 113a is generated by the method described above, the validity of the verification condition 113a is determined, a return target is detected, and/or the determination result is transmitted to the output unit 102 .

Hereinafter, an example of a program code expressing the operation of the smart contract verification apparatus 100 described above will be described.

8 is a diagram illustrating an example in which the operation of the smart contract verification apparatus is expressed in program code.

The work set W of the first line of FIG. 8 refers to a set of invariant candidates. In this case, each invariant candidate may include a transaction invariant (ψ) and a loop invariant mapping (μ). In this case, each invariant candidate can be expressed as an invariant pair (ψ, μ).

According to the first line, the work set W may be initialized. This may be performed by the above-described initialization unit 171 . In the program code of FIG. 8, the work set W is initialized to (true, λLL.true), which is the most inaccurate invariant information. Here, λLL.true indicates in lambda notation that all loop labels LL are mapped to true.

Sequentially, in the third line, an invariant candidate having the smallest expression size may be selected from the work set W and removed. Removal of an invariant candidate having the smallest size may also be performed in the initialization unit 171 .

In the fourth line, the verification unit 110 determines whether the selected invariant candidate is inductive to the contract (c) and/or checks whether each statement (query) present in the contract (c) is safe, According to the verification result, a data pair of ( inductive, U ) is returned. As described above, inductive is a Boolean variable indicating whether or not a given invariant candidate is inductive, and U is a set of paths (ie, return targets) for which inductive or query safety proofs have failed.

As described in line 5, if the set (U) of return objects is an empty set, it means that the safety verification of the contract (c) is successful, and accordingly, the safety verification algorithm of the contract (c) is terminated. In this case, as described in line 11, the output unit 102 may output the analysis result of the contract (c).

As described in the 6th and 7th lines, if the induction or safety proof fails, the refiner 183 of the invariant processing unit 180 receives the feedback set U of return objects, and the current invariant expression Candidates (ψ, μ), for example, initialized invariant candidates, are purified to generate new invariant candidates, and new invariant candidates are added to work set W.

According to an embodiment, the safety of the program code has not been verified by the current invariant candidates (ψ, μ) as in the 8th and 9th lines, but when it is determined to be inductive (line 8), it is determined that it is inductive. The information may be transmitted to all candidates of the work set W to further refine the information of the invariant candidates (line 9). In the ninth line, μ′∧μ indicates that an AND logical operator is performed on each loop invariant of each loop label LL (ie, λLL.μ′(LL)∧μ(LL)). This may be performed by the above-described result processing unit 119 .

The above-mentioned lines 3 to 9 may be repeated until the set U of return objects is an empty set (that is, the safety of the contract c has been verified), or a predefined time expires ( 2nd line). In this process, the initially initialized invariant candidates are gradually refined and specified.

Hereinafter, the effect of the smart contract verification apparatus described above will be described with reference to FIGS. 9 and 10 .

9 is a first chart showing the results of comparing the performance of the smart contract verification device with other conventional devices, specifically comparing the performance with the bug detector by verifying integer overflow, underflow, and division by zero vulnerabilities. It's about a result. For performance comparison, after selecting any 60 out of 487 smart contracts known to have overflow vulnerabilities, for an analysis time within 30 minutes, the smart contract verification apparatus 100 and the first to fourth bug detectors described above Verification of the smart contract was performed using the , and recorded and organized as shown in FIG. 9 . In FIG. 9, #CVE vulnerability detection means the number of cases in which all known and reported vulnerabilities are detected for each contract, and #alarm is the number of cases reported by each analyzer for integer overflow, integer underflow, and division by zero vulnerabilities. It counts the total number of alarms. #False alarms are counts of cases in which the analyzer erroneously judges those that are not vulnerable as vulnerable among all the alarms generated by the analyzer.

Referring to FIG. 9 , the smart contract verification apparatus 100 described above detected 58 of the previously known 60 vulnerabilities. Of the 60 vulnerabilities, two undetected vulnerabilities actually corresponded to incorrectly reporting the safe part as a vulnerability. On the other hand, other bug detectors were able to detect only 41, 20, 10, and 2 vulnerabilities out of 60 known vulnerabilities.

In addition, as a result of analyzing other potential vulnerabilities, the above-described smart contract verification apparatus 100 detected 492 vulnerabilities in 60 contracts and output only two false alarms, so a very low false alarm rate of 0.4% was shown. On the other hand, other conventional bug detectors detected a relatively small number of vulnerabilities, and the false alarm rate was also 5.4% to 10.6%.

This indicates that the smart contract verification apparatus 100 has more accurate safety and excellent analysis power compared to the conventional bug detector.

10 is a second chart showing the results of comparing the performance of the smart contract verification device with other conventional devices, and shows the performance comparison results with the conventional verification device. 10 is a comparison of the performance of the above-described smart contract verification apparatus 100 and the conventional first and second verifiers using 25 smart contracts in which the conventional verifier generated false alarms regarding integer overflow vulnerabilities. will be. In FIG. 10 , verification success means that there are no false alarms and undetected vulnerabilities, and verification failure means that false alarms or undetected vulnerabilities exist.

As shown in FIG. 10, the smart contract verification apparatus 100 described above only outputs a false alarm for only one contract among 25 contracts that have generated false alarms, and does not output false alarms for other contracts. didn't On the other hand, the first validator did not generate an execution error in only 13 of the 25 contracts, and only one of the 13 contracts succeeded in verification. The second verifier failed all verification.

The above-described experimental results indicate that the smart contract verification apparatus 100 described above can verify smart contract vulnerabilities relatively more accurately than existing verifiers.

As described above, according to the smart contract verification apparatus 100 described above, it is possible to obtain the effect of detecting vulnerabilities more accurately and more closely compared to other conventional bug detectors or verifiers, while sounding and producing almost no false alarms.

Hereinafter, various embodiments of the smart contract verification method will be described with reference to FIGS. 11 to 13 .

11 is a flowchart of a first embodiment of a smart contract verification method.

Referring to FIG. 11 , an invariant candidate group may be initialized ( 300 ). The initialization of the invariant candidate may be performed according to a user's operation or a predefined setting. For example, the invariant candidate may be initialized with (true, λLL.true), which is the most inaccurate invariant information.

A smart contract to be analyzed and verified is obtained, and at least one verification object (eg a default path) is obtained from the smart contract ( 302 ). Acquisition of the verification target may be performed after the invariant candidate group is initialized, as shown in FIG. 11 , or may be performed before the invariant candidate group is initialized or together with initialization of the invariant expression candidate group. have.

When the at least one verification target is generated, a verification condition corresponding to the at least one verification target may be generated ( 304 ). The verification condition may be generated for all verification targets or may be generated for some verification targets. The verification condition may be expressed in the form of a predetermined formula, for example, may be expressed in the form of a first-order logical expression. According to an embodiment, the verification condition may be generated by obtaining at least one expression for whether an invariant candidate is inductive or not and whether a query is safe for at least one basic path, and more specifically, for example, It may be generated in the form of one of Equations 3 to 5.

Once the verification condition is generated, the validity of the verification condition may be checked and determined (306). In this case, the verification unit generating the verification condition may be transmitted to a validity determination unit such as an SMT solver, and the validity determination unit may determine the validity of the verification condition and then transmit the determination result to the verification unit.

As a result of the confirmation and determination, if the verification condition is valid (YES in 308), the verification process is terminated and a determination result that the smart contract is secure may be output (314). In this case, the result of determining whether the invariability of the used invariant candidate is inductive (ie, the result of determining that the inductance of the invariant candidate is recognized) may also be output.

Conversely, as a result of verification and judgment, if the verification condition is not valid (No of 308) and the verification is not terminated (No of 310), based on the information on the invalid verification target (ie, return target), Refinement is performed on the invariant candidate group (ie, the initialized candidate group) used in , and thus a new invariant candidate group may be generated ( 312 ). The new invariant candidate group may be refined based on at least one predefined pattern. For example, it is also possible to generate a group of invariant expression candidates by using a specific pattern of an atomic formula or an invariant formula formed by a bonding formula in which two or more atomic formulas are combined. Here, for example, the expression of the predefined pattern is at least one of x≥y, x=y, x=n, x≥n, x≤n, sum(x)=n, and sum(x)=y may be included, but is not limited thereto.

When a new invariant candidate group is generated, a new verification condition for a verification target may be generated based on the new invariant candidate group ( 304 ). In this case, the verification target may be the same as or different from the previously generated verification target. If necessary, the verification object may be regenerated and obtained from the contract (302). When a new validation condition is created, the validity is sequentially checked (306), if it is valid, the validation is terminated, and the result is output (examples of 308 and 314), or a new invariant candidate group is generated again if it is still not valid. generated (312). Accordingly, the above-described steps 302 to 314 are repeated until all of the verification conditions are valid (YES in 308) or the verification is finished (YES in 310).

On the other hand, as a result of the verification and determination, the verification condition is not valid (No of 308), but the verification may be terminated depending on whether a predefined verification end condition (eg, the verification time is exceeded) is satisfied (Yes of 310) ). In this case, depending on the embodiment, the reason for the completion of verification (exceeding the verification time, etc.) may be output to the outside ( 314 ).

12 is a flowchart of a second embodiment of a smart contract verification method.

According to another embodiment, in the smart contract verification method, the invariant candidate group is initialized as described above, the smart contract to be analyzed and verified is obtained, and at least one verification target (eg, the default path) is obtained from the smart contract. may be (320). These processes may be performed simultaneously or at the same time.

Verification conditions may be sequentially generated for all or a part of at least one verification target ( 322 ).

When the verification condition is generated, simplification may be further performed on the generated verification condition ( 324 ). The verification condition may be briefly modified or changed, for example, based on a predefined simplification rule. Here, the predefined simplification rule may be defined based on various formulas, laws, and/or axioms previously defined mathematically or logically, as described above.

If the verification condition is simplified, validity of the simplified verification condition may be checked and determined ( 326 ). In this case, the validity determination of the simplified verification condition may be performed by the validity determination unit, not the verification unit that generated and simplified the verification condition. The validity determination unit transmits the determination result to the verification unit.

As a result of the confirmation and determination, if the verification condition is valid (YES in S328), the verification process is terminated and the determination result that the smart contract is safe may be output in a visual or auditory form (334). As described above, it is also possible to output the result of the determination that the inductiveness of the currently used invariant expression candidate is recognized.

Conversely, as a result of confirmation and determination, if the verification condition is not valid (No in 328) and the verification termination condition is not satisfied (No in 330), as described above, the verification target (ie, return target) is not valid. The invariant candidate group (ie, the initialized candidate group) may be refined using the information about the invariant expression candidate group to generate a new invariant expression candidate group ( 332 ).

When a new invariant candidate group is generated, a new verification condition for the verification target is generated based on the new invariant candidate group (322), the verification of the contract is successful (Yes in 328), or a predefined verification termination condition is satisfied The above-described processes 322 to 334 may be repeated until (Yes in 330). Meanwhile, although the verification condition is not valid (No of 328), the verification may be terminated according to a predefined verification termination condition (Yes of 330).

13 is a flowchart of a third embodiment of a smart contract verification method.

According to the third embodiment of the smart contract verification method shown in FIG. 13, as described in FIGS. 11 and 12, an invariant candidate group is first initialized, a smart contract to be analyzed and verified is obtained, and at least one A verification target (eg, a default path) is obtained ( 320 ).

Subsequently, at least one verification condition may be generated for all or part of the at least one verification target ( 322 ).

When at least one verification condition is generated, the verification unit may first determine whether to transmit the verification condition to the validity determination unit ( 344 ). That is, the verification unit may determine whether to check validity in advance. For example, when the verification condition corresponds to a predefined template, the verification unit may determine to check validity in advance. For another example, the verification unit may determine whether to confirm validity in advance according to the type of verification condition.

If the verification unit determines to transmit to the validity determination unit (No in 344), the verification condition is transmitted to the validity determination unit as described above (348), and the validity determination unit may determine the validity of each of the at least one verification condition (350). ).

Conversely, if the verification unit does not transmit the verification condition to the validity determining unit and directly decides to precede the validity (Yes in 344), the verification unit may precede the validity check (346). For example, the verification unit may determine the validity of the verification condition by using a predefined template. Here, the predefined template may be defined based on a verification condition commonly generated/detected in the analysis process of a smart contract or a pattern of such verification condition. More specifically, for example, the predefined template may include content that is determined to be valid or not valid according to a verification condition of a specific pattern. As another example, the verification unit may determine the validity of the verification condition based on the type of verification condition. Specifically, the verification unit can also quickly determine the validity of the contract by examining the relationship between the prerequisites and the result based on the set of free variables.

Depending on the embodiment, it is also possible that the simplification 324 of the verification condition is further performed as shown in FIG. 12 before the prior validation 344 of validity. In this case, the verification unit determines the validity in advance based on the simplified verification conditions.

According to the validity determination result of the verification unit or the determination result of the validity determination unit, if the verification condition is valid (Yes in 352), the verification process is terminated and the determination result that the smart contract is safe may be output to the outside, and the current invariant A result of determining whether the candidate is inductive or not may also be output ( 358 ).

As a result of the validity determination of the verification unit or the determination result of the validity determination unit, if the verification condition is not valid (No in 352) and the verification is not completed (No in 354), as described above, the return target (that is, the validity Refining of the previously used invariant candidate group is performed based on the information on the verification target that has not been verified (356). Based on the new invariant candidate group generated according to the purification result, a new verification condition for an existing verification target or a new verification target may be generated ( 342 ).

Similarly, the above-described processes 342 to 358 may be repeated until the verification of the contract is successful (Yes in 352) or a predefined verification termination condition is satisfied (Yes in 354). In addition, even in the case of the third embodiment, although the verification condition is not judged to be valid (No in 352), the contract according to the verification termination condition predefined by the user or designer (for example, exceeding the verification time, etc.) Verification may be finished (Yes of 354).

The smart contract verification method according to the above-described embodiment may be implemented in the form of a program that can be driven by a computer device. Here, the program may include program instructions, data files, and data structures alone or in combination. The program may be designed and manufactured using machine code or high-level language code. The program may be specially designed to implement the above-described method, or may be implemented using various functions or definitions that are known and available to those skilled in the art of computer software. In addition, here, the computer device may be implemented including a processor or memory that enables the function of the program to be realized, and may further include a communication device if necessary.

A program for implementing the smart contract verification method described above may be recorded in a computer-readable recording medium. The computer-readable recording medium includes, for example, a magnetic disk storage medium such as a hard disk or a floppy disk, a magnetic tape, an optical recording medium such as a compact disk or DVD, a magneto-optical recording medium such as a floppy disk, and a ROM. , a semiconductor storage device such as a RAM or a flash memory, and the like, may include various types of hardware devices capable of storing a specific program executed in response to a computer call.

Although several embodiments of the smart contract verification apparatus and method have been described above, the apparatus and method are not limited only to the above-described embodiments. Various devices or methods that can be implemented by a person skilled in the art by modifying and modifying based on the above-described embodiment may also be an example of the smart contract verification device and method described above. For example, the described techniques are performed in an order different from the described method, and/or the described components of a system, structure, apparatus, circuit, etc. are combined or combined in a different form than the described method, or other components or Even if it is replaced or substituted by an equivalent, it may be an embodiment of the smart contract verification apparatus and method described above.

100: smart contract verification device
110: verification unit
111: path set generator
113: condition generator
119: result processing unit
190: invariant processing unit
191: initialization unit
193: refining unit
200: feasibility judgment unit

Claims (14)

an invariant processing unit for generating a group of invariant candidates including at least one invariant candidate; and
A verification unit for obtaining at least one verification target of a contract and generating verification conditions for each of the at least one verification target using the invariant candidate,
The verification unit detects a return target from among the at least one verification target and transmits it to the invariant processing unit, wherein the return target includes a verification target corresponding to an invalid verification condition,
The invariant processing unit generates a new invariant candidate group by refining the invariant candidate based on the at least one return target, and delivers the new invariant candidate group to the verification unit,
Smart contract verification device.
delete According to claim 1,
The invariant processing unit purifies the invariant expression candidate by detecting an invariant expression including an expression of a predefined pattern and determining it as the invariant expression candidate,
Smart contract verification device.
According to claim 1,
The verification unit transmits the verification condition to the validity determination unit, the validity determination unit determines the validity of the verification condition and then transmits the determination result to the verification unit, and the verification unit detects the return target based on the determination result Smart contract verification device.
According to claim 1,
The verification unit determines the validity of the verification condition based on the inclusion relationship of the set of free variables or a predefined template,
Smart contract verification device.
6. The method according to claim 4 or 5,
The verification unit simplifies the verification condition before transmitting the verification condition to the validity determining unit or before determining the validity of the verification condition,
Smart contract verification device.
According to claim 1,
The verification unit determines that verification is successful when the return target is absent,
Smart contract verification device.
generating a group of invariant candidates including at least one invariant candidate;
obtaining at least one verification target of the contract;
generating a verification condition for each of the at least one verification target by using the invariant candidate;
detecting a return target from among the at least one verification target, wherein the return target includes a verification target corresponding to an invalid verification condition; and
and generating a new group of invariant candidates by refining the invariant candidates based on the at least one return target.
delete 9. The method of claim 8,
The step of generating a new invariant candidate group by refining the invariant candidate based on the at least one return target includes detecting an invariant expression including an expression of a predefined pattern and determining the invariant candidate as the invariant candidate ,
Smart contract verification method.
9. The method of claim 8,
The step of detecting a return target from among the at least one verification target includes:
determining the validity of the verification condition; and
Comprising the step of detecting the return target based on the determination result of the validity,
Smart contract verification method.
9. The method of claim 8,
Further comprising the step of determining the validity of the verification condition based on the inclusion relationship of the set of free variables or a predefined template,
Smart contract verification method.
13. The method of claim 11 or 12,
Further comprising the step of simplifying the verification condition,
Smart contract verification method.
9. The method of claim 8,
Further comprising the step of determining that the verification is successful when the return target is absent,
Smart contract verification method.

Images