We define a simple process calculus, based on Hennessy and Regan's Timed Process Language, for specifying networks of communicating programmable logic controllers (PLCs) enriched with monitors enforcing specifications compliance. We define a synthesis algorithm that given an uncorrupted PLC returns a monitor that enforces the correctness of the PLC, even when injected with malware that may forge/drop actuator commands and inter-controller communications. Then, we strengthen the capabilities of our monitors by allowing the insertion of actions to mitigate malware activities. This gives us deadlock-freedom monitoring : malware may not drag monitored controllers into deadlock states.
Industrial Control System (ICSs) are distributed systems controlling physical processes via programmable logic controllers (PLCs) connected to sensors and actuators. PLCs have an ad-hoc architecture to execute simple processes known as scan cycles. Each scan cycle consists of three phases: (i) reading of the sensor measurements of the physical process; (ii) derivation of the commands to guide the evolution of the physical process; (iii) transmission of the calculated commands to the actuator devices.
Published scan data show how thousands of PLCs are directly accessible from
the Internet [
As a consequence, extra trusted hardware components have been proposed to
enhance the security of ICS architectures [
Both architectures above have been validated by means of simulation-based techniques. However, as far as we know, formal methodologies have not been used yet to model and formally verify security-oriented architectures for ICSs.
The goal of the paper is to verify the effectiveness of a process calculus
approach to formalise runtime enforcement of specification compliance in
networks of PLCs injected with colluding malware that may forge/drop both
actuator commands and inter-controller communications3. Process calculi represent
a successful and widespread formal approach in concurrency theory relying on
a variety of behavioural equivalences (e.g., trace equivalence and bisimilarity)
for studying complex systems, such as distributed migrating systems [
Thus, we propose to synthesise a proxy from an uncorrupted PLC, to form a monitored PLC ensuring: 1. observation-based monitoring, i.e., the proxy should only look at the observables of the PLC, and not at its internal execution; 2. transparency, i.e., the semantics of the monitored PLC must not differ from the semantics of the genuine (i.e., uncorrupted) PLC; 3. sound execution of the monitored PLC, to prevent incorrect executions; 4. deadlock-freedom, i.e., an injected malware may not drag a monitored PLC into a deadlock state.
Obviously, if the PLC is compromised then its correct execution can only be
enforced with the help of an extra component, a secured proxy, as advocated by
McLaughlin [
Contribution. We define a simple timed process calculus, based on Hennessy
and Regan’s TPL [
Mon1 ` fCtrl1 j Malw1g k : : : k Monn ` fCtrln j Malwng :
3 We do not deal with alterations of sensor signals within a PLC, as they can already
occur either at the network level or within the sensor devices [
Then, we propose a synthesis function q y that, given an uncorrupted
(deterministic) PLC Ctrl returns, in polynomial time, a syntactically deterministic
[
However, our monitors do not protect against malware that may drag a
monitored PLC into a deadlock state. In fact, Equation 1 does not hold with respect
to weak bisimilarity, which is a notoriously deadlock-sensitive semantic
equivalence. Thus, in order to achieve deadlock-freedom we equip our monitors with the
semantic capability to mitigate those malicious activities that may deadlock the
controller. In practice, our monitors will be able to insert actions, i.e., to emit
correct actions in full autonomy to complete scan cycles. The enforcement
resulting from the introduction of mitigation allows us to recover deadlock-freedom
monitoring by proving Equation 1 with respect to weak bisimilarity.
Outline. Section 2 defines our process calculus to express monitored controllers
injected with malware. Section 3 defines an algorithm to synthesise our monitors.
Section 4 introduces mitigation to recover deadlock-freedom. Section 5 draws
conclusions and discusses related work. In this extended abstract, proofs are
omitted; full proofs can be found in the full version of this paper [
We define our process calculus as an extension of Hennessy and Regan’s TPL [
Let us start with some preliminary notation. We use s; sk 2 Sens for sensor signals, a; ak 2 Act for actuator commands, and c; ck 2 Chn for channel names. Controller. In our setting, controllers are nondeterministic sequential timed processes evolving through three different phases: sensing of sensor signals, communication with other controllers, and actuation. For convenience, we use four different syntactic categories to distinguish the four main states of a controller: Ctrl for initial states, Sens for sensing states, Com for communication states, and Act for actuation states. In its initial state, a controller is a recursive process starting its scan cycle in the sensing phase:
Ctrl 3 P ::= rec X:S Notice that due to the cyclic behaviour of controllers, the process variable X may syntactically occur only in the last phase, actuation. We assume time guarded recursion to avoid undesired zeno behaviours. Intuitively, in time guarded recursion the process variable must occur prefixed by at least one timed action tick.
During the sensing phase, the controller waits for a finite number of admissible sensor signals. If none of those signals arrives in the current time slot then the controller will timeout moving to the following time slot (we adopt the TPL construct b c for timeout). The controller may also sleep for a while, waiting for sensor signals to become stable. The syntax is the following:
Sens 3 S ::=
P b i2I si:SicS tick:S
C
Once the sensing phase is concluded, the controller starts its calculations that may depend on communications with other controllers. Controllers communicate to each other for mainly two reasons: either to receive notice about the state of other physical sub-processes or to require an actuation on a different physical process that will have an influence on the physical process governed by the controller. We adopt a channel-based handshake point-to-point communication paradigm. Notice that, in order to avoid starvation, the communication is always under timeout. The syntax for the communications phase is:
Comm 3 C ::=
P b i2I ci:CicC bc:CcC
A Thus, our controllers can either listen on a finite number of communication channels or transmit on specific channels to pass some local information.
Finally, in the actuation phase the controller eventually transmits a finite sequence of commands to a number of different actuators, and then, it emits a special signal end to denote the end of the scan cycle. After that, it restarts its cycle in the sensing phase via a recursive call denoted with a process variable X. In order to ensure semantics closure, we also have a construct end:P which will be only generated at runtime but never used to write PLC programs.
Act 3 A ::= a:A end:X
end:P
Remark 1 (Scan cycle duration and maximum cycle limit). Notice that any scan
cycle of a PLC must be completed within a maximum cycle limit which depends
on the controlled physical process; if this time limit is violated the PLC stops
and throws an exception [
The operational semantics of controllers is given in Table 1. In the following, we use the metavariables and to range over the set of possible actions: fs; a; a; c; c; ; tick; endg. These actions denote: sensor readings, actuator commands, drops of actuator commands, channel transmissions, channel receptions/drops, internal actions, passage of time, end of a scan cycle, respectively. Malware. Let us provide a formalisation of the malware code that we assume may be injected in a controller to compromise its runtime behaviour. The kind of malware we wish to deal with may perform the following malicious activities: (i) forging fake channel transmissions towards other controllers (via actions c); (ii) dropping incoming communications from other controllers (via actions c); (iii) forging fake actuator commands (via actions a); (iv) dropping actuator commands launched by the controller (via actions a).
The formal syntax of the admitted malware is the following: Malw 3 M ::=
P b i2I i:MicM rec X:M
X tick:M nil where the prefixes i 2 fc; c; a; ag, for i 2 I, denote the possible malicious actions mentioned above. Again, we assume time guarded recursion to avoid undesired zeno behaviours. A straightforward operational semantics is given in Table 2. Compromised controller. In our setting, a compromised controller may potentially run in parallel with an arbitrary piece of malware. The syntax is:
Z ::= P CCrtl 3 J ::= Z
S where Z 2 Ctrl [ Sens [ Comm [ Act denotes a controller in an arbitrary state, and j is the standard process algebra construct for parallel composition.
The operational semantics of a compromised controller is given by the transition rules of Table 3. Rule (Ctrl) models the genuine behaviour of the controller even in the presence of the malware. Rule (Inject) denotes the injection of a malicious fabricated action. Rule (DropAct) models the drop of an actuator command a; thus, the command a never reaches its intended actuator device. Rule (TimePar) models time synchronisation between the controller and the malware.
We recall that recursion processes in a malware are always time guarded; thus,
a malware can never inject zeno behaviours preventing the passage of time.
Remark 2 (Attacks on channels). Notice that injection/drop on communication
channels affects the interaction between controllers and not within them. For this
reason, we do not have a rule for channels similar to (DropAct). Inter-controller
malicious activities on communication channels will be prevented by the monitor.
Monitored controller(s). The core of our runtime enforcement relies on a
(recursive) timed variant of Ligatti et al.’s edit automata [
Pi2I i= i:Ei rec X:E
X Intuitively, the automaton go will admit any action of the monitored system, while the edit automaton Pi2I i= i:Ei replaces actions i with i, and then continues as Ei, for any i 2 I, with I finite. The operational semantics of our edit automata is the following: (Go) go = ! go (Edit) When an edit automaton performs a transition labeled = , with 6= and = , we say that the automaton suppresses the observable action .
Our monitored controllers, written E ` fJ g, are constituted by a (potentially) compromised controller J and an edit automaton E enforcing the behaviour of J according to the following transition rule for correction/suppression: (Enforce)
J In a monitored controller E ` fJ g with no malware inside, the enforcement never occurs, i.e., in rule (Enforce) we always have = , and the two components E and J evolve in a tethered fashion, moving through related correct states. (ParL)
N1 N1 k N2 ! N10 ! N10 k N2
(ParR) (TimeSync) (ChnSync)
N1 tick ! N10
N1 c ! N10 N2 N1 k N2
N2 N1 k N2 ! N10 k N20 tick
! N20 tick
! N10 k N20
Obviously, we can easily generalise the concept of monitored controller to a field communications network of communicating monitored controllers, each one acting on different actuators. These networks are defined via the grammar: FNet 3 N ::= E ` fJ g
N k N
and described via the operational semantics given in Table 4. Notice that
monitored controllers may interact with each other via channel communication.
Moreover, they may evolve in time when no communication occurs (we recall that
neither controllers nor malware admit zeno behaviours). This ensures us
maximal progress [
Behavioural equalities. In the paper, we adopt standard behavioural equivalences between (networks of) monitored controllers. In particular, we use trace equivalence, written ', weak similarity, denoted v, and weak bisimilarity, written . 2.1
Use case: a small water-tank system In this section, we specify the controller of a simple water-tank system depicted in Figure 1. Basically, in this system the water is pumped into the tank via a pump. Furthermore, a valve connects the tank with an external unit which is not represented. Here, we assume that the incoming water flow is lower than the out-coming flow passing through the valve.
The PLC works as follows: it waits for one time slot (to get stable sensor signals) and then checks the water level of the tank, distinguishing between three possible states. If the tank reaches a low level (signal l) then the pump is turned on (command on) and the valve gets closed (command close). If the level of the tank is high (signal h) then the PLC listens for requests arriving at channel open_req to open the valve; if the PLC gets a request then it opens the valve (command open) and returns; otherwise, it timeouts and then turns the pump off (commands o ) and closes the valve (command close). Finally, if the tank is at some intermediate level between l and h (signal m) the PLC listens for requests of water; if it gets a request of water (via the channel open_req) then it turns the pump on and opens the valve, letting the water flow out; otherwise, if it receives
ú pump water on, open off, close
Tank h− m−.
.. ml−−.. ./
. valve PLC
l, m, h open req, close req a request to close the valve (via the channel close_req) then it closes the valve, and then returns.
The specification of the controller PLC mentioned above is the following: rec X: tick:bl:on:close:end:X + h:bopen_req:open:end:Xc(o :close:end:X)c(end:X)
+ m:bopen_req:on:open:end:X + close_req:close:end:Xc(end:X) : 3
In Table 5, we provide a synthesis function q y that given a controller P 2 Ctrl returns a syntactically deterministic edit automaton E 2 Edit enforcing the correct behaviour of P , independently of the presence of an arbitrary malware M 2 Malw that attempts to inject and/or drop both actuator commands and channel communications.
In our synthesis, we adopt the following notation for co-actions regarding actuator commands and channel communications: Act , fa j a 2 Actg and Chn , fc j c 2 Chng. Furthermore, we set Act , Act[Act and Chn , Chn[Chn.
Let us comment on the details of the synthesis function q y of Table 5. The edit automaton associated to listening on sensor signals allows all incoming signals expected by the controller, together with the passage of time due to eventual timeouts. All other actions are suppressed. The edit automaton associated to the listening on communication channels is similar, except that communications that are not admitted by the controller are suppressed to prevent both drops and injections on system channels, as well as, covert communications between colluding malware running in different PLCs. Channel transmissions are allowed only when occurring, in the right order, on those channels intended by the controller; all other actions are suppressed. Only genuine actuator commands (again, in the , rec X:qSy qbPi2I si:SicSy , rec Y: Pi2I si=si:qSiy + tick=tick:qSy + , rec Y: tick=tick:qSy +
P = :Y qbc:C1cC2y qbPi2I ci:CicCy , rec Y: Pi2I ci=ci:qC2iAyct+[tCichkn=tick:qCy + P 2Act , rec Y: c=c:qC1y + tick=tick:qC2y + = :Y + , rec Y: a=a:qAy + = :Y + , rec Y: end=end:X +
P 2Act [Chn
P 2Act
P 2Act nfa;ag = :Y
P 2Act [Chn
= :Y = :Y + = :Y +
P 2Chn nfcg P = :Y 2Chn
P 2Chn n[i2I fcig = :Y = :Y qrec X:Sy qtick:Sy qa:Ay qend:Xy right order) are allowed. Drops of actuator commands, the only possible intracontroller interaction occurring between the genuine controller and the malware, are allowed because we want an observation-based monitoring. Finally, the monitoring edit automaton and the associated controller do synchronise at the end of each controller cycle via the action end: all other actions emitted by the compromised controller are suppressed, included those actions coming from the genuine controller that was left behind in its execution due to some injection attack mimicking (part of) some correct behaviour. We recall that only the construct end:X (and not end:P ) is used to write PLC programs.
Let us start with two easy observations.
Remark 3 (Observation-based monitoring). The edit automata resulting from our synthesis never correct -actions (i.e., non-observable actions). Remark 4 (Colluding malicious activities). Any inter-controller activity which does not comply with the genuine behaviour of the PLC under scrutiny is suppressed by the enforcement.
The synthesis proposed in Table 5 is suitable for implementation.
Proposition 1 (Determinism preservation). Let P 2 Ctrl be a
deterministic controller. The automaton qP y is syntactically deterministic in the sense of [
As required at the beginning of this section, the synthesised edit automata are always transparent, i.e., they never introduce non-genuine behaviours. Proposition 3 (Transparency). If P 2 Ctrl then qP y ` fP g go ` fP g:
Furthermore, our enforcement enjoys soundness preservation : in a monitored controller, a malware may never trigger an incorrect behaviour.
Proposition 4 (Soundness). Let P be an arbitrary controller and M be an arbitrary malware. Then, qP y ` fP j M g v qP y ` fP g.
In the next proposition, we provide a result that is somehow complementary to Proposition 4. The intuition being that in a monitored controller qP y ` fP j M g the controller P may execute all its (genuine) execution traces even in the presence of an arbitrary malware M . Said in other words, the controller P has a chance to follow (and complete) its correct execution, even when compromised by the presence of a malware M .
Proposition 5. Let P be an arbitrary controller and M be an arbitrary malware. Then, qP y ` fP j M g w qP y ` fP g.
By applications of Propositions 3, 4, and 5 we can summarise our enforcement in a single equation.
Theorem 1 (Weak enforcement). Let P 2 Ctrl be an arbitrary controller and M 2 Malw be an arbitrary malware. Then, qP y ` fP j M g ' go ` fP g :
The result of weak enforcement scales to field communications networks of communicating controllers compromised by the presence of colluding malware. Proposition 6 (Weak enforcement of field networks). Let Pi 2 Ctrl and Mi 2 Malw, for 1 i n. Then, Qin=1 qPiy ` fPi j Mig ' Qin=1 go ` fPig :
However, our enforcement does not enjoy deadlock-freedom.
Remark 5 (Injection attacks may prevent deadlock-freedom). In a monitored controller of the form qP y ` fP j M g, it may well happen that the malware M misleads the edit automaton qP y by injecting an untimed trace M 1! : : : n! M 0 of actions, with i 6= tick, compatible with the correct behaviour of the controller, in the sense that the very same trace may be executed by P : P 1! : : : n! Q, for some state Q. This would give rise to the following admissible execution trace for the monitored controller: qP y ` fP j M g 1! : : : n! qQy ` fP j M 0g, in which the actual controller P remains inactive. At that point, if the malware M 0 stops following an admissible runtime behaviour for the controller, the edit automaton qQy will suppress all possible actions, even those proposed by P , which was left behind in its execution. Thus, the monitored controller will continue its evolution as follows: qQy ` fP j M 0g ! : : : ! qQy ` fP 0 j M 00g. In this case, as neither the controller nor the malware can give rise to zeno behaviours, the enforced system may eventually reach a deadlock state in which (i) P 0 = end:X, (ii) M 00 = tick:M 000, for some M 000, or M 00 = nil, and (iii) qQy does not allow end-actions because it requires some actions (e.g., actuations) to be performed before ending the controller cycle. Notice that Remark 5 is not in contradiction with Proposition 5 because in that proposition we proved that a controller has a chance to follow and complete its correct behaviour in the presence of an arbitrary malware. Here, we say a different thing: a malware has a chance to deadlock our monitored controllers. 4
In this section, we introduce an extra transition rule for monitored controllers to implement mitigation, i.e., the insertion of activities in full autonomy, when the controller has lost contact with its enforcer: (Mitigation)
J end Intuitively, if the compromised controller signals the end of the scan cycle by emitting the action end and, at the same time, the current edit automaton E is not in the same state, then E will command the execution of a safe trace, without any involvement of the controller, to reach the end of the controller cycle. When both the controller and the edit automaton will be aligned (at the end of the cycle) they will synchronise on the action end, via an application of the transition rule (Enforce), and from then on they will continue in a tethered fashion.
Notice that in a monitored controller E ` fJ g where J is corrupted by some malware, the two components E and J may get misaligned as they may reach unrelated states. For instance, in case of drop of actuator commands the corrupted controller J may reach an incorrect state, leaving behind its monitoring edit automata E. In this case, the remaining observable actions in the current cycle will be suppressed until the controller reaches the end of the scan cycle, signalled by the emission of an end-action (notice that since our malware are time-guarded they cannot introduce zeno behaviours to prevent a controller to reach the end of its scan cycle). Once the compromised controller has been driven to the end of its cycle, the transition rule (Mitigation) goes into action.
Remark 6. The assumption made in Remark 1 ensures us enough time to complete the mitigation of the scan cycle, well before the maximum cycle limit.
As a main result, we prove that with the introduction of the rule (Mitigation) our runtime enforcement for controllers works faithfully up to weak bisimilarity, ensuring deadlock-freedom.
Theorem 2 (Strong enforcement). Let P 2 Ctrl be an arbitrary controller and M 2 Malw be an arbitrary malware. Then, qP y ` fP j M g go ` fP g :
Strong enforcement easily scales to field networks of communicating controllers compromised by the presence of (potentially) colluding malware. Corollary 1 (Strong enforcement of field networks). LQetnPi 2 Ctrl and Mi 2 Malw, for 1 i n. Then, Qin=1 qPiy ` fPi j Mig i=1 go ` fPig :
We have defined a formal language to express networks of monitored PLCs,
potentially compromised with colluding malware that may forge/drop actuator
commands and inter-controller communications. We do not deal with alterations
of sensor signals within a PLC, as they can already occur either at the network
level or within the sensor devices [
Related work. The notion of runtime enforcement was introduced by
Schneider [
Finally, in our companion paper [