Statically analyzing information flows
Isabella Mastroeni, Michele Pasqua · 2019
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 sensitive 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 domain, able to approximate the information flows occurring in the analyzed programs.