The Methodology

We devise the following methodology to perform our analyses (See also Figure 2):

Figure 2: The process of formal procedural security.

The first step consists of providing (business) models of the procedures under evaluation (Step 1 of Figure 2). These models are meant to describe the process or the processes to be analyzed, and to define how assets are elaborated and transformed by such procedures. In order to ease the task of translating the models into executable specification, we decided to stick to a subset of the UML, that allows us to describe the domain concepts in a strict and defined way (see [15]). The model contains information about the procedures (workflows), the assets used, their features, and the actors and their role when participating to different workflows.

So far we managed to provide UML models of the electoral procedures in place in the Autonomous Province of Trento and in Regione Friuli Venezia Giulia. We use Visual Paradigm ³ as our reference modeling tool. See [16,17] for more details about the notation, tool support, and the model themselves.

The second step consists of ``injecting`` threat actions into the model and generate what we call extended model  (Step 2 of Figure 2). A threat is an action that alters some features of an assets or allows some actors privileges (e.g. a ``read'' privilege) on some assets. Thus, in the extended model, not only assets are modified according to what the procedures define, but they can also be transformed by the (random) execution of one or more threat actions. Since attacks depend on what threat-actions are carried out, the effectiveness of the analysis depends upon the threat actions that are defined and the injection strategy that is chosen. With respect to the first point (threat action), we allow attackers any possible privilege and action to assets. With respect to the second point, it turns out that the best and most general strategy is that of injecting all possible threat-actions at all possible steps of the nominal procedures (the model checker will then take care of ``pruning'' useless threats, namely threats which do not lead to any successful attack). The construction of the extended model, whose generation can be automated, is currently performed by hand.

The third step is encoding the asset model into executable specification (Step 3 of Figure 2). From the extended models defined at the previous step we derive executable specification that define how each asset is manipulated by the procedures. Asset flows are represented in the NuSMV input language [18]. The NuSMV model of the asset flows is based on the definition of ``program counters'' that ensure that procedures are executed according to the specifications, and by defining one module per asset with one state variable per asset-feature. The state variables encode how features change during the execution of the procedures. Accessory information, such as actors responsible for the different activities can be used, e.g., to express security properties, which, in turn, are verified against the asset model.

The fourth step is specifying security properties to model check. The specification of the desired (procedural) security properties, namely, the security goals that have to be satisfied are then encoded using LTL/CTL formula. Asset flows and security properties are then the input to NuSMV.

In step five (Step 5 of Figure 2) we perform analyses, namely, we run the model checker and collect results (counter-examples). Counter-examples of security properties found by the model checker encode sequences of actions that, if executed, pose a threat to security of one or more assets. In standard situations, the counter-example will contain the execution of one (or more) asset threat. A counter-example in which no asset threats need to be executed would show an inherent weakness in the nominal workflows or, otherwise, an error in the specifications.

The last step consists in analyzing the obtained results (Step 6 of Figure 2), by looking at the counter-examples generated by the model-checker. In particular some of the information we are interested in is:

1. The Actor-Play-Role namely, the roles actors have in the execution of the attack and the privileges they get on assets.

2. Reachability the sequence of actions leading to the violation of a security goal, with particular respect to the execution of asset-threats.

This step allows us to achieve two goals. First, it allows us to understand what are the hypotheses and conditions under which a given security goal is achieved or breached. Second, it provides information to try and modify the existing procedures, so that security breaches can be taken care of.

The analysis approach we take is very similar to that of FSAP/NuSMV-SA [19], for safety analysis, whereby a system specification is ``enriched'' with information about faults and analyzes are carried out to understand the effect and impact of faults on safety requirements expressed in the form of LTL/CTL formulae. Analogously to what happens in safety analysis when analyzing, e.g., the loss of a critical functions, enhancing the procedures results in reducing the probability of an attack or making the attack more complex, rather than eliminating it.