|
|
|
1 Smart Grids and Security Challenges |
|
|
3 | (12) |
|
|
4 | (1) |
|
|
5 | (2) |
|
|
7 | (2) |
|
|
9 | (1) |
|
1.5 Security Goals and Challenges |
|
|
10 | (2) |
|
|
11 | (1) |
|
|
11 | (1) |
|
|
12 | (3) |
|
|
12 | (3) |
|
2 Analytics for Smart Grid Security and Resiliency |
|
|
15 | (14) |
|
|
15 | (2) |
|
2.2 Technical Approach Overview |
|
|
17 | (3) |
|
2.2.1 Security Analytics for AMI and SCADA |
|
|
17 | (1) |
|
2.2.2 Security Analytics for EMS Modules |
|
|
18 | (1) |
|
2.2.3 Intrusion Detection Systems for AMI |
|
|
19 | (1) |
|
2.3 Overview of SMT and Probabilistic Model Checking |
|
|
20 | (4) |
|
2.3.1 Satisfiability Modulo Theories |
|
|
20 | (1) |
|
2.3.2 Probabilistic Model Checking |
|
|
21 | (3) |
|
|
24 | (5) |
|
|
25 | (4) |
|
Part II Formal Analytics for Secure and Resilient Smart Grids |
|
|
|
3 Security Analytics for AMI and SCADA |
|
|
29 | (32) |
|
3.1 Overview of the Security Analysis Framework |
|
|
30 | (1) |
|
3.2 AMI Security Analysis |
|
|
31 | (13) |
|
|
31 | (1) |
|
3.2.2 Formal Model of AMI Security Verification |
|
|
32 | (7) |
|
|
39 | (5) |
|
3.3 SCADA Security Analysis |
|
|
44 | (11) |
|
|
44 | (1) |
|
3.3.2 Formal Model of SCADA Security Verification |
|
|
45 | (8) |
|
|
53 | (2) |
|
3.4 Scalability of the Security Analysis Framework |
|
|
55 | (3) |
|
3.4.1 Time Complexity Analysis |
|
|
55 | (2) |
|
3.4.2 Memory Complexity Analysis |
|
|
57 | (1) |
|
3.4.3 Time Complexity in Unsatisfied Cases |
|
|
57 | (1) |
|
|
58 | (3) |
|
|
59 | (2) |
|
4 Security Analytics for EMS Modules |
|
|
61 | (44) |
|
|
62 | (4) |
|
|
62 | (1) |
|
|
63 | (1) |
|
|
63 | (1) |
|
|
64 | (1) |
|
|
64 | (1) |
|
|
65 | (1) |
|
4.2 Stealthy Attack Verification |
|
|
66 | (10) |
|
4.2.1 Formalizations of Power Flow Equations |
|
|
66 | (2) |
|
4.2.2 Formalization of Change in State Estimation |
|
|
68 | (1) |
|
4.2.3 Formalization of Topology Change |
|
|
68 | (2) |
|
4.2.4 Formalization of False Data Injection to Measurements |
|
|
70 | (1) |
|
4.2.5 Formalization of Attack Attributes |
|
|
70 | (2) |
|
4.2.6 An Example Case Study |
|
|
72 | (4) |
|
4.3 Impact Analysis of Stealthy Attacks |
|
|
76 | (6) |
|
4.3.1 Impact Analysis Framework Design |
|
|
76 | (2) |
|
4.3.2 Formalization of Optimal Power Flow |
|
|
78 | (1) |
|
4.3.3 Formalization of Attack Impact on OPF |
|
|
79 | (1) |
|
4.3.4 An Example Case Study |
|
|
80 | (2) |
|
4.4 Security Hardening Against Stealthy Attacks |
|
|
82 | (5) |
|
|
82 | (2) |
|
4.4.2 Formalization of Candidate Architecture Selection |
|
|
84 | (1) |
|
4.4.3 An Example Case Study |
|
|
85 | (2) |
|
4.5 Proactive Defense Against Persistent Attacks |
|
|
87 | (8) |
|
4.5.1 Moving Target Defense Strategy |
|
|
87 | (2) |
|
4.5.2 Formal Model for Strategy Selection |
|
|
89 | (3) |
|
4.5.3 An Example Case Study |
|
|
92 | (3) |
|
|
95 | (7) |
|
|
95 | (1) |
|
4.6.2 Time Complexity of Verification Model |
|
|
95 | (2) |
|
4.6.3 Time Complexity of Impact Analysis |
|
|
97 | (2) |
|
4.6.4 Time Complexity of Synthesis Mechanism |
|
|
99 | (2) |
|
4.6.5 Time Complexity of MTD Strategy Selection Models |
|
|
101 | (1) |
|
|
101 | (1) |
|
|
102 | (3) |
|
|
103 | (2) |
|
5 Intrusion Detection Systems for AMI |
|
|
105 | (30) |
|
|
106 | (1) |
|
|
107 | (1) |
|
5.3 Statistical Analysis and Motivation |
|
|
108 | (5) |
|
|
113 | (7) |
|
|
113 | (2) |
|
5.4.2 Properties Specification for Model Checking |
|
|
115 | (2) |
|
5.4.3 Randomization Module |
|
|
117 | (3) |
|
|
120 | (12) |
|
|
121 | (1) |
|
5.5.2 Robustness Against Evasion and Mimicry Attacks |
|
|
122 | (3) |
|
5.5.3 Accuracy Evaluation |
|
|
125 | (5) |
|
|
130 | (2) |
|
|
132 | (1) |
|
|
132 | (3) |
|
|
133 | (2) |
|
A Resiliency Threat Analysis for SCADA |
|
|
135 | (6) |
|
A.1 k-Resilient Secured Observability Threat Model |
|
|
135 | (3) |
|
|
138 | (3) |
Index |
|
141 | |