US 12,259,980 B2
Method for verifying implementation of security policy, storage medium, computer program, and processing circuit
Benoit Boyer, Rennes (FR)
Assigned to MITSUBISHI ELECTRIC CORPORATION, Tokyo (JP)
Appl. No. 17/922,687
Filed by MITSUBISHI ELECTRIC CORPORATION, Tokyo (JP)
PCT Filed Mar. 11, 2021, PCT No. PCT/JP2021/010956
§ 371(c)(1), (2) Date Nov. 1, 2022,
PCT Pub. No. WO2022/004072, PCT Pub. Date Jan. 6, 2022.
Claims priority of application No. 20305745 (EP), filed on Jul. 2, 2020.
Prior Publication US 2023/0169182 A1, Jun. 1, 2023
Int. Cl. G06F 21/57 (2013.01)
CPC G06F 21/577 (2013.01) [G06F 2221/033 (2013.01)] 14 Claims
OG exemplary drawing
 
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.