The disclosure relates to a method for verifying an implementation of a security policy by a computer program.;The method comprises obtaining (S3) the computer program.;The method further comprises, based on obtaining (S2) a security policy correspondence table, annotating (S4) 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 (S1) propagation rule sets, analyzing the instructions of the annotated computer program to associate (S5) 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 (S6) 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.
展开▼
