Marco Bernardo

Andrea Esposito, Alessandro Aldini, Marco Bernardo

The theory of noninterference supports the analysis of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on bisimilarity. In a nondeterministic setting, assessing noninterference through weak bisimilarity is adequate for irreversible systems, whereas for reversible ones branching bisimilarity has been recently proven to be more appropriate. In this paper we address the same two families of systems with the difference that probabilities come into play in addition to nondeterminism according to the alternating model of Hansson and Jonsson. For irreversible systems we extend the results of Aldini, Bravetti, and Gorrieri developed in a generative-reactive probabilistic setting, while for reversible systems we extend the results of Esposito, Aldini, Bernardo, and Rossi developed in a purely nondeterministic setting. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities for irreversible and reversible systems, respectively. Then we investigate a taxonomy of those properties as well as their preservation and compositionality aspects, along with a comparison with earlier taxonomies. The adequacy of the extended noninterference theory is illustrated via a probabilistic smart contract lottery.

Marco Bernardo, Federico Calandra, Andrea Esposito et al.

Information and communication technologies are by now employed in most human activities, including economics and finance. Modern computers have reached an extraordinary power in terms of information processing, storage, retrieval, and transmission. However, several results of theoretical computer science imply the impossibility of certifying software quality in general. With the exception of safety-critical systems, this has primarily concerned information processed by confined systems, with limited socio-economic consequences. In the emerging era of technologies for exchanging tokenized assets and digital money over the Internet, such as in particular central bank digital currency (CBDC), even a minor bug could trigger a financial collapse. Although the aforementioned impossibility results cannot be overcome in an absolute sense, there exist formal methods that can provide correctness assertions for software system models under suitable conditions. We advocate their use to validate the operational resilience of software infrastructures enabling CBDC, with special emphasis on offline payments as they constitute a very critical issue.

Marco Bernardo, Edoardo Bontà, Alessandro Aldini

In the original paper, we showed how to enhance the expressiveness of a typical process algebraic architectural description language by including the capability of representing nonsynchronous communications. In particular, we extended the language by means of additional qualifiers enabling the designer to distinguish among synchronous, semi-synchronous, and asynchronous ports. Moreover, we showed how to modify techniques for detecting coordination mismatches such as the compatibility check for star topologies and the interoperability check for cycle topologies, in such a way that those two checks are applicable also in the presence of nonsynchronous communications. In this addendum, we generalize those results by showing that it is possible to verify in a component-oriented way an arbitrary property of a certain class (not only deadlock) over an entire architectural type having an arbitrary topology (not only stars and cycles) by considering also behavioral variations, exogenous variations, endogenous variations, and multiplicity variations, so to deal with the possible presence of nonsynchronous communications. The proofs are at the basis of some results mentioned in the book "A Process Algebraic Approach to Software Architecture Design" by Alessandro Aldini, Marco Bernardo, and Flavio Corradini, published by Springer in 2010.