High-Performance Computing for Formal Security Assessment

Assessing the degree of security of a given system w.r.t. some attacker model and security policy can be done by means of formal methods. For instance, the system can be described as a Markov Decision Process, the security policy by means of a modal logic formula, PCTL*, and then a probabilistic model checker can return the probability with which the policy holds in the system. This methodology suffices when all the system parameters and their values are known a priori. On the other side, in case the degree of security of the system depends on the values of the system parameters, the formally security assessment task must output a probability function which takes the system parameters and returns the probability of a successful attack to the security of the system. One simple way to describe such function involves solving many instances of the probabilistic model checking problem, one for each combination of the parameter values. In this scenario, probabilistic model checking, which suffers from the state explosion problem, may become an unfeasible task for traditional workstations or even servers. In this work we introduce the tool SecMC which drives the user in the task of modeling the system under analysis and the required security policies, together with the parameters that affect them. Next, the user can specify the range of values assumed by the parameters, and the tool can take care of iterating the probabilistic model checking task, distributing the computations among different local or remote nodes of a cluster, and collect the results to produce a combined picture of how the level of security varies w.r.t. the parameter values. In this paper we show how the tool can be used in order to formally assess security of probabilistic systems known from the literature, viz. a probabilistic cryptographic protocol, a synchronization algorithm for wireless devices inspired by fireflies in nature, and the privacy of dispersed cloud storages.