A Trusted Safety Verifier for
Process Controller Code
Stephen McLaughlin, Devin Pohly, Patrick McDaniel and
Saman Zonouz
February 24, 2014
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 1
Control Systems Under Threat
Programmable Controllers are
Insecure By Design
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 2
Control Systems Under Threat
Programmable Controllers are
Insecure By Design
Control systems not robust enough for security patches
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page
3
Control Systems Under Threat
Programmable Controllers are
Insecure By Design
Control systems not robust enough for security patches
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page
4
A new perspective on SCADA
Supervisory Control and Data Acquisition
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page
5
A new perspective on SCADA
Tens of Millions of Files
Hundreds of Millions of LoC
Anything cloud
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page
6
A new perspective on SCADA
Far smaller codebase
Tens of Millions of Files
Hundreds of Millions of LoC
Anything cloud
Hundreds of Devices
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page
7
We would like to directly protect the
physical process, regardless of the
integrity of the IT perimeter.
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page
8
A PLC’s life
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page
9
A PLC’s life
Turn left 2º
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 10
A PLC’s life
Turn left 2º
Turn left!
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 11
A PLC’s life
Turn left 2º
Turn left!
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 12
A PLC’s life
???
Turn left!
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 13
A PLC’s life
Turn left 2º
Turn left!
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 14
A PLC’s life
Turn left 2º
Turn left!
1º
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 15
A PLC’s life
Not quite …
Turn left!
1º
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 16
A PLC’s life
Not quite …
Turn left!
2º
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 17
A PLC’s life
BINGO!
Stop!
2º
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 18
A PLC’s life
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 19
A PLC’s life
Control
Logic
L DW2
< ID255
ST Q 3.2
Systems and Internet Infrastructure Security Laboratory (SIIS)
;; Degrees
Page 20
A PLC’s life
Control
Logic
L DW2
< ID255
ST Q 3.2
;; Degrees
Control Signal
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 21
A PLC’s life
Control
Logic
L DW2
< ID255
ST Q 3.2
;; Degrees
Control Signal
Sensor
Measurements
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 22
A PLC’s life
Control
Logic
L DW2
< ID255
ST Q 3.2
;; Degrees
Control Signal
🔄
Scan Cycle
Sensor
Measurements
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 23
A PLC’s life
Applications
• Chemical processing
• Railroad safety
• Manufacturing
• Traffic Control
• PID Control
Systems and Internet Infrastructure Security Laboratory (SIIS)
L DW2
< ID255
ST Q 3.2
;; Degrees
Page 24
A PLC’s life
L DW2
< ID255
ST Q 3.2
;; Degrees
;; Spin out
;; of control!
!
S Q 3.2
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 25
A PLC’s life
L DW2
< ID255
ST Q 3.2
;; Spin out
;; of control!
;; Degrees
⨉
!
S Q 3.2
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 26
A PLC’s life
L DW2
< ID255
ST Q 3.2
;; Degrees
TSV
;; Spin out
;; of control!
!
“The Arm must remain within
a quarter hemisphere at all times”
S Q 3.2
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 27
Trusted Safety Verifier
• Goal: Only allow code to be run on a PLC if it satisfies
a set of engineer-supplied safety properties.
• Challenges:
‣
Existing tools not up to the task.
‣
Control systems are stateful, requiring temporal properties.
‣
State space explosion with existing analysis techniques.
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 28
Consider some PLC code
A I
0.5
= Q
0.1
. . .
;; And input bit 5
;; Store at output bit 1
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 29
Consider some PLC code
A I
0.5
= Q
0.1
. . .
;; And input bit 5
;; Store at output bit 1
• Side effects
!
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 30
Consider some PLC code
A I
0.5
= Q
0.1
. . .
;; And input bit 5
;; Store at output bit 1
• Side effects
• PLC special features
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 31
Consider some PLC code
A I
0.5
= Q
0.1
. . .
;; And input bit 5
;; Store at output bit 1
• Side effects
• PLC special features
• Architecture dependent
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 32
Consider some PLC code
A I
0.5
= Q
0.1
. . .
;; And input bit 5
;; Store at output bit 1
• Side effects
• PLC special features
• Architecture dependent
Instruction List
Intermediate Language
// A I 0.5
STA := load(mem, [I::0::0::0::5]);
cjmp FC == 0 : reg1_t,L1,L2;
label L1;
RLO := STA;
label L2;
RLO := RLO && STA;
FC :=1 : reg1_t;
// = Q 0.1
STA := RLO;
mem := store(mem, [Q::0::0::0::1], RLO);
FC := 0 : reg1_t;
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 33
ILIL
Based on the Vine IL
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 34
ILIL Analysis
// A I 0.5
STA := load(mem, [I::0::0::0::5]);
cjmp FC == 0 : reg1_t,L1,L2;
label L1;
RLO := STA;
label L2;
RLO := RLO && STA;
FC :=1 : reg1_t;
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
[X_7] -> (and (and X_1 true)
(not X_3))
[X_0] -> (X_2)
// = Q 0.1
STA := RLO;
mem := store(mem, [Q::0::0::0::1], RLO);
FC := 0 : reg1_t;
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 35
ILIL Analysis
Symbolic Sensor Values
// A I 0.5
STA := load(mem, [I::0::0::0::5]);
cjmp FC == 0 : reg1_t,L1,L2;
label L1;
RLO := STA;
label L2;
RLO := RLO && STA;
FC :=1 : reg1_t;
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
[X_7] -> (and (and X_1 true)
(not X_3))
[X_0] -> (X_2)
// = Q 0.1
STA := RLO;
mem := store(mem, [Q::0::0::0::1], RLO);
FC := 0 : reg1_t;
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 36
ILIL Analysis
// A I 0.5
STA := load(mem, [I::0::0::0::5]);
cjmp FC == 0 : reg1_t,L1,L2;
label L1;
RLO := STA;
label L2;
RLO := RLO && STA;
FC :=1 : reg1_t;
// = Q 0.1
STA := RLO;
mem := store(mem, [Q::0::0::0::1], RLO);
FC := 0 : reg1_t;
Systems and Internet Infrastructure Security Laboratory (SIIS)
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
[X_7] -> (and (and X_1 true)
(not X_3))
[X_0] -> (X_2)
Symbolic Control Signal
Page 37
Checking Temporal Properties
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
[X_7] -> (and (and X_1 true)
(not X_3))
[X_0] -> (X_2)
G (!a)
a: (and X_0 X_5)
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 38
removed from each state to produce an abstract graph, which
fed to the model checker. Before exploring this process in mor
detail, we briefly review LTL as used for safety specification
Checking Temporal Properties
A. Linear Temporal Logic
To formulate control system security requirements, TSV
makes use of the linear temporal logic formalism [2], [25
Let us define A to be a finite set of atomic logical proposition
about the system {b1 , b2 , · · · , b|A| }, e.g., relay R1 is open
(assert ((and (not (and X_3 X_2))
and S = 2A a finite alphabet composed of the abovementione
(not X_5)))) : propositions. Every element of the alphabet is a possibly empt
[X_5] -> (X_2)
set of propositions from A, and is denoted by ai , e.g., ai =
[X_7] -> (and (and X_1 true)
b1 , b4 , b9 .
(not X_3))
[X_0] -> (X_2)
G (!a)
a: (and X_0 X_5)
Systems and Internet Infrastructure Security Laboratory (SIIS)
The set of linear temporal logic-based safety requiremen
is inductivelyLinear
defined byTemporal
the grammar Logic
j ::= true | b | ¬j | j _ j | j U j | X j,
(1
where ¬ and _ denote negation and logical OR operator
ji U j j denotes “the LTL expression ji remains true until j
becomes true,” and X j j reads “j j must be true in the nex
step (execution state)”. TSV also makes use of the followin
redundant notations: j ^ y instead of ¬(¬j _ ¬y), j ! y
instead of ¬j _ y, F j (Eventually) instead of true U j, an
Page 39
Checking Temporal Properties
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
[X_7] -> (and (and X_1 true)
(not X_3))
[X_0] -> (X_2)
G (!a)
a: (and X_0 X_5)
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 40
Checking Temporal Properties
• Input Variables
• State Variables
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
[X_7] -> (and (and X_1 true)
(not X_3))
[X_0] -> (X_2)
G (!a)
a: (and X_0 X_5)
Systems and Internet Infrastructure Security Laboratory (SIIS)
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
. . .
???
???
(assert ((and (not (and X_3 X_2))
(X_5)))) : [X_5] -> (X_2)
. . .
Page 41
Checking Temporal Properties
• Input Variables
• State Variables
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
[X_7] -> (and (and X_1 true)
(not X_3))
[X_0] -> (X_2)
G (!a)
a: (and X_0 X_5)
Systems and Internet Infrastructure Security Laboratory (SIIS)
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
. . .
??? Reachability determined
??? by SMT solver
(assert ((and (not (and X_3 X_2))
(X_5)))) : [X_5] -> (X_2)
. . .
Page 42
Temporal
Execution
Graph
(TEG)
RLO);
onstraint for the green light
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
. . .
(assert ((and (not (and X_3 X_2))
(not X_5)))) : [X_5] -> (X_2)
[X_7] -> (and (and X_1 true)
(not X_3))
[X_0] -> (X_2)
0_0_0_0)
_0_6)) (not T_1))
(assert ((and (not (and X_3 X_2))
(X_5)))) : [X_5] -> (X_2)
. . .
Fig. 10.
Partial TEG without Symbolic State Matching
S10
<a:0 b:1>
S7
<a:0 b:1>
S11
<a:1 b:1>
S8
<a:1 b:1>
of the produced symbolic
S3
...
onding temporal execution
<a:0 b:0>
S4
y shown in Figure 10. Here,
<a:0 b:0>
ymbolic state matching to
helps TSV to save the TEG
S9
<a:1 b:0>
uently improve the overall
strates the generated TEG
he same controller program
Fig. 11. Partial TEG with Symbolic State Matching
engine was on. As shown,
beenandlumped
together
in (SIIS)
Systems
Internet Infrastructure
Security Laboratory
S5
<a:0 b:0>
S6
<a:1 b:0>
Page 43
Performance
TEG Depth bounded at 14
Time%(seconds)%
Time (s)
100$
10$
1$
0.1$
0.01$
Lifting SymEx
IL'to'ILIL$Transla0on$
Fig. 7.
Symbolic$Execu0on$
TEG1 TEG2,3 Trans NuSMV2
Ini0al$Model$Crea0on$
Temporal$Execu0on$
Graph$Genera0on$
Model$Transla0on$
Symbolic$Model$Checking$
PLC%Program%Analysis%and%Formal%Verifica9on%Steps%
Time Requirements for All Case Studies on Raspberry Pi.
The reported numbers, only 4K states for a full 14 horizon
analysis, proves the effectiveness of the usage of symbolic
execution at reducing the state space size.
Figure 6 shows a sample generated execution graph for
the Assembly
Way case
study
with
a model checking bound
Systems
and Internet Infrastructure
Security
Laboratory
(SIIS)
1000"
ber'of'States'
0.001$
100"
Page 44
Performance
Traffic Light
Time%(seconds)%
Time (s)
100$
10$
1$
0.1$
0.01$
Lifting SymEx
IL'to'ILIL$Transla0on$
Fig. 7.
Symbolic$Execu0on$
TEG1 TEG2,3 Trans NuSMV2
Ini0al$Model$Crea0on$
Temporal$Execu0on$
Graph$Genera0on$
Model$Transla0on$
Symbolic$Model$Checking$
PLC%Program%Analysis%and%Formal%Verifica9on%Steps%
Time Requirements for All Case Studies on Raspberry Pi.
The reported numbers, only 4K states for a full 14 horizon
analysis, proves the effectiveness of the usage of symbolic
execution at reducing the state space size.
Figure 6 shows a sample generated execution graph for
the Assembly
Way case
study
with
a model checking bound
Systems
and Internet Infrastructure
Security
Laboratory
(SIIS)
1000"
ber'of'States'
0.001$
100"
Page 45
Performance
Large Symbolic Scan Cycle
Assembly Way
Time%(seconds)%
Time (s)
100$
10$
1$
0.1$
0.01$
Lifting SymEx
IL'to'ILIL$Transla0on$
Fig. 7.
Symbolic$Execu0on$
TEG1 TEG2,3 Trans NuSMV2
Ini0al$Model$Crea0on$
Temporal$Execu0on$
Graph$Genera0on$
Model$Transla0on$
Symbolic$Model$Checking$
PLC%Program%Analysis%and%Formal%Verifica9on%Steps%
Time Requirements for All Case Studies on Raspberry Pi.
The reported numbers, only 4K states for a full 14 horizon
analysis, proves the effectiveness of the usage of symbolic
execution at reducing the state space size.
Figure 6 shows a sample generated execution graph for
the Assembly
Way case
study
with
a model checking bound
Systems
and Internet Infrastructure
Security
Laboratory
(SIIS)
1000"
ber'of'States'
0.001$
100"
Page 46
Performance
Stacker
Large State Space
Time%(seconds)%
Time (s)
100$
10$
1$
0.1$
0.01$
Lifting SymEx
IL'to'ILIL$Transla0on$
Fig. 7.
Symbolic$Execu0on$
TEG1 TEG2,3 Trans NuSMV2
Ini0al$Model$Crea0on$
Temporal$Execu0on$
Graph$Genera0on$
Model$Transla0on$
Symbolic$Model$Checking$
PLC%Program%Analysis%and%Formal%Verifica9on%Steps%
Time Requirements for All Case Studies on Raspberry Pi.
The reported numbers, only 4K states for a full 14 horizon
analysis, proves the effectiveness of the usage of symbolic
execution at reducing the state space size.
Figure 6 shows a sample generated execution graph for
the Assembly
Way case
study
with
a model checking bound
Systems
and Internet Infrastructure
Security
Laboratory
(SIIS)
1000"
ber'of'States'
0.001$
100"
Page 47
Performance
Complex path predicates
Sorter
Time%(seconds)%
Time (s)
100$
10$
1$
0.1$
0.01$
Lifting SymEx
IL'to'ILIL$Transla0on$
Fig. 7.
Symbolic$Execu0on$
TEG1 TEG2,3 Trans NuSMV2
Ini0al$Model$Crea0on$
Temporal$Execu0on$
Graph$Genera0on$
Model$Transla0on$
Symbolic$Model$Checking$
PLC%Program%Analysis%and%Formal%Verifica9on%Steps%
Time Requirements for All Case Studies on Raspberry Pi.
The reported numbers, only 4K states for a full 14 horizon
analysis, proves the effectiveness of the usage of symbolic
execution at reducing the state space size.
Figure 6 shows a sample generated execution graph for
the Assembly
Way case
study
with
a model checking bound
Systems
and Internet Infrastructure
Security
Laboratory
(SIIS)
1000"
ber'of'States'
0.001$
100"
Page 48
Performance
Train
Time%(seconds)%
Time (s)
100$
10$
1$
0.1$
0.01$
Lifting SymEx
IL'to'ILIL$Transla0on$
Fig. 7.
Symbolic$Execu0on$
TEG1 TEG2,3 Trans NuSMV2
Ini0al$Model$Crea0on$
Temporal$Execu0on$
Graph$Genera0on$
Model$Transla0on$
Symbolic$Model$Checking$
PLC%Program%Analysis%and%Formal%Verifica9on%Steps%
Time Requirements for All Case Studies on Raspberry Pi.
The reported numbers, only 4K states for a full 14 horizon
analysis, proves the effectiveness of the usage of symbolic
execution at reducing the state space size.
Figure 6 shows a sample generated execution graph for
the Assembly
Way case
study
with
a model checking bound
Systems
and Internet Infrastructure
Security
Laboratory
(SIIS)
1000"
ber'of'States'
0.001$
100"
Page 49
Performance
PID
Time%(seconds)%
Time (s)
100$
10$
1$
0.1$
0.01$
Lifting SymEx
IL'to'ILIL$Transla0on$
Fig. 7.
Symbolic$Execu0on$
TEG1 TEG2,3 Trans NuSMV2
Ini0al$Model$Crea0on$
Temporal$Execu0on$
Graph$Genera0on$
Model$Transla0on$
Symbolic$Model$Checking$
PLC%Program%Analysis%and%Formal%Verifica9on%Steps%
Time Requirements for All Case Studies on Raspberry Pi.
The reported numbers, only 4K states for a full 14 horizon
analysis, proves the effectiveness of the usage of symbolic
execution at reducing the state space size.
Figure 6 shows a sample generated execution graph for
the Assembly
Way case
study
with
a model checking bound
Systems
and Internet Infrastructure
Security
Laboratory
(SIIS)
1000"
ber'of'States'
0.001$
100"
Page 50
Related Work
n
tio
De
tec
cks
Blo
ter
s
un
ter
s
X
X
X
X
ta
Tim
ers
Lo
gic
Ed
ge
X
X
X
Ne
ste
d
Co
n
me
ric
X
X
Da
X
X
X
X
Po
in
X
X
Nu
En
um
Lo
gi
ole
Bo
X
X
X
X
X
X
X
Co
SAT
SAT
Thm
Thm
Mod
Mod
-
an
h
Ap
pro
ac
Park et al. [22]
Groote et al. [14]
Homer [15]
Biha [21]
SABOT [18]
Canet et al. [6]
TSV
d.
Br
an
chi
ng
Fu
nct
i on
Blo
cks
MC
R
C OMPARISON OF ANALYZED FEATURES WITH RELATED WORK . R ELATED APPROACHES ARE ABBREVIATED : SAT=SAT S OLV
T HM =T HEOREM P ROVING , M OD =M ODEL C HECKING
c
E I.
X
X
X
X
X
X
X
tems, distributed control systems, and PLCs. Such gu
are also used in the energy industry [20], [32]. It has, h
been argued that compliance with these standards can
a false sense of security [24], [33].
Systems and Internet Infrastructure Security Laboratory (SIIS)
There have also been efforts to build novel securit
anisms for control systems. Mohan et al. [19] intro
monitor that dynamically checks the safety of Page
plant
51 b
Related Work
No efficient reduction
n
tio
De
tec
cks
Blo
ter
s
un
ter
s
X
X
X
X
ta
Tim
ers
Lo
gic
Ed
ge
X
X
X
Ne
ste
d
Co
n
me
ric
X
X
Da
X
X
X
X
Po
in
X
X
Nu
En
um
Lo
gi
ole
Bo
X
X
X
X
X
X
X
Co
SAT
SAT
Thm
Thm
Mod
Mod
-
an
h
Ap
pro
ac
Park et al. [22]
Groote et al. [14]
Homer [15]
Biha [21]
SABOT [18]
Canet et al. [6]
TSV
d.
Br
an
chi
ng
Fu
nct
i on
Blo
cks
MC
R
C OMPARISON OF ANALYZED FEATURES WITH RELATED WORK . R ELATED APPROACHES ARE ABBREVIATED : SAT=SAT S OLV
T HM =T HEOREM P ROVING , M OD =M ODEL C HECKING
c
E I.
X
X
X
X
X
X
X
tems, distributed control systems, and PLCs. Such gu
are also used in the energy industry [20], [32]. It has, h
been argued that compliance with these standards can
a false sense of security [24], [33].
Systems and Internet Infrastructure Security Laboratory (SIIS)
There have also been efforts to build novel securit
anisms for control systems. Mohan et al. [19] intro
monitor that dynamically checks the safety of Page
plant
52 b
Related Work
Hard to formalize IL instructions with side-effects
n
tio
De
tec
cks
Blo
ter
s
un
ter
s
X
X
X
X
ta
Tim
ers
Lo
gic
Ed
ge
X
X
X
Ne
ste
d
Co
n
me
ric
X
X
Da
X
X
X
X
Po
in
X
X
Nu
En
um
Lo
gi
ole
Bo
X
X
X
X
X
X
X
Co
SAT
SAT
Thm
Thm
Mod
Mod
-
an
h
Ap
pro
ac
Park et al. [22]
Groote et al. [14]
Homer [15]
Biha [21]
SABOT [18]
Canet et al. [6]
TSV
d.
Br
an
chi
ng
Fu
nct
i on
Blo
cks
MC
R
C OMPARISON OF ANALYZED FEATURES WITH RELATED WORK . R ELATED APPROACHES ARE ABBREVIATED : SAT=SAT S OLV
T HM =T HEOREM P ROVING , M OD =M ODEL C HECKING
c
E I.
X
X
X
X
X
X
X
tems, distributed control systems, and PLCs. Such gu
are also used in the energy industry [20], [32]. It has, h
been argued that compliance with these standards can
a false sense of security [24], [33].
Systems and Internet Infrastructure Security Laboratory (SIIS)
There have also been efforts to build novel securit
anisms for control systems. Mohan et al. [19] intro
monitor that dynamically checks the safety of Page
plant
53 b
Related Work
No symbolic state lumping
n
tio
De
tec
cks
Blo
ter
s
un
ter
s
X
X
X
X
ta
Tim
ers
Lo
gic
Ed
ge
X
X
X
Ne
ste
d
Co
n
me
ric
X
X
Da
X
X
X
X
Po
in
X
X
Nu
En
um
Lo
gi
ole
Bo
X
X
X
X
X
X
X
Co
SAT
SAT
Thm
Thm
Mod
Mod
-
an
h
Ap
pro
ac
Park et al. [22]
Groote et al. [14]
Homer [15]
Biha [21]
SABOT [18]
Canet et al. [6]
TSV
d.
Br
an
chi
ng
Fu
nct
i on
Blo
cks
MC
R
C OMPARISON OF ANALYZED FEATURES WITH RELATED WORK . R ELATED APPROACHES ARE ABBREVIATED : SAT=SAT S OLV
T HM =T HEOREM P ROVING , M OD =M ODEL C HECKING
c
E I.
X
X
X
X
X
X
X
tems, distributed control systems, and PLCs. Such gu
are also used in the energy industry [20], [32]. It has, h
been argued that compliance with these standards can
a false sense of security [24], [33].
Systems and Internet Infrastructure Security Laboratory (SIIS)
There have also been efforts to build novel securit
anisms for control systems. Mohan et al. [19] intro
monitor that dynamically checks the safety of Page
plant
54 b
Thanks!
Steve: [email protected]
Saman: [email protected]
???
Systems and Internet Infrastructure Security Laboratory (SIIS)
Page 55

Seminarkalender 2015

3rd February 2015 Dear shareholder, RE: Notice of General Meeting

MAXWELL ACADEMY PVT. LTD.

In ndexe ed Ir ish E Equit ty Fu und S Series s H

For personal use only

Released : 26 Jun 2014 RNS Number : 6506K Lamprell plc 26 June

FACTSHEET - Solactive European High Dividend Low Volatility

IndraLogic L Controller-based

Download Full Text - International Journal of Science, Engineering

ATLAS Max-RTL

Abalone withering syndrome: distribution, impacts, current