Noninterference theory supports the analysis of secure computations in multi-level security systems. In the nondeterministic setting, the approach to noninterefence based on weak bisimilarity has turned out to be inadequate for reversible systems. This drawback can be overcome by employing a more expressive semantics, which has been recently proven to be branching bisimilarity. In this paper we extend the result to reversible systems that feature both nondeterminism and probabilities. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities. Then we investigate a taxonomy of those properties as well as their preservation and compositionality aspects, along with a comparison with the nondeterministic taxonomy. The adequacy of the resulting noninterference theory for reversible systems is illustrated via a probabilistic smart contract example.

Noninterference Analysis of Reversible Probabilistic Systems

Esposito, Andrea;Aldini, Alessandro;Bernardo, Marco
2024

Abstract

Noninterference theory supports the analysis of secure computations in multi-level security systems. In the nondeterministic setting, the approach to noninterefence based on weak bisimilarity has turned out to be inadequate for reversible systems. This drawback can be overcome by employing a more expressive semantics, which has been recently proven to be branching bisimilarity. In this paper we extend the result to reversible systems that feature both nondeterminism and probabilities. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities. Then we investigate a taxonomy of those properties as well as their preservation and compositionality aspects, along with a comparison with the nondeterministic taxonomy. The adequacy of the resulting noninterference theory for reversible systems is illustrated via a probabilistic smart contract example.
2024
978-3-031-62645-6
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: https://hdl.handle.net/11576/2740871
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact