Abstract
The security and resiliency analysis of a smart grid needs to consider the target component(s), flexible attack model, and the integration among different smart grid components and attack properties. An exhaustive security analysis is not only expensive but also infeasible using testbeds. Formal analytics can play an important role toward comprehensive security analysis of the system, which can identify potential threats provably, that can further be verified on testbeds.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
M.Q. Ali, E. Al-Shaer, Randomization-based intrusion detection system for advanced metering infrastructure*. ACM Trans. Inf. Syst. Secur. 18 (2), 1–30 (2015)
E. Al-Shaer et al., Network configuration in a box: towards end-to-end verification of network reachability and security, in IEEE International Conference on Network Protocols (ICNP), NY (2009), pp. 107–116
C. Baier, J.P. Katoen, Principles of Model Checking (The MIT Press, Cambridge, 2008)
P. Bera, S. Ghosh, P. Dasgupta, Policy based security analysis in enterprise networks: a formal approach. IEEE Trans. Netw. Serv. Manage. 7 (4), 231–243 (2010)
N. Bjørner, L. Moura, Z310: applications, enablers, challenges and directions, in International Workshop on Constraints in Formal Verification (2009)
E.M. Clarke, O. Grumberg, D. Peled (eds.), Model Checking (MIT Press, Cambridge, 1999)
L. de Moura, N. Bjørner, Satisfiability modulo theories: an appetizer, in Brazilian Symposium on Formal Methods (2009)
A.D. Gordon et al., Probabilistic programming, in the 36th International Conference on Software Engineering, Hyderabad (2014), pp. 167–181
Guide to Industrial Control Systems (ICS) Security, NIST Special Publication 800-82 (Revision 1) (2013), http://dx.doi.org/10.6028/NIST.SP.800-82r1
D. Knuth, A. Yao, The complexity of nonuniform random number generation, in Algorithms and Complexity: New Directions and Recent Results (Academic Press, New York, 1976)
M. Kwiatkowska, Probabilistic model checking with PRISM: an overview (2015), http://qav.comlab.ox.ac.uk/papers/acmper_prismperf.pdf
M. Kwiatkowska, G. Norman, D. Parker, Stochastic model checking, in the 7th International Conference on Formal Methods for Performance Evaluation, Bertinoro (2007), pp. 220–270
M.W. Moskewicz et al., Chaff: engineering an efficient SAT solver, in Annual ACM IEEE Design Automation Conference (2001)
R. Nieuwenhuis, A. Oliveras, On SAT modulo theories and optimization problems, in Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 4121 (Springer, New York, 2006), pp. 156–169
NISTIR 7628: Guidelines for Smart Grid Cyber Security, Smart Grid Inter-Operability Panel- Cyber Security Working Group (2010), http://www.nist.gov/smartgrid/upload/nistir-7628_total.pdf
North American Electric Reliability Corporation, Comments of the North American Electric Reliability Corporation in Response to NIST Smart Grid Cyber Security Strategy and Requirements (Draft NISTIR 7628) (2009)
North-American Electric Reliability Corporation, Critical Infrastructure Protection (CIP) Standards (2015), http://www.nerc.com/pa/Stand/Pages/CIPStandards.aspx. Accessed 2015
Probabilistic Symbolic Model Checker, PRISM (2015), http://www.prismmodelchecker.org/. Accessed 2015
M.A. Rahman, E. Al-Shaer, P. Bera, SmartAnalyzer: a noninvasive security threat analyzer for AMI smart grid, in 31st IEEE International Conference on Computer Communications (INFOCOM) (2012), pp. 2255–2263
M.A. Rahman, E. Al-Shaer, Md. Rahman, A formal model for verifying stealthy attacks on state estimation in power grids, in IEEE International Conference on Smart Grid Communications, October 2013
M.A. Rahman, E. Al-Shaer, P. Bera, A noninvasive threat analyzer for advanced metering infrastructure in smart grid. IEEE Trans. Smart Grid 4 (1), 273–287 (2013)
M.A. Rahman, E. Al-Shaer, R. Kavasseri, A formal model for verifying the impact of stealthy attacks on optimal power flow in power grids, in ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), April 2014
M.A. Rahman, E. Al-Shaer, R. Kavasseri, Security threat analytics and countermeasure synthesis for state estimation in smart power grids, in IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), June 2014
M.A. Rahman, E. Al-Shaer, R. Kavasseri, Impact analysis of topology poisoning attacks on economic operation of the smart power grid, in IEEE 34th International Conference on Distributed Computing Systems (ICDCS), June 2014, pp. 649–659
M.A. Rahman, E. Al-Shaer, R.B. Bobba, Moving target defense for hardening the security of the power system state estimation, in The First ACM Workshop on Moving Target Defense (MTD), Scottsdale (2014), pp. 59–68
M.A. Rahman, A. Jakaria, E. Al-Shaer, Formal analysis for dependable supervisory control and data acquisition in smart grids, in IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). June 2016
Recommended Security Controls for Federal Information Systems and Organizations, NIST special publication 800-53 (Revision 4) (2013), http://dx.doi.org/10.6028/NIST.SP.800-53r4
The Die Example (2015), http://www.prismmodelchecker.org/tutorial/die.php. Accessed 2015
Z3 @ rise4fun from Microsoft, Microsoft research (2015), http://rise4fun.com/z3. Accessed 2015
The Z3 Theorem Prover, Microsoft research, https://github.com/Z3Prover/z3/wiki
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Al-Shaer, E., Rahman, M.A. (2016). Analytics for Smart Grid Security and Resiliency. In: Security and Resiliency Analytics for Smart Grids. Advances in Information Security, vol 67. Springer, Cham. https://doi.org/10.1007/978-3-319-32871-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-32871-3_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-32870-6
Online ISBN: 978-3-319-32871-3
eBook Packages: Computer ScienceComputer Science (R0)