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-01-01

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.
2022
Opacity, Static analysis, Information flows, Abstract interpretation, Hyperproperties verification
File in questo prodotto:
File Dimensione Formato  
main.pdf

solo utenti autorizzati

Tipologia: Documento in Pre-print
Licenza: Accesso ristretto
Dimensione 551.16 kB
Formato Adobe PDF
551.16 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: https://hdl.handle.net/11562/1058610
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact