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.

Verifying Opacity by Abstract Interpretation

Isabella Mastroeni;Michele Pasqua
2022

Abstract

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.
Opacity, Static analysis, Information flows, Abstract interpretation, Hyperproperties verification
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/1058610
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact