Verifying opacity by abstract interpretation.

Nowadays, preventing sensitive information leakage is a crucial issue. Indeed, in order to deploy secure computing systems, data protection is an aspect that cannot be ignored. In this respect, opacity is a security policy aiming at hiding the truth value of a predicate during computation. Unfortunately, despite its simple intended meaning, opacity is a quite difficult program property (indeed it is actually an hyperproperty) to guarantee. In this paper, we propose a verification mechanism, based on abstract interpretation, for opacity. Indeed, while studying the relation between opacity and abstract non-interference, a weakening of non-interference observing properties of program computations instead of concrete values, we noticed that under particular conditions opacity is implied by abstract non-interference. Hence, by exploiting the recently proposed static approach for verifying non-interference, based on hypersemantics, we can show how to verify abstract non-interference and therefore opacity.