Agenda

Speaker: Andrea Esposito, Università degli Studi di Urbino Carlo Bo

Abstract:
We address Goguen-Meseguer's noninterference for reversible systems by relying on branching bisimilarity due to its connection with De Nicola-Montanari-Vaandrager's weak back-and-forth bisimilarity. We start by extending to the reversible setting Focardi-Gorrieri's classical taxonomy based on Milner's weak bisimilarity over nondeterministic processes, then we highlight the preservation and compositionality features of the resulting noninterference properties based on branching bisimilarity. We show the effectiveness in detecting covert channels arising in a reversible framework through some examples about database management system authentication. The same approach is subsequently applied to reversible processes exhibiting nondeterminism and probabilities expressed in the strictly alternating model of Hansson-Jonsson. We recast all the noninterference properties of interest by using weak and branching probabilistic bisimilarities, study their characteristics, establish a new taxonomy along with its relationships with the nondeterministic one, and illustrate their adequacy on a probabilistic smart contract lottery. Lastly, we consider reversible processes featuring nondeterminism and stochastic time expressed as Hermanns' interactive Markov chains. We define noninterference properties based on weak and branching stochastic bisimilarities, study their characteristics, further extend the aforementioned taxonomies, and provide some examples about obfuscation and permission mechanisms in database management systems.

Bio Sketch:
Dr. Andrea Esposito earned a Bachelor's degree in Philosophy from the University of Naples "Federico II" and a Master’s degree in Logic, History, and Philosophy of Science from the University of Florence. He subsequently obtained a Ph.D. in Research Methods in Science and Technology from the University of Urbino Carlo Bo, where he is currently working as a research fellow.
His scientific work focuses on the study of concurrent and distributed systems through process algebras, with particular attention to reversible computation and the analysis of noninterference properties. He is the author of numerous publications featured in international conference proceedings and specialized journals.