SecureFlow is a security-oriented plug-in aimed at verifying that the values of private memory locations cannot influence the values of public locations, i.e. that there are no information leaks in the program.
In order to take advantage of the plug-in, the main locations of the program must be annotated with ACSL attributes
/*@ public */ and
/*@ private */. SecureFlow will then build upon the results of Eva and From plug-ins to check that an expression that gets stored into a
public location does not depend on any