Method for verifying implementation of security policy, storage medium, computer program, and processing circuit

Patent metadata

Field	Value
Publication number	US-12259980-B2
Application number	US-202117922687-A
Country	US
Kind code	B2
Filing date	Mar 11, 2021
Priority date	Jul 2, 2020
Publication date	Mar 25, 2025
Grant date	Mar 25, 2025

Abstract

The disclosure relates to a method for verifying an implementation of a security policy by a computer program. The method comprises obtaining (S 3 ) the computer program. The method further comprises, based on obtaining (S 2 ) a security policy correspondence table, annotating (S 4 ) the computer program with at least one annotation comprising an expected security type associated to a variable output by a critical instruction of the computer program. The method further comprises, based on obtaining (S 1 ) propagation rule sets, analyzing the instructions of the annotated computer program to associate (S 5 ) a propagated security type to each variable output by an instruction of the annotated computer program. The method further comprises verifying the implementation of the security policy by comparing (S 6 ) the propagated and expected security types. The disclosure further relates to a corresponding computer program, a corresponding computer-readable storage medium and a corresponding processing circuit.

First claim

The invention claimed is:

1. A method for verifying an implementation of a security policy by a computer program, wherein the method comprises:
for a plurality of expressions, each expression setting a content of an output variable, obtaining a propagation rule set, associated to each of the plurality of expressions, comprising at least one instruction for associating a security type to said output variable;
obtaining a security policy correspondence table associated to a subset of the plurality of expressions, the security policy correspondence table associating, for each expression of the subset, an expected security type to the output variable which content is set by each expression in the subset of the plurality of expressions;
obtaining the computer program, which comprises a plurality of instructions, each instruction being an occurrence of an expression of the plurality of expressions and at least one instruction being an occurrence of an expression of the subset;
based on the obtained security policy correspondence table, annotating the obtained computer program to obtain an annotated computer program comprising, for each instruction that is the occurrence of the expression of the subset, an annotation associated to said instruction and comprising the expected security type associated to the output variable which content is set by said expression;
by analyzing the instructions of the annotated computer program using the obtained propagation rule set, associating a propagated security type to each output variable which content is set by an instruction of the annotated computer program; and
verifying the implementation of the security policy by the computer program, by comparing, for each instruction of the annotated computer program that is the occurrence of the expression of the subset, the propagated security type with the expected security type.

2. The method according to claim 1 , wherein the propagated security type is chosen in a list of security types comprising at least a trusted type and a suspicious type.

3. The method according to claim 1 , wherein the propagated security type is chosen in a list of security types comprising at least a secret type and a public type.

4. The method according to claim 1 , wherein:
the obtained propagation rule set is associated to an expression using a reference to a variable as input data to set a given content to a given output variable,
the annotated computer program comprises an instruction being an occurrence of said expression, and
analyzing the instructions of the annotated computer program comprises associating a variable security type to the variable and associating a propagated security type to the given output variable based on the obtained propagation rule set and on the variable security type.

5. The method according to claim 1 , wherein:
the obtained propagation rule set is associated to an expression using a reference to an array of variables as input data to set a given content to a given output variable,
the array of variables comprises a plurality of variables,
the annotated computer program comprises an instruction being an occurrence of said expression, and
analyzing the instructions of the annotated computer program comprises:
associating a variable security type to each variable of the array of variables,
associating an array security type to the array of variables based on the associated variable security types, and
associating the propagated security type to the given output variable based on the obtained propagation rule set and on the array security type.

6. The method according to claim 1 , wherein:
the obtained propagation rule set is associated to an expression using a reference to a structure as input data to set a given content to a given output variable,
the structure comprises a plurality of arrays of variables,
each array of variables comprises a plurality of variables,
the annotated computer program comprises an instruction being an occurrence of said expression, and
analyzing the instructions of the annotated computer program comprises:
for each array of variables, associating a variable security type to each variable of said array of variables and associating an array security type to said array of variables based on the associated variable security types;
associating a structure security type to the structure based on the associated array security types; and
associating the propagated security type to the given output variable based on the obtained propagation rule set and on the associated structure security type.

7. The method according to claim 1 , wherein:
the obtained propagation rule set is associated to an expression using a first reference to a first variable having a first content and a second reference to a second variable having a second content as input data to output an updated first variable having the second content and an updated second variable having the first content,
the annotated computer program comprises an instruction being an occurrence of said expression, and
analyzing the instructions of the annotated computer program comprises:
associating a first variable security type to the first variable;
associating a second variable security type to the second variable;
associating the first variable security type to the updated second variable; and
associating the second variable security type to the updated first variable.

8. The method according to claim 1 , wherein:
a first obtained propagation rule set is associated to a first expression setting a first content to a first output variable,
a second obtained propagation rule set is associated to a second expression using the first output variable as an input variable to set a second content to a second output variable,
the annotated computer program comprises a first instruction being an occurrence of the first expression and a second instruction, downstream from the first expression, being an occurrence of the second expression, and
analyzing the instructions of the annotated computer program comprises associating a first propagated security type to the first output variable based on the first propagation rule set and associating a second propagated security type to the second output variable based on the second propagation rule set and on the first propagated security type.

9. The method according to claim 1 , wherein:
a first obtained propagation rule set is associated to a first expression setting a first content to a first output variable,
a second obtained propagation rule set is associated to a second expression setting a second content to the first output variable,
a third obtained propagation rule set is associated to a third expression using the first output variable as an input variable to determine an output content of a second output variable,
the annotated computer program comprises a first branch, comprising a first instruction being an occurrence of the first expression,
the annotated computer program comprises a second branch, comprising a second instruction being an occurrence of the second expression,
the annotated computer program comprises a third instruction, downstream from the first branch and the second branch, being an occurrence of the third expression, and
analyzing the instructions of the annotated computer program comprises associating a first propagated security type to the first output variable based on the first propagation rule set and on the second propagation rule set, and associating a second propagated security type to the second output variable based on the third propagation rule set and on the first propagated security type.

10. The method according to claim 1 ,

Assignees

• Mitsubishi Electric Corp

Inventors

• Boyer Benoit

Classifications

• G06F2221/033

  Test or assess software · CPC title

• G06F21/577 Primary

  Assessing vulnerabilities and evaluating computer system security · CPC title