CN119201564B - Method and apparatus for detecting bounded models of cyclic units - Google Patents
Method and apparatus for detecting bounded models of cyclic unitsInfo
- Publication number
- CN119201564B CN119201564B CN202411224063.5A CN202411224063A CN119201564B CN 119201564 B CN119201564 B CN 119201564B CN 202411224063 A CN202411224063 A CN 202411224063A CN 119201564 B CN119201564 B CN 119201564B
- Authority
- CN
- China
- Prior art keywords
- variable
- statement
- memory
- symbolic
- unit
- 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.)
- Active
Links
Classifications
-
- G—PHYSICS
- G06—COMPUTING OR CALCULATING; COUNTING
- G06F—ELECTRIC DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/22—Detection or location of defective computer hardware by testing during standby operation or during idle time, e.g. start-up testing
- G06F11/2273—Test methods
-
- G—PHYSICS
- G06—COMPUTING OR CALCULATING; COUNTING
- G06F—ELECTRIC DIGITAL DATA PROCESSING
- G06F11/00—Error detection; Error correction; Monitoring
- G06F11/22—Detection or location of defective computer hardware by testing during standby operation or during idle time, e.g. start-up testing
- G06F11/2268—Logging of test results
Landscapes
- Engineering & Computer Science (AREA)
- General Engineering & Computer Science (AREA)
- Theoretical Computer Science (AREA)
- Computer Hardware Design (AREA)
- Quality & Reliability (AREA)
- Physics & Mathematics (AREA)
- General Physics & Mathematics (AREA)
- Debugging And Monitoring (AREA)
Abstract
The embodiment of the specification provides a technical scheme for detecting a bounded model of a circulation unit, which abstracts continuous variable of a memory in the circulation unit of a module to be verified into a symbol variable, and sets a value interval of the symbol variable according to the element number corresponding to the continuous variable of the memory, so that the symbol variable abstract description is utilized to replace the exhaustion of a circulation statement in the circulation unit for element values, and the memory security verification of the circulation unit is performed. In addition, considering that a specific value cannot be obtained after the abstraction is a symbolic variable, in a verification statement using a result value of a circulation statement in the follow-up, setting a overexposed value range covering the value range of the result of the circulation statement for verification. In this way, the verification efficiency can be improved.
Description
Technical Field
One or more embodiments of the present disclosure relate to the field of computer technology, and in particular, to a method and apparatus for detecting a bounded model of a circulation unit.
Background
Bounded model checking (Bounded Model Checking, BMC) is a technique that verifies whether a target property is met by traversing the state space of the machine language description in a limited way. The target attributes herein may be predetermined business attributes, such as various attributes related to business logic, memory security, etc. Specifically, the BMC technology can abstract the machine language statement in the application or the module into a finite state machine, so that the statement in the machine language, the attribute to be verified and the like are encoded into SAT/SMT constraint expressions, and finally an automatic solver is called to solve the counterexample of violating the target attribute. Typically, in the presence of a counterexample, it is indicated that the corresponding target attribute is not satisfied. When the target attribute is related to memory security, the BMC technique may be used to verify whether the machine language statement is memory secure.
Because BMC technology needs to traverse the state space of an application or a module exhaustively, aiming at a circulation statement, the circulation body needs to be unfolded to a preset times, and then the state space is traversed. The extent of cyclic deployment determines the effectiveness of mining for potential safety issues. For the safety problem which can be found only by the complete unfolding circulation, when the unfolding times are too large (such as 1000 ten thousand times), the converted constraint expressions are too many, the solving time for calling the solver is also obviously increased, and even the final result cannot be generated. Therefore, how to optimize the verification scheme of the module to be tested of the circulation unit and improve the verification efficiency of the application or the module is an important technical problem.
Disclosure of Invention
One or more embodiments of the present specification describe a method and apparatus for bounded model detection of a cyclic unit to solve one or more of the problems mentioned in the background.
According to a first aspect, a bounded model detection method of a circulation unit is provided, and the method comprises the steps of identifying a memory continuous variable in a first circulation unit of a module to be detected, generating a first symbol variable for the memory continuous variable and determining a first value interval for the memory continuous variable, rewriting circulation sentences in the first circulation unit through the first symbol variable to obtain first check sentences described through the first symbol variable, rewriting sentences referring to the result values of the circulation sentences into corresponding second check sentences through determining a second value interval covering the result values of the circulation sentences, and solving constraint expressions comprising the first check sentences and the second check sentences by a solver so as to detect the bounded model of the first circulation unit.
In one embodiment, the memory continuous variable is one of an array, a vector, and a slice.
In one embodiment, the first symbolic variable is used for abstractly describing each sequence of the memory continuous variable, and the value range of the first value interval is consistent with the element number range corresponding to the memory continuous variable.
In one embodiment, the first check statement comprises a first statement for assigning values to second symbolic variables, which correspond to element addresses of each sequence of the continuous variable of the memory, obtained by performing address fetching operation on the continuous variable of the memory through the first symbolic variables, a second statement for dereferencing each second symbolic variable, and a third statement for processing elements obtained by dereferencing each second symbolic variable according to the loop statement in the first loop unit.
In one embodiment, the solving the constraint expression comprising the first check statement and the second check statement by using a solver, so that the bounded model detection of the first loop unit comprises obtaining a counterexample to feed back to a user in the case that a counterexample in a numerical processing result or an intermediate result which causes a memory overflow problem exists, otherwise, feeding back to the user no operation or obtaining verification-free information in the case that a counterexample in a numerical processing result or an intermediate result which causes a memory overflow problem does not exist.
According to a second aspect, there is provided a bounded model detecting apparatus of a circulation unit, the apparatus comprising:
the identifying unit is configured to identify the memory continuous variable in the first circulating unit of the module to be detected;
the generating unit is configured to generate a first symbol variable for the memory continuous variable and determine a first value interval for the first symbol variable;
a rewrite unit configured to rewrite a loop sentence in the first loop unit by the first symbolic variable to obtain a first check sentence described by the first symbolic variable, and
For sentences referring to the result values of the cyclic sentences, the second value interval covering the result values of the cyclic sentences is rewritten into corresponding second check sentences by determining;
And a verification unit configured to solve a constraint expression containing the first check statement and the second check statement by using a solver, thereby performing bounded model detection of the first loop unit.
According to a third aspect, there is provided a computer readable storage medium having stored thereon a computer program which, when executed in a computer, causes the computer to perform the method of the first aspect.
According to a fourth aspect, there is provided a computing device comprising a memory and a processor, wherein the memory has executable code stored therein, and wherein the processor, when executing the executable code, implements the method of the first aspect.
According to the method and the device provided by the embodiment of the specification, for the module to be tested comprising the circulation unit, in consideration of the fact that the circulation statement generally comprises the memory continuous variable, a corresponding symbol variable can be generated for the memory continuous variable, so that the memory continuous variable is described through symbol variable abstraction, namely, the memory continuous variable corresponding to a plurality of values is abstracted into the symbol variable corresponding to a corresponding value interval, and constraint expressions comprising a plurality of values of the memory continuous variable are abstracted into a small quantity of constraint expressions described by the symbol variable, such as a first check statement. And for the statement referring to the result value of the cyclic statement, the corresponding constraint expression is obtained by determining a larger value interval covering the result value of the cyclic statement to rewrite, for example, the constraint expression is recorded as a second check statement. Therefore, under the condition of reading in the process of writing and solving the check statement, a large amount of resources can be saved. And then, solving two types of constraint expressions comprising a first check statement and a second check statement by using a solver to check corresponding circulation units, so that the number of the constraint expressions is greatly reduced, and the overall check efficiency of the module to be tested is improved by solving a small number of constraint expressions.
Drawings
In order to more clearly illustrate the technical solutions of the embodiments of the present invention, the drawings required for the description of the embodiments will be briefly described below, it being obvious that the drawings in the following description are only some embodiments of the present invention, and that other drawings may be obtained according to these drawings without inventive effort for a person skilled in the art.
FIG. 1 shows a bounded model detection flow schematic of a cyclic unit according to one embodiment of the present description;
FIG. 2 is a schematic diagram of a bounded model test statement of a cyclic unit of a specific example, wherein the screen shot is included in FIG. 2, and English characters included in the screen shot can be machine language statements actually used, which are only some specific examples under the inventive concept of the present specification;
Fig. 3 shows a schematic block diagram of a bounded model detection device of a circulation unit according to one embodiment of the present description.
Detailed Description
The technical scheme provided in the specification is described below with reference to the accompanying drawings.
It is appreciated that BMC is one of the formalized attestation (Formal Verification) methods of memory security. Formalized proofs may generally utilize mathematical methods to perform a rigorous, logical analysis of computer sentences to prove that the properties or values involved in the computer sentences satisfy predetermined properties, specifications (e.g., collectively referred to as target properties), and the like. For example, if the addition result overflows, memory security issues occur. This often involves comprehensive enumeration and deduction of the variable value space and path space of the application that formed the computer sentence. Formalized proof may be performed by a verification tool (e.g., kani, etc.). Specifically, the computer sentence may be encoded in a verification tool as a verification sentence, and a solver (e.g., a SAT solver) is utilized to solve the counterexample according to a constraint expression (e.g., a SAT/SMT constraint expression) given by the verification sentence. In the absence of counterexamples, the computer sentence is indicated as meeting the target attribute, such as meeting the memory security attribute, etc.
The BMC may be directed to an application or module or the like for performing a predetermined function. The predetermined function may be a function determined according to a business requirement, such as a social function, a navigation function, a prediction function, a classification function, a calculation function, and the like. The corresponding module to be tested may be a social class application, a navigation application, a predictive service module, a classification service module, a privacy calculation module, etc. The processing object targeted by the BMC verification can be the source code of the module to be tested. In this specification, applications or modules to be inspected are collectively referred to as modules to be tested.
For modules under test that contain loop units (Loops), conventional techniques often provide only proof of a limited limit. Specifically, one approach is, for example, a method that utilizes a loop invariance (loop invariants) (e.g., CBMC, etc.), which can automatically infer invariance for certain types of loops, but may not support automatic generation of loop invariance for all types of loops. Providing the loop invariance manually often requires a high degree of experience and expertise of a verifier, has a high writing threshold, is difficult to ensure correctness and integrity, and especially aims at the situation of nested loops, if all the attributes to be verified are not covered, incomplete and unreliable verification results can be caused. Another approach is to directly expand the loops (as provided by cbmc—the unwind N option, where N is the number of times all loops are expanded). For the case of a large upper bound or nested loop, it is not practical to unroll. To ensure termination of the validation analysis, it is often necessary to determine an upper limit, i.e., the number of iterations of the Loop (i.e., loop Bound). Limiting Loop Bound means that only module behavior within a limited execution step can be checked. This may result in the BMC failing to discover errors that would only occur over a longer execution path. If the set Loop Bound is less than the number of actual Loop iterations, a true error may be missed. In addition, for a large or complex practical system containing a large number of Loops, even if a reasonable Loop bounds condition is provided, the state space may increase exponentially due to the existence of a large number of states to be verified, i.e. the state space explodes, so that the computational complexity and the memory requirement are obviously increased, and the verification efficiency is affected.
In view of this, the present disclosure provides a technical solution for bounded model detection, which considers that, for a module to be detected including a cyclic unit, an object that is generally operated in a cyclic statement is a memory continuous variable, and may generate a corresponding symbol variable for the memory continuous variable, where the symbol variable may correspond to an index interval, and each element in the memory continuous variable is represented by the index interval. For operations on any element in the memory continuation variable using a loop, the operation on the symbolic variable may be replaced, and thus the loop may be removed by the symbolic variable in the validation statement. Thus, the full expansion of the original loop translates into a large number of constraint expressions, and a small number of constraint expressions for a single symbolic variable. And for the statement for rewriting the result value of the cyclic statement, the corresponding constraint expression is obtained by determining a larger value interval covering the result value of the cyclic statement for rewriting. Under the condition of reading in the process of writing and solving the check statement, a large amount of resources can be saved. And then, solving the two types of constraint expressions by using a solver to test the corresponding circulation units, thereby greatly reducing the number of the constraint expressions and improving the overall test efficiency of the module to be tested.
The technical idea of the present specification is described in detail below with reference to the embodiment shown in fig. 1.
FIG. 1 illustrates a bounded model detection flow of a cyclic unit according to one embodiment of the present description. The execution subject of the process can be any computer, equipment or server with certain computing power.
As shown in fig. 1, the bounded model detection procedure of the cyclic unit provided in the embodiment of the present disclosure may include the following steps:
The method comprises the steps of identifying a memory continuous variable in a first circulation unit of a module to be tested, generating a first symbol variable for the memory continuous variable and determining a first value interval for the first symbol variable, writing a circulation statement in the first circulation unit through the first symbol variable to obtain a first check statement described through the first symbol variable, 104 writing a statement referring to a result value of the circulation statement into a corresponding second check statement through determining a second value interval covering the result value of the circulation statement, and 105 solving a constraint expression comprising the first check statement and the second check statement by a solver to detect a bounded model of the first circulation unit.
First, in step 101, a memory continuous variable in a first loop unit of a module under test is identified.
The first circulation unit may be any operation unit for realizing a circulation operation function of the module to be tested.
For example, FIG. 2 shows a specific example of a cyclic unit, wherein the cyclic unit is an array summing unit described in the following machine language (e.g., rust):
Where 1 to 5 denote the number of rows, a, b are two arrays defined as generalization, the cyclic unit is used to sum the arrays a, b, and the arrays are denoted as c. T defines the type of value in the array. "&" is an address operator that returns the address of an object when & acts on the object. "a: & [ T ], b: & [ T ]" defines two address pointers to the first element addresses of arrays a and b, respectively, "c: & mut [ T ])" defines an address pointer to the sum array, pointing to the first element address of the sum array c. "x" is the dereferencing operator, returning the value of the object pointed to by the corresponding pointer. * r, x and y are the values of specific elements in the corresponding addresses in the arrays c, a and b respectively.
Generally, a memory continuous variable is a variable in which addresses are stored in a memory, and common memory continuous variables include an array, a vector, a slice (such as a Rust slice type, etc.), and the like. When processing is performed, corresponding elements are sequentially read out and processed along with the gradual increase of addresses. It can be seen that in the cyclic unit example described in the above sentence, the elements in the arrays a and b are added one by one in the process that the address pointer is gradually increased. The cyclic rotation is consistent with the number of elements in the arrays a and b. The memory continuation type variable may be identified by a predetermined type (e.g., array type, vector type, slice type, etc.). As in this step 101, arrays a, b, c can be identified as memory continuation variables.
Next, a first symbolic variable is generated for the memory continuous variable and a first value interval is determined for the first symbolic variable, via step 102.
It will be appreciated that in order to access the memory continuation variable, a pointer (pointer) may be generated to the corresponding memory address for the elements in array a, array b, and array c. In other specific examples, the corresponding element may also be accessed via a reference (reference). Under the technical conception of the present specification, a new index symbol variable may be introduced to represent an access interval (e.g., an address interval) corresponding to the element of the identified memory continuous variable. Here, the symbol variable may be denoted as a first symbol variable, where "first" means correspondence with "first loop unit" and does not form other substantial limitation on the symbol variable itself.
As an example, for the loop unit exemplified above, an abstract symbolic variable i may be defined for replacing the respective order of the memory continuation type variable. For example, defined as "let i: usize = verifier:: any ()". The arrays a, b and c have the same length, so that the length interval can be defined by any one of the array lengths of a, b and c. "verifier:: assume (i < b.len ())", is defined by the length b.len () of the array b. In this way, the first value interval corresponding to the first symbol variable is 0 to b.len () -1, and is consistent with the array length b.len () of a, b, and c. In practice, when the length is consistent with the array length of a, b, and c, the first value interval may be defined by other manners, which is not limited herein.
Then, using step 103, the loop sentence in the first loop unit is rewritten by the first symbolic variable, resulting in a first check sentence described by the first symbolic variable.
Here, the first symbolic variable may be an abstraction of an index of elements in the memory continuation type variable. Through the abstract index symbol variable, the address of each value of the memory continuous variable can be unified abstract representation. That is, the first symbolic variable is used as an abstraction of the memory address pointed to by the memory continuous variable, and may replace any element sequence in the memory continuous variable. In this way, the processing procedure of each element in the memory continuous variable can be abstracted into the variable processing procedure uniformly described by the first symbolic variable. The processing process at least comprises 3 steps, the numerical value in the memory continuity variable is taken out, the numerical value is processed, and the value is assigned to the return parameter (namely the return value). For example, "= x + & y", a process of fetching the values in the addresses corresponding to x and y, summing the fetched values (indicated by the memory continuous variable r), and assigning the summation result to the addresses corresponding to r is included.
On the one hand, through the first symbolic variable and the corresponding first value interval thereof, each element (such as an element in a and b) corresponding to the memory continuous variable in the first circulation unit and the corresponding result element (such as an element in c) can be also abstracted into the symbolic variable. For example, in the specific example above, according to the symbol variable i, the three memory continuous variables of the groups a, b, and c may be introduced with corresponding references, for example, three symbol variables rx, ry, and rr (for example, the second symbol variable) are defined by "let (rx, ry, rr) = (& a [ i ], & b [ i ], & mut c [ i ])" (for example, denoted as the first sentence), and represent the addresses & a [ i ], & b [ i ] & mut c [ i ] corresponding to the elements of any order i in the three memory continuous variables a, b, and c, respectively. Wherein, & a [ i ], & b [ i ], & mut [ c [ i ] can be understood as the element address corresponding to the sequence i in the three arrays a, b and c. The check statement "let (rx, rr) = (& a [ i ], & b [ i ] & mut c [ i ])" can replace the exhaustion of various values of i by determining the first value interval of i.
In the loop unit, the dereferencing is to acquire the corresponding numerical value so that a specific operation for the corresponding element can be applied to the specific numerical value by the dereferencing. The check statement may abstract concrete element values, but to maintain consistency with parameters in the original cyclic unit, a dereferencing operation consistent with the original cyclic unit may be performed. The dereferencing operation is a process of fetching elements in a corresponding address in the memory according to the address. In the check statement, the dereferencing operation can still be performed by "×". For example, in the example of fig. 2, corresponding to the dereferencing operation of line 3 of the loop unit, a corresponding check statement may be given as "let (x_, y_, r_) = (/ rx, ry, rr)" (e.g., noted as second statement). For the dereferencing operation of three symbolic variables, the checking of the dereferencing legitimacy of the add function in the original circulation unit can be reserved.
When the first symbol variable introduced, the second symbol variable obtained through the abstract indication of the first symbol variable and the like are used for rewriting the statement in the cyclic unit, the principle of rewriting is to ensure that the check on the safety of the memory in the cyclic unit is kept. The respective variables obtained by the dereferencing also need to be subjected to a corresponding operation to obtain an operation result, such as a summation operation in which two variables are added in the example shown in fig. 2, so as to check the memory security of the summation operation, that is, check that the addition result will not overflow, etc. Thus, for the dereferenced variables, the constraint expression may be rewritten further according to the summation process, for example, "r_ = x_ +y_" (as noted as the third statement).
The above parameter assignment statement (denoted as a first statement, such as "let (rx, ry, rr) = (& a [ i ], & b [ i ], & mut c [ i ])"), the dereferencing statement (denoted as a second statement, such as "let (x_, y_, r_) = (& rx, & rr)"), the variable processing after dereferencing (denoted as a third statement, such as "r_ = x_ +y_;") and the like) may be used as the first check statement.
From the above description, it is understood that the verification statement involved after overwriting is very few compared with the conventional technique of converting the loop unit into the verification statement after fully expanding (e.g., 10 ten thousand times). Since the writing of the cyclic unit is to access the continuous variable of the memory, the writing task is light and the correctness is easy to be ensured.
Further, according to step 104, for the statement referencing the result value of the loop statement, the corresponding second check statement is rewritten by determining a second value interval encompassing the result value of the loop statement.
It can be understood that in the above process of rewriting the loop sentence according to the symbolic variable, the memory continuous variable is abstracted into the symbolic variable, and therefore, a specific value cannot be obtained in the verification process. Considering that a write operation inside a loop causes side effects, variables declared outside the loop are affected. To ensure the correctness of the verification result (sound), these variables may be given appropriate intervals to make an overapproximation (over-approximation). That is, a broader range encompassing the original range of values is determined, for example, as the second interval. For example, the result interval is 1000 to 10000, and the second value interval may describe any reasonable value range covering the result interval, such as 0 to 20000. At this time, the statement of the sum value assignment check is "×rr= verifier:: any ()". Here, any () means any value within the second value interval, and is an excessive approximation of the actual value.
A statement rewritten through the second value interval of the overexposure (e.g., ".rrr= verifier:: any ()") may be referred to as a second check statement.
According to the specific example shown in fig. 2, the check expression corresponding to the loop unit of the array summation can be written as:
The parameter type in the circulation unit is designated as 'T', the 3 rd line defines the consistent element quantity of the memory continuous variables a, b and c, the 7 th line defines the first symbol variable i and gives the corresponding first value range in the 8 th line, the 10 th line can abstract and describe each element in the memory continuous variable under the first value range through the first symbol variable, the 13 th line is dereferenced, the 15 th line is used for summing constraint expression, and the 17 th line is constraint expression described for the summation result value. In this specific example, lines 10, 13, 15 may be the first check statement and line 17 may be the second check statement.
In step 105, a bounded model detection of the first cyclic unit is performed by solving constraint expressions comprising the first check statement and the second check statement with a solver.
It will be appreciated that the above rewritten statements constitute constraint expressions. The solver may be used to solve for the counterexamples in constraint expressions, for example, the solver solves constraint expressions (such as constraint expressions corresponding to lines 10, 13, 15, and 17 in the above example) comprising a first check statement and a second check statement, i.e., finds whether there are counterexamples in the numerical processing results or intermediate results that cause problems such as memory overflow. If the counterexample exists, the counterexample can be acquired to be fed back to the user, and if the counterexample does not exist, no operation is performed or information with no verification errors is acquired to be fed back to the user. The solver may be any reasonable solver in the conventional technology that can be used to verify the corresponding check statement, and will not be described in detail herein. The solver often comprises various optimization algorithms, and verification sentences described for the symbolic variables can be used for solving according to a value range limited by the symbolic variables without substituting each specific numerical value for real operation.
Reviewing the above process, the bounded model detection technical concept of the circulation unit provided in the embodiments of the present disclosure abstracts the continuous variable of the memory in the circulation unit of the module to be verified into the symbolic variable, and sets the value interval of the symbolic variable according to the number of elements corresponding to the continuous variable of the memory, so that the abstract description of the symbolic variable is used to replace the exhaustion of the element values in the circulation unit to perform the memory security verification of the circulation unit, thereby greatly reducing the complexity of verification sentences, and saving a large amount of resources under the condition of reading in the verification sentence writing and solving process. And, through solving a small amount of constraint expressions, the verification efficiency can be improved.
In addition, considering that a specific value cannot be obtained after abstraction is a symbolic variable, in a verification statement using a cyclic unit result in the follow-up process, setting an over-approximation value range covering the value range of the cyclic unit result to verify, and effectively ensuring the correctness of the verification result of the follow-up statement.
According to an embodiment of another aspect, there is also provided a bounded model detecting apparatus of a circulation unit. The bounded model detecting device of the circulation unit of the graph can be arranged on a computer, equipment or a server with certain computing capability. As shown in fig. 3, the bounded model detecting apparatus 300 of the circulation unit may include:
An identifying unit 301 configured to identify a memory continuous variable in a first cyclic unit of the module to be tested;
A generating unit 302 configured to generate a first symbolic variable for the memory continuous variable and determine a first value interval for the first symbolic variable;
a rewrite unit 303 configured to rewrite the loop sentence in the first loop unit with the first symbolic variable to obtain a first check sentence described by the first symbolic variable, and
For sentences referring to the result values of the cyclic sentences, the second value interval covering the result values of the cyclic sentences is rewritten into corresponding second check sentences by determining;
a validation unit 304 configured to solve, with a solver, a constraint expression comprising a first check statement and a second check statement, thereby performing bounded model detection of the first loop unit.
In one embodiment, the memory continuation type variable is one of an array, a vector, and a slice.
The first symbolic variable is used for abstractly describing each sequence of the memory continuous variable, and the value range of the first value interval is consistent with the element number range corresponding to the memory continuous variable.
According to some alternative embodiments, the first check statement may include a first statement obtained by performing an address fetching operation on each memory continuous variable through a first symbolic variable, where the first statement is assigned to a second symbolic variable, the second symbolic variable corresponds to an element address of each sequence of the memory continuous variable, a second statement for dereferencing each second symbolic variable, and a third statement determined according to a loop statement in the first loop unit and processed by using elements obtained by dereferencing each second symbolic variable.
In one embodiment, the verification unit 304 is further configured to:
Under the condition that the counter examples in the numerical processing result or the intermediate result which cause the memory overflow problem exist, obtaining the counter examples to feed back to the user;
Otherwise, under the condition that no counter example exists in the numerical processing result or the intermediate result which causes the memory overflow problem, no operation or acquisition of verification error-free information is fed back to the user.
It should be noted that, the apparatus 300 shown in fig. 3 corresponds to the method flow described in fig. 1, and the corresponding description in the method embodiment shown in fig. 1 is also applicable to the apparatus 300, which is not repeated herein.
According to an embodiment of another aspect, there is also provided a computer-readable storage medium having stored thereon a computer program which, when executed in a computer, causes the computer to perform the method described in connection with fig. 1 and the like.
According to an embodiment of yet another aspect, there is also provided a computing device including a memory having executable code stored therein and a processor that, when executing the executable code, implements the method described in connection with fig. 1 and the like.
Those skilled in the art will appreciate that in one or more of the examples described above, the functions described in the embodiments of the present disclosure may be implemented in hardware, software, firmware, or any combination thereof. When implemented in software, these functions may be stored on or transmitted over as one or more instructions or code on a computer-readable medium.
The above-described specific embodiments are used for further describing the technical concept of the present disclosure in detail, and it should be understood that the above description is only specific embodiments of the technical concept of the present disclosure, and is not intended to limit the scope of the technical concept of the present disclosure, and any modifications, equivalent substitutions, improvements, etc. made on the basis of the technical scheme of the embodiment of the present disclosure should be included in the scope of the technical concept of the present disclosure.
Claims (10)
1. A method of bounded model detection of a cyclic unit, the method comprising:
Identifying a memory continuous variable in a first circulation unit of a module to be tested;
Generating a first symbolic variable for the memory continuous variable and determining a first value interval for the first symbolic variable, wherein the first symbolic variable is used for replacing any element sequence in the memory continuous variable, and the first value interval is used for describing the element sequence of the memory continuous variable;
the first symbolic variable represents any sequence in the memory continuous variable, and the circulation statement in the first circulation unit is rewritten to obtain a first check statement described by the first symbolic variable;
For sentences referring to the result values of the cyclic sentences, the second value interval covering the result values of the cyclic sentences is rewritten into corresponding second check sentences by determining;
And solving constraint expressions comprising the first check statement and the second check statement by utilizing a solver, so that bounded model detection of the first cyclic unit is performed.
2. The method of claim 1, wherein the memory continuation type variable is one of an array, a vector, a slice.
3. The method of claim 1, wherein the first symbolic variable is used for abstractly describing each sequence of the memory continuous variable, and a value range of the first value interval is consistent with a range of element numbers corresponding to the memory continuous variable.
4. The method of claim 1, wherein the first check statement comprises:
performing address fetching operation on each memory continuous variable through the first symbolic variable to obtain a first statement for assigning a value to a second symbolic variable, wherein the second symbolic variable corresponds to element addresses of each sequence of the memory continuous variable;
A second sentence dereferencing each second symbolic variable;
And determining a third statement which is processed by using the elements obtained by dereferencing the second symbolic variables according to the loop statement in the first loop unit.
5. The method of claim 1, wherein said solving, with a solver, a constraint expression comprising the first and second check statements, thereby performing bounded model detection of the first cyclic unit comprises:
Under the condition that the counter examples in the numerical processing result or the intermediate result which cause the memory overflow problem exist, obtaining the counter examples to feed back to the user;
Otherwise, under the condition that no counter example exists in the numerical processing result or the intermediate result which causes the memory overflow problem, no operation or acquisition of verification error-free information is fed back to the user.
6. A bounded model checking device for a cyclic unit, the device comprising:
the identifying unit is configured to identify the memory continuous variable in the first circulating unit of the module to be detected;
The generating unit is configured to generate a first symbol variable for the memory continuous variable and determine a first value interval for the first symbol variable, wherein the first symbol variable is used for replacing any element sequence in the memory continuous variable, and the first value interval is used for describing the element sequence of the memory continuous variable;
A rewrite unit configured to rewrite a loop sentence in the first loop unit by using the first symbolic variable to represent an arbitrary order in a memory continuous variable, to obtain a first check sentence described by the first symbolic variable, and
For sentences referring to the result values of the cyclic sentences, the second value interval covering the result values of the cyclic sentences is rewritten into corresponding second check sentences by determining;
And a verification unit configured to solve a constraint expression containing the first check statement and the second check statement by using a solver, thereby performing bounded model detection of the first loop unit.
7. The apparatus of claim 6, wherein the first symbolic variable is used to abstract each sequence describing the memory continuous variable, and a value range of the first value interval is consistent with a range of element numbers corresponding to the memory continuous variable.
8. The apparatus of claim 6, wherein the first check statement comprises:
performing address fetching operation on each memory continuous variable through the first symbolic variable to obtain a first statement for assigning a value to a second symbolic variable, wherein the second symbolic variable corresponds to element addresses of each sequence of the memory continuous variable;
A second sentence dereferencing each second symbolic variable;
And determining a third statement which is processed by using the elements obtained by dereferencing the second symbolic variables according to the loop statement in the first loop unit.
9. A computer readable storage medium having stored thereon a computer program which, when executed in a computer, causes the computer to perform the method of any of claims 1-5.
10. A computing device comprising a memory and a processor, wherein the memory has executable code stored therein, which when executed by the processor, implements the method of any of claims 1-5.
Priority Applications (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202411224063.5A CN119201564B (en) | 2024-09-02 | 2024-09-02 | Method and apparatus for detecting bounded models of cyclic units |
Applications Claiming Priority (1)
| Application Number | Priority Date | Filing Date | Title |
|---|---|---|---|
| CN202411224063.5A CN119201564B (en) | 2024-09-02 | 2024-09-02 | Method and apparatus for detecting bounded models of cyclic units |
Publications (2)
| Publication Number | Publication Date |
|---|---|
| CN119201564A CN119201564A (en) | 2024-12-27 |
| CN119201564B true CN119201564B (en) | 2026-01-06 |
Family
ID=94065512
Family Applications (1)
| Application Number | Title | Priority Date | Filing Date |
|---|---|---|---|
| CN202411224063.5A Active CN119201564B (en) | 2024-09-02 | 2024-09-02 | Method and apparatus for detecting bounded models of cyclic units |
Country Status (1)
| Country | Link |
|---|---|
| CN (1) | CN119201564B (en) |
Citations (2)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| EP1515251A1 (en) * | 2003-09-12 | 2005-03-16 | Nec Corporation | Efficient approaches for bounded model checking |
| CN117688876A (en) * | 2023-12-08 | 2024-03-12 | 中国科学院软件研究所 | An enhanced bounded model checking method and system based on attribute-guided reachability |
Family Cites Families (7)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| US8131661B2 (en) * | 2008-03-03 | 2012-03-06 | Nec Laboratories America, Inc. | Efficient decision procedure for bounded integer non-linear operations using SMT(LIA) |
| US8601414B2 (en) * | 2009-11-12 | 2013-12-03 | The Regents Of The University Of Michigan | Automated scalable verification for hardware designs at the register transfer level |
| CN102663191B (en) * | 2012-04-09 | 2014-07-23 | 西安电子科技大学 | SAT (satisfiability) based method for bounded model checking (BMC) for propositional projection temporal logic (PPTL) |
| US9158506B2 (en) * | 2014-02-27 | 2015-10-13 | Tata Consultancy Services Limited | Loop abstraction for model checking |
| EP3859532B1 (en) * | 2020-01-31 | 2022-10-12 | Tata Consultancy Services Limited | Method and system for counter example guided loop abstraction refinement |
| CN113783721B (en) * | 2021-08-20 | 2022-06-21 | 大连理工大学 | Credibility modeling and verification method for industrial control network protocol |
| CN118295690A (en) * | 2024-05-07 | 2024-07-05 | 支付宝(杭州)信息技术有限公司 | Method and apparatus for determining loop boundaries of source code |
-
2024
- 2024-09-02 CN CN202411224063.5A patent/CN119201564B/en active Active
Patent Citations (2)
| Publication number | Priority date | Publication date | Assignee | Title |
|---|---|---|---|---|
| EP1515251A1 (en) * | 2003-09-12 | 2005-03-16 | Nec Corporation | Efficient approaches for bounded model checking |
| CN117688876A (en) * | 2023-12-08 | 2024-03-12 | 中国科学院软件研究所 | An enhanced bounded model checking method and system based on attribute-guided reachability |
Also Published As
| Publication number | Publication date |
|---|---|
| CN119201564A (en) | 2024-12-27 |
Similar Documents
| Publication | Publication Date | Title |
|---|---|---|
| CN109063477B (en) | Automatic intelligent contract code defect detection system and method | |
| CN109426723B (en) | Detection method, system, equipment and storage medium using released memory | |
| EP2420931B1 (en) | Solving hybrid constraints to generate test cases for validating a software module | |
| CN108459954B (en) | Application program vulnerability detection method and device | |
| US8572574B2 (en) | Solving hybrid constraints to validate specification requirements of a software module | |
| EP2420932B1 (en) | Solving hybrid constraints to validate a security software module for detecting injection attacks | |
| US20060253739A1 (en) | Method and apparatus for performing unit testing of software modules with use of directed automated random testing | |
| US20240121261A1 (en) | Automated Security Analysis of Software Libraries | |
| EP2718820A1 (en) | Identifying and triaging software bugs through backward propagation of under-approximated values and empiric techniques | |
| CN111045927A (en) | Performance test evaluation method and device, computer equipment and readable storage medium | |
| US11573887B2 (en) | Extracting code patches from binary code for fuzz testing | |
| Wille et al. | Debugging of inconsistent UML/OCL models | |
| Wei et al. | State-sensitive points-to analysis for the dynamic behavior of JavaScript objects | |
| JP6976064B2 (en) | Data structure abstraction for model checking | |
| JP6142705B2 (en) | Iterative generation of symbolic test drivers for object-oriented languages | |
| US9396097B2 (en) | Methods, circuits, devices, systems and associated computer executable code for testing software code | |
| CN116775040B (en) | Pile inserting method for realizing code vaccine and application testing method based on code vaccine | |
| CN113220302B (en) | Code defect static detection method and system for Internet of Things operating system | |
| CN117972707A (en) | Software vulnerability detection method, device, equipment and storage medium | |
| US11868465B2 (en) | Binary image stack cookie protection | |
| EP3765965B1 (en) | Static software analysis tool approach to determining breachable common weakness enumerations violations | |
| CN119201564B (en) | Method and apparatus for detecting bounded models of cyclic units | |
| Yousaf et al. | Efficient Identification of Race Condition Vulnerability in C Code by Abstract Interpretation and Value Analysis | |
| CN117616423A (en) | Systems, methods, and media for dynamically shaping tensors using liquid types | |
| CN106294130A (en) | A kind of unit test method and device |
Legal Events
| Date | Code | Title | Description |
|---|---|---|---|
| PB01 | Publication | ||
| PB01 | Publication | ||
| SE01 | Entry into force of request for substantive examination | ||
| SE01 | Entry into force of request for substantive examination | ||
| CB02 | Change of applicant information |
Country or region after: China Address after: 310000 Zhejiang Province, Hangzhou City, Xihu District, Xixi Road 543-569 (continuous odd numbers) Building 1, Building 2, 5th Floor, Room 518 Applicant after: Alipay (Hangzhou) Digital Service Technology Co.,Ltd. Address before: 310000 801-11 section B, 8th floor, 556 Xixi Road, Xihu District, Hangzhou City, Zhejiang Province Applicant before: Alipay (Hangzhou) Information Technology Co., Ltd. Country or region before: China |
|
| CB02 | Change of applicant information | ||
| GR01 | Patent grant | ||
| GR01 | Patent grant |