Statically Analyzing Information Flows - An Abstract Interpretation-based Hyperanalysis for Non-Interference.

In the context of systems security, information flows play a central role. Unhandled information flows potentially leave the door open to very dangerous types of attacks, such as code injection or sen- sitive information leakage. Information flows verification is based on the definition of Non-Interference [8], which is known to be an hyperproperty [7], i.e., a property of sets of executions. The sound verification of hyperproperties is not trivial [3, 16]: It is not easy to adapt classic verification methods, used for trace properties, in order to deal with hyperproperties. In the present work, we design an abstract interpretation-based static analyzer soundly checking Non-Interference. In particular, we define an hyper abstract do- main, able to approximate the information flows occurring in the analyzed programs.