Abstract Interpretation-based Verification for Confidentiality: Information Hiding and Code Protection by Abstract Interpretation

In modern computing systems, preventing sensitive information leakage is a crucial issue. Indeed, to deploy secure computing systems, data protection is an aspect that cannot be ignored. Many security requirements are adopted in this respect, such as opacity and non-interference. The first assures that the truth value of a predicate is masked during computation, while the second prevents confidential information is leaked through uncontrolled system components. Unfortunately, despite their simple intended meaning, confidentiality notions are quite difficult requirements to enforce. In fact, they are actually hyperproperties, and thus require enforcing mechanisms that reason on multiple executions at a time. To develop effective verification and validation mechanisms for confidentiality notions, it is crucial to precisely characterize the requirements of system executions they dictate. In this paper, we investigate the relation between \emph{abstract non-interference} (a weakening of non-interference observing properties of data instead of concrete values) and opacity through the lens of abstract interpretation. By adopting such a holistic, abstract approach, we show how to formally characterize the structure of confidentiality notions and to compare them in terms of the constraints on system executions they impose and verification complexity. In addition, we show how \emph{code obfuscation} can be restated as a confidentiality problem by defining a corresponding confidentiality notion that can possibly be enforced. Finally, by exploiting the recently proposed static analysis approach for verifying non-interference, based on \emph{hypersemantics}, we show how to verify abstract non-interference, therefore opacity and other security requirements. Based on abstract interpretation, this yields an effective mechanism to enforce a broad range of confidentiality notions.