CN112364392B - A method to prove the security of high-order power consumption side channels of programs based on graph isomorphism - Google Patents

Abstract

The application relates to a proving method of program high-order power consumption side channel safety based on graph isomorphism. The method provided by the application judges whether the joint probability distribution of two variable sets is the same or not through isomorphism of the variable type sensitive graph. In the method provided by the application, the following steps are adopted: converting the computing expression of the variable into forms such as abstract syntax tree or directed acyclic graph; when the expression is simplified, in order to ensure that the verification result is not influenced, an equivalent rule in algebra is adopted; for constants in the expression, when the constants are reduced by a method of replacing the sub-expressions, the joint probability distribution of the observable variable set is ensured to be unchanged. Through a plurality of experiments, the method provided by the application can effectively reduce the number of times of model counting and solving, thereby improving the verification efficiency.

Description

A method to prove the security of high-order power consumption side channels of programs based on graph isomorphism

Technical field

The invention relates to a method for proving the security of a program's high-order power consumption side channel based on graph isomorphism, which can be applied to the verification of the security of a random mask's high-order power consumption side channel.

Background technique

With the development of information technology, cryptographic algorithms are widely used to protect the transmission and processing of private data. Modern cryptography is built on computational complexity, so keys are difficult to crack through brute force enumeration attacks. However, the side-channel attack proposed by Kocher, Quisquater, Mangard and others can quickly crack the key by using physical information such as time, power consumption, and electromagnetic radiation when the system is running.

Random masking is an effective strategy to defend against power-consuming side channel attacks, so it has been researched and adopted by domestic and foreign research institutes and enterprises. Random masking uses a random number mask to avoid statistical dependencies between physical information and encryption keys. Programs using n-order masks should theoretically be resistant to n-order power-consuming side-channel attacks. However, correctly implementing n-order mask cryptographic algorithms is a complex and error-prone task, so automated verification methods are needed to prove the high-order power side channel security of the program.

Proof methods based on type derivation and proof methods based on model counting solutions have been proposed to prove the security of high-order power consumption side channels. The proof method based on type derivation is efficient, but there are false positives resulting in false positives; the proof method based on model counting does not theoretically have false positives, but it cannot efficiently verify the complete program due to the high computational cost.

Contents of the invention

The purpose of the present invention is to reduce the number of model counting and solving times and effectively improve the verification efficiency.

In order to achieve the above objectives, the technical solution of the present invention is to provide a method for proving the security of program high-order power consumption side channels based on graph isomorphism, which is characterized by including the following steps:

Step 1. Enter the program and its variable types, mutually disjoint sets T ₁ and T ₂ , where: the joint statistical distribution of the set of observable variables in any set T ₁ is independent of the key, and the joint statistical distribution of the set of observable variables in any set T ₂ The joint statistical distribution of a set of variables is not independent of the key;

Step 2. Construct an intermediate representation of the input program, which is an abstract syntax tree or directed acyclic graph;

For any set t containing d observable variables, the intermediate representation is t abstract syntax trees or directed acyclic graphs; an abstract syntax tree or directed acyclic graph corresponds to a calculation expression, and the abstract syntax tree or directed acyclic graph corresponds to a calculation expression. The middle nodes of the directional acyclic graph correspond to the operators of the calculation expression, and the leaf nodes correspond to the input variables of the calculation expression;

Step 3. For any set t containing d observable variables, check whether the corresponding t abstract syntax trees or directed acyclic graphs contain constants. If there are constants, proceed to step 4 to simplify and sum the expression. Transform; if there is no constant, go to step 6 for variable type-sensitive graph isomorphism checking;

Step 4. Equivalently transform the subexpressions in t abstract syntax trees or directed acyclic graphs so that the appearance form of each constant c becomes x☉c, where x is a variable and ☉ represents addition, subtraction, For any operator in XOR, the appearance form of x in t abstract syntax trees or directed acyclic graphs can only be x☉c, or x☉c ₁ and c ₁ represents other constants different from c;

Step 5. For all sub-expressions of the form x☉c in t abstract syntax trees or directed acyclic graphs, iteratively perform the following steps 5.1 and 5.2 to reduce the constants:

Step 5.1. Replace all subexpressions x☉c with x;

Step 5.2, replace all sub-expressions x☉c ₁ with x☉c ₂ , where If ☉ is the XOR operator, then // Represents the exclusive OR operator; if ☉ is an addition or subtraction operator, then /> Represents the subtraction operator.

Step 6. Find whether there is an observable variable set t ₁ in the set T ₁ and the set T ₂ , so that the set t and the observable variable set t ₁ are variable type-sensitive graph isomorphisms, that is, the following two conditions are met at the same time:

Condition 1) The observable variable set t ₁ and the set t have the same size;

Condition 2) There is a one-to-one correspondence h:t1→t between the set of observable variables t ₁ and the set t, so that the abstract syntax tree or directed acyclic graph of any pair of variables (x, h(x)) is The graph isomorphism, and the corresponding variables in the graph isomorphism have the same type, h(x) is the corresponding relationship function;

Step 7. If an observable variable set t ₁ described in step 6 is found in the set T ₁ , prove that the joint statistical distribution of the set t is independent of the key; if an observable variable set t 1 described in step 6 is found in the set T ₂ The set of observable variables t ₁ , then it is proved that the joint statistical distribution of the set t is not independent of the key; if the set of observable variables t ₁ described in step 6 does not exist in the set T ₁ and the set T ₂ , the set cannot be determined Whether the joint statistical distribution of t is independent of the key.

Preferably, in step 1, the variable types include key variables, plaintext variables and random variables.

Preferably, in step 2, an intermediate representation of the input program is constructed through a lexical analyzer and a syntax analyzer of compilation technology.

Preferably, in step 4, the subexpressions in the t abstract syntax trees or directed acyclic graphs are equivalently transformed according to the equivalence rules in algebra, such as associative law, commutative law, distributive law, etc. .

The method provided by the present invention determines whether the joint probability distributions of two variable sets are the same through variable type-sensitive graph isomorphism. In the method provided by the present invention: the calculation expression of the variable is converted into an abstract syntax tree or a directed acyclic graph; when simplifying the expression, in order to ensure that it does not affect the verification result, the equation in algebra is used Valence rules; for constants in expressions, when reducing the constants through subexpression substitution, the joint probability distribution of the set of observable variables is guaranteed to remain unchanged. Through multiple experiments, the method proposed by the present invention can effectively reduce the number of model count solutions, thereby improving verification efficiency.

Description of drawings

Figure 1 shows the specific steps of the present invention;

Figure 2 is an example abstract syntax tree, in which the leaf nodes are variables and constants, and the intermediate nodes are operators;

Figure 3 shows the abstract syntax tree after expression reduction of the calculation expressions of variables y and z in the example;

Figure 4 shows the abstract syntax tree after step 5 of the calculation expressions of variables y and z in the example.

Detailed ways

The present invention will be further described below in conjunction with specific embodiments. It should be understood that these examples are only used to illustrate the invention and are not intended to limit the scope of the invention. In addition, it should be understood that after reading the teachings of the present invention, those skilled in the art can make various changes or modifications to the present invention, and these equivalent forms also fall within the scope defined by the appended claims of this application.

The present invention provides a method for proving the security of program high-order power consumption side channels based on graph isomorphism, which includes the following steps:

Step 1. Enter the program and its variable types. The variable types include three types: key variables, plaintext variables and random variables. Disjoint sets T ₁ and T ₂ , where: the set of observable variables in any set T ₁ The joint statistical distribution is independent of the key, and the joint statistical distribution of any set of observable variables in T ₂ is not independent of the key;

Step 2. Construct an intermediate representation of the input program through the lexical analyzer and syntax analyzer of compilation technology. The intermediate representation is an abstract syntax tree or a directed acyclic graph;

For any set t containing d observable variables, the intermediate representation is t abstract syntax trees or directed acyclic graphs; an abstract syntax tree or directed acyclic graph corresponds to a calculation expression, and the abstract syntax tree or directed acyclic graph corresponds to a calculation expression. The middle nodes of the directional acyclic graph correspond to the operators of the calculation expression, and the leaf nodes correspond to the input variables of the calculation expression;

Step 3. For any set t containing d observable variables, check whether the corresponding t abstract syntax trees or directed acyclic graphs contain constants. If there are constants, proceed to step 4 to simplify and sum the expression. Transform; if there is no constant, go to step 6 for variable type-sensitive graph isomorphism checking;

Step 4. According to the equivalence rules in algebra, equivalently transform the subexpressions in t abstract syntax trees or directed acyclic graphs, so that the appearance form of each constant c becomes x☉c, where x is a variable , ☉ represents any operator among addition, subtraction, and XOR. The appearance form of x in t abstract syntax trees or directed acyclic graphs can only be x☉c, or x☉c ₁ and c ₁ means different from c. other constants.

Step 5. For all sub-expressions of the form x☉c in t abstract syntax trees or directed acyclic graphs, iteratively perform the following steps 5.1 and 5.2 to reduce the constants:

Step 5.1. Replace all subexpressions x☉c with x;

Step 5.2, replace all sub-expressions x☉c ₁ with x☉c ₂ , where If ☉ is the XOR operator, then // Represents the exclusive OR operator; if ☉ is an addition or subtraction operator, then /> Represents the subtraction operator.

Step 6. Find whether there is an observable variable set t ₁ in the set T ₁ and the set T ₂ , so that the set t and the observable variable set t ₁ are variable type-sensitive graph isomorphisms, that is, the following two conditions are met at the same time:

Condition 1) The observable variable set t ₁ and the set t have the same size;

Condition 2) There is a one-to-one correspondence h:t1→t between the set of observable variables t ₁ and the set t, so that the abstract syntax tree or directed acyclic graph of any pair of variables (x, h(x)) is The graph isomorphism, and the corresponding variables in the graph isomorphism have the same type, h(x) is the corresponding relationship function;

Step 7. If an observable variable set t ₁ described in step 6 is found in the set T ₁ , prove that the joint statistical distribution of the set t is independent of the key; if an observable variable set t 1 described in step 6 is found in the set T ₂ The set of observable variables t ₁ , then it is proved that the joint statistical distribution of the set t is not independent of the key; if the set of observable variables t ₁ described in step 6 does not exist in the set T ₁ and the set T ₂ , the set cannot be determined Whether the joint statistical distribution of t is independent of the key.

According to the technical solution of the present invention, the key point of implementation is to ensure that the results of verification are not affected when simplifying expressions and reducing constants, and the results of the method based on graph isomorphism cannot cause false positives. The present invention is further described in detail, and the specific implementation technical scheme is shown in Figure 1.

Taking the observable variable set t = {x, y, z} and t ₁ = {x, y ₁ , z ₁ } as an example, the calculation expressions of x, y, z, y ₁ and z ₁ are as follows:

The calculation expression of x is x;

The calculation expression of y is

The calculation expression of z is

The calculation expression of y ₁ is

The calculation expression of z ₁ is

in is the XOR operator, k and k ₁ are key variables, x, r and r ₁ are random variables. After compilation technology processing (i.e. step 2), the abstract syntax tree of the observable variables x, y, z, y ₁ and z ₁ is shown in Figure 2.

It is assumed that the joint probability distribution of the known set t ₁ ={x, y ₁ , z ₁ } does not depend on the key variable k ₁ , that is, T ₁ ={t ₁ }.

When simplifying expressions and reducing constants, it must be ensured that the results of verification will not be affected.

When simplifying expressions, in order to ensure that the results of the verification are not affected, equivalence rules in algebra must be used, such as associative laws, commutative laws, and distributive laws; or other replacement rules that can ensure that the joint probability distribution remains unchanged .

In the above demonstration, step 3 found that the calculation expression in the set t = {x, y, z} contains constants 1 and 2. After the expression is simplified (that is, step 4): the calculation expression of y is The calculation expression of and z is/> Its abstract syntax tree is shown in Figure 3. When simplifying the expression here, the associativity law is used to ensure that it will not affect the verification result.

In step 5, consider the subexpression Will/> Replace with k; then subexpression/> Replace with Among them/> That is, the calculation expression of y becomes/> The calculation expression of and z becomes/> Changes to the expression here ensure that the joint probability distribution remains unchanged.

The results of methods based on graph isomorphism do not cause false positives.

In order to ensure that the results of methods based on graph isomorphism will not cause false positives, while satisfying graph isomorphism, it must be ensured that the corresponding variables in the graph isomorphism have the same type.

In the above demonstration, the abstract syntax tree of the expressions of variables y and z after step 5 is shown in Figure 4. It can be found that the expression abstract syntax tree of x, y, z and the expression abstract syntax tree of x, y ₁ , z ₁ are graph isomorphism, and the corresponding variable types in the graph isomorphism are the same. Therefore, it can be determined that the joint probability distribution of the set t = {x, y, z} does not depend on the key variable k. The key here is that k and k ₁ are corresponding variables in the graph isomorphism and are both key variables; similarly, r and r ₁ are corresponding variables in the graph isomorphism and have the same type and are both random variables; others are the same in the graph. The structure is that the corresponding constant values must be equal.

Claims (4)

1. The proving method of the program high-order power consumption side channel safety based on graph isomorphism is characterized by comprising the following steps:

step 1, inputting programs and variable types thereof, mutually disjoint sets T ₁ And T ₂ Wherein: any set T ₁ The joint statistical distribution of the observable variable sets in (1) is independent of the key, any set T ₂ The joint statistical distribution of the observable variable sets in (a) is not independent of the key;

step 2, constructing an intermediate representation form of the input program, wherein the intermediate representation form is an abstract syntax tree or a directed acyclic graph;

for any set t containing d observable variables, the intermediate representation is t abstract syntax trees or directed acyclic graphs; an abstract syntax tree or directed acyclic graph corresponds to a computational expression, intermediate nodes of the abstract syntax tree or directed acyclic graph correspond to operators of the computational expression, and leaf nodes correspond to input variables of the computational expression;

step 3, checking whether the corresponding t abstract syntax trees or directed acyclic graphs contain constants for any set t containing d observable variables, and if so, entering step 4 to simplify and transform the expression; if the constant is not present, the step 6 is entered to perform isomorphism check of the variable type sensitive graph;

step 4, equivalently transforming sub-expressions in t abstract syntax trees or directed acyclic graphs to change the appearance form of each constant c into x ☉ c, wherein x is a variable, ☉ represents any one operator of addition, subtraction and exclusive OR, and x can only be x ☉ c or x ☉ c in the t abstract syntax trees or directed acyclic graphs ₁ And c ₁ Representing other constants than c;

step 5, iteratively executing the following steps 5.1 and 5.2 to reduce constants for all the sub-expressions of x ☉ c in the t abstract syntax trees or the directed acyclic graph:

step 5.1, replacing all sub-expressions x ☉ c with x;

step 5.2, all sub-expressions x ☉ c ₁ Replaced by x ☉ c ₂ WhereinIf ☉ is an exclusive OR operator, then +.>Representing an exclusive or operator; if ☉ is the plus or minus operator, +.>Representing a minus operator;

step 6, in the set T ₁ Sum set T ₂ Find out whether there is an observable variable set t ₁ Such that set t and observable variable set t ₁ Is a graph isomorphism that is variable type sensitive, i.e., satisfies the following two conditions simultaneously:

condition one) Observable variable set t ₁ The size of the set t is the same as that of the set t;

condition two) observable variable set t ₁ A one-to-one correspondence h is formed between the set t and the set t, namely t1→t, so that an abstract syntax tree or a directed acyclic graph of any pair of variables (x, h (x)) is graph isomorphic, the types of corresponding variables in the graph isomorphic are the same, and h (x) is a corresponding relation function;

step 7, if in set T ₁ Find a set t of observable variables as described in step 6 ₁ The joint statistical distribution of the attestation set t is independent of the key; if at set T ₂ Find a set t of observable variables as described in step 6 ₁ The joint statistical distribution of the proof set t is not independent of the key; if set T ₁ Sum set T ₂ None of the set of observable variables t described in step 6 ₁ It cannot be determined whether the joint statistical distribution of the set t is independent of the key.

2. The method for proving the security of a program high-order power consumption side channel based on graph isomorphism according to claim 1, wherein in step 1, the variable types include a key variable, a plaintext variable and a random variable.

3. The method for proving the high-order power consumption side channel security of a program based on graph isomorphism according to claim 1, wherein in step 2, an intermediate representation of the input program is constructed by a lexical analyzer and a syntax analyzer of a compiling technique.

4. The method for proving the security of the program high-order power consumption side channel based on graph isomorphism as recited in claim 1, wherein in step 4, the sub-expressions in the t abstract syntax trees or directed acyclic graphs are equivalently transformed according to equivalence rules in algebra.