Verifying Opacity by Abstract Interpretation

Nowadays, preventing sensitive information leakage is a crucial issue. Indeed, in order to deploy secure computing systems, data pro- tection 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 pro- pose 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 observ- ing properties of program computations instead of concrete values, we noticed that under particular conditions opacity is implied by ab- stract non-interference. Hence, by exploiting the recently proposed static approach for verifying non-interference, based on hyperse- mantics, we can show how to verify abstract non-interference and therefore opacity.