Using Statistical Model Checking for Cybersecurity Analysis

This work discusses an approach to estimate the likelihood of occurrence and evolution in time of software security issues. First, software vulnerability assessment is revised under the light of recent studies. Then, guidelines are proposed that allow for (formal) modelling stochastic aspects of cybersecurity-relevant scenarios. This opens a connection to the field of formal methods, where automated tools like statistical model checkers can estimate the value of property queries characterising such scenarios. But exploitable vulnerabilities and attacks in cybersecurity are rare events, which calls for specialised tools. In view of this, the work finalises presenting FIG, a statistical model checker specialised on rare event simulation. FIG, an open source software tool freely available at https://git.cs.famaf.unc.edu.ar/dsg/fig, can be used to estimate the probability of an attack within the next release cycle.