Model the asset-flow in NuSMV

The next step is modeling the asset flows into executable NuSMV specification. In particular, the translation is performed as follows:

1. we define a module that ``works'' as the ``program counter'', that is, it encodes the sequence of actions defined by the workflow. The ``program counter'' ensures that the order in which activities are executed (let them be ``nominal'' or the execution of ``threat actions'') is the one defined by the UML diagrams.

2. we define a module for each asset that it is specified in the UML diagram. Assets have features (properties): each feature of the asset is defined as a state variable of the module encoding the asset. The transition from one asset state to the next is determined by the ``program counter'' (which represents the execution of an action of the workflow) and some accessory information such as role(s) (which encodes the relationship between the workflow activity and actors who are assigned to perform the execution of the workflow).

3. finally, we define some boolean variables to capture malicious asset flows and the execution of threat actions.

For instance, the following snippet of code defines the asset type electionSW and some of its features, named status (that is, the states in which the electionSW can be), value (the relative weight of an asset assigned based on the criticality of the asset, basically the analyst decide and assign this value), and content (that is, the qualitative value of the electionSW can be).

 
 MODULE electionSW ( ... ) 
 VAR 
 status  : {plain, encrypted}; 
 value   : {noValue, lowValue, 
 highValue,inf};
 content : {sw,esw,eesw};

Similarly, other modules with their corresponding feature variables are declared (e.g., MODULE Key(...), MODULE memorySupport (...)). ``Accessory'' information (not strictly necessary to execute the workflows), such as the actors responsible for each activity, is encoded in the model through DEFINEs in the main module, such as in the following snippet:

 
DEFINE 
 ElectoralServiceActive := pc.pc  = 
 loadMemSup || [...]

Evolution of assets' properties are encoded using state machines, which are encoded in NuSMV with the next construct (which specifies the value of a variable at step $n+1$, given the value at step $n$). Notice that asset flows are defined both in terms of the ``program counter'' (e.g. the current step of the workflow) and the value of the asset features. Figure 5 shows a model of feature content variable of electionSW asset where it's state changes according to the program counters and some other variables; its corresponding snippet NuSMV code is also given below:

Figure 5: A simple example of state transition model for content feature of electionSW.

 
[...]
next(sw.content) := case 
(pc.pc = encrypt && 
 content =  sw) || 
(content = eesw &&  
 pc.pc =  openEnvelope && 
 POfficersActive) 
:esw;  
(pc.pc = loadEnvelope && 
(TechnicianTwoActive ||
ElectoralServiceActive) && content 
= esw)
:eesw; 
pc.pc =decrypt &&POfficersActive  
&&(status = encrypted 
|| content = esw) && !fakeKey 
:sw; 
[...]

Note that in the code above we have left some detail specification (such as location) for the matter of presentation purpose.

Threat injection (model extension) corresponds to augmenting the state machine of the asset flow with new transitions corresponding to the execution of threat actions. Figure 6, for instance, shows an asset flow with some threat actions that may alter a feature of an asset (e.g. content), in some undesired way.

Figure 6: An extension of Figure 5.

The triggering of a threat action is "monitored" through boolean variables that are set to true when the action takes place, as illustrated by the following pieces of code. We first declare one boolean variable per threat:

 can_mesw, can_meesw: boolean; 
 can_garbageSW: boolean; 
 can_mPPin, can_mePPin: boolean

The above variables are initially set to false. When a variable is set to true (either because constrained to do so by the model or, more often, at random⁴), a transition in the state machine encoding the asset flow is triggered and the value of the asset flow changed according to the threat-action (rather than to the nominal flow), as illustrated by the following piece of code:

 next(can_mesw) := case 
 (malS && pc.mpc = replaceS &&  
 (next(pc.pc)=loadMemSup)) 
 || (can_meesw && pc.pc = 
 openEnvelope) 
 :1;
 1: can_mesw;
 esac;