Title :
Probabilistic model checking for AMI intrusion detection
Author :
Ali, Muhammad Qasim ; Al-Shaer, Ehab
Author_Institution :
Dept. of Software & Inf. Syst., Univ. of North Carolina Charlotte, Charlotte, NC, USA
Abstract :
Smart grids provide bi-directional communication between smart meters at user premises and utility provider for the purpose of efficient energy management through Advanced Metering Infrastructure (AMI). Recent studies have shown that the potential threats targeting AMI are significant. Despite the need of developing intrusion detection systems (IDS) tailored for the smart grid [4], very limited progress has been made in this area so far. Unlike traditional networks, smart grid has its unique challenges, such as limited computational power devices and potentially high deployment cost, which restrict the deployment options of intrusion detectors. However, smart grid exhibits behavior that can be accurately modeled based on its configuration, which can be exploited to design efficient intrusion detectors. In this paper, we show that AMI behavior can be modeled using event logs collected at smart collectors, which in turn can be verified using the specifications invariant generated from the configurations of the AMI devices. We model the AMI behavior using the fourth order Markov chain and the stochastic model is then probabilistically verified using specifications written in Linear Temporal Logic. Our model is capable of detecting malicious behavior in the AMI network due to intrusions or device malfunctioning. We validate our approach on a real-world dataset of thousands of meters collected at the AMI of a leading utility provider.
Keywords :
Markov processes; energy management systems; power engineering computing; safety systems; smart meters; smart power grids; temporal logic; AMI; IDS; advanced metering infrastructure; bidirectional communication; device malfunctioning; energy management; event log collection; fourth order Markov chain; intrusion detection systems; linear temporal logic; malicious behavior detection; probabilistic model checking; real-world dataset; smart collectors; smart grids; smart meters; stochastic model; user premises; utility provider; Accuracy; Correlation; Entropy; Markov processes; Monitoring; Smart grids;
Conference_Titel :
Smart Grid Communications (SmartGridComm), 2013 IEEE International Conference on
Conference_Location :
Vancouver, BC
DOI :
10.1109/SmartGridComm.2013.6688002