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
© Copyright 2025 ExpyDoc