Model Checking di Attack Trees utilizzando PRISM

In the digital era, cybersecurity has become a crucial priority. As cyber threats continue to rise, tools like Attack Trees have proven to be effective methodologies for analyzing potential attack paths. However, for a more rigorous and quantitative assessment, it is useful to combine these models with formal verification techniques such as Model Checking. This thesis explores the integration of Attack Trees with probabilistic model checking, using PRISM, an advanced tool for analyzing stochastic models. After an overview of fundamental concepts, including Markov Decision Processes (MDP) and Probabilistic Timed Automata (PTA), various models are developed to simulate realistic attack scenarios. The quantitative analysis helps estimate the probability of a successful attack, the associated costs, and execution times, providing critical insights for improving defense strategies. The aim of this work is to propose a methodological framework for cybersecurity, leveraging the integration of Attack Trees and Model Checking to enhance system protection through a more formal and scientific approach.

Nell’era digitale, la sicurezza informatica è diventata una priorità fondamentale. Con l’aumento delle minacce informatiche, strumenti come gli Attack Trees si sono affermati come metodologie efficaci per analizzare i potenziali percorsi di attacco. Tuttavia, per una valutazione più rigorosa e quantitativa, è utile combinare tali modelli con tecniche formali di verifica, come il Model Checking. Questa tesi esplora l’integrazione degli Attack Trees con il model checking probabilistico, utilizzando PRISM, un tool avanzato per l’analisi di modelli stocastici. Dopo una panoramica dei concetti fondamentali, tra cui Markov Decision Processes (MDP) e Probabilistic Timed Automata (PTA), vengono sviluppati diversi modelli per simulare scenari realistici di attacco. L’analisi quantitativa permette di stimare la probabilità di successo di un attacco, i costi associati e i tempi di esecuzione, fornendo informazioni cruciali per migliorare le strategie di difesa. L’obiettivo di questo lavoro è proporre un framework metodologico per la sicurezza informatica, sfruttando l’integrazione tra Attack Trees e Model Checking al fine di rafforzare la protezione dei sistemi informatici con un approccio più formale e scientifico.