On May 28th, 2024 at 1.30 pm the seminar "Nonderminism-free stochastic automata for safety and security quantifications via fault and attack tree analysis"  will take place at DEIB Seminar Room "Nicola Schiavoni" (Building 20).

Formal guarantees on safety and security quantifications turn from desirable to necessary when studying highly-reliable systems such as nuclear power plants and satellite networks. Many a flavour of automata can be used to model these systems, and temporal logics to query the desired safety/liveness property, e.g. what is the transient probability of system failure before mission time in my Markov decision process. However, two classical limitations of these approaches put a cap on their usability: how large is the state space that can be modelled, and how general are the probabilistic distributions allowed.
While compositional variants and model abstractions can alleviate the issue, the divergent solution of trace-generation from the formal model for statistical analysis ("statistical model checking") offers a simple solution to both, but it falters to quantify rare events, like failures in highly-reliable systems. This last challenge can be overcome by rare event simulation (RES), which embedded in statistical model checking frameworks is capable of providing push-button automation that approach that of traditional model checking. In this talk we will discuss how the usually ad hoc solutions proposed by RES can be derived from the system under study, as long as the corresponding model is simulatable. We will present a compositional formalism called I/O stochastic automata that has this property, and whose models decorated with the property query of interest allow to define an importance function for automatic RES implementations. We will also show how high-level abstractions for system description, such as fault and attack trees, not only help the layman to describe their system but also provide high-level information which can further enhance the quality of the RES deployment. Last, we will briefly display some recent implementations of these frameworks for safety and security quantification, and pinpoint some open problems in the field.

Carlos E. Budde received his PhD in Computer Science in 2017 from the Universidad Nacional de Córdoba (Argentina), specialising in rare event simulation for formal methods. From 2017 to 2021 he worked as postdoc researcher at the Universiteit Twente (The Netherlands), also in collaboration with Dutch Railways, applying simulation and machine learning to big data for risk management. Since 2021 Carlos holds a position as assistant professor at the Università di Trento (Italy), using simulation and probabilistic-based analyses to assess the cybersecurity resilience of systems' models. In 2022 Carlos was awarded a Marie Curie Postdoctoral Fellowship: his ProSVED project studies how security vulnerabilities can be used for the estimation of future exploits, combining formal methods with cybersecurity analyses. In 2023 Carlos' project "SMARTITUDE" was granted PRIN/PNRR funds, on software verification, testing, and the formalisation of security models for Smart Contracts in the Ethereum blockchain.