Probabilistic model checking for AMI intrusion detection

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.