A declarative logic-based approach for threat analysis of advanced metering infrastructure

The Advanced Metering Infrastructure (AMI) is the core component in a smart grid. It exhibits highly complex heterogeneous network configurations comprising of different cyber-physical components. These components are interconnected through different communication media, protocols, and secure tunnels, and are operated using different modes of data delivery and security policies. The inherent complexity and heterogeneity in AMI significantly increase the potential of security threats due to misconfiguration or attacks, which can cause devastating damage to AMI. Therefore, creating a formal model that can represent the global behavior based on AMI configuration is evidently essential to verify, evaluate and harden its capabilities against dormant security threats. In this paper, we present a novel declarative logic approach for analyzing AMI configurations against various security threats. We develop a tool, called AMISecChecker, which offers manifold contributions: (i) modeling of AMI components' configurations and their interactions based on property level abstraction; (ii) modeling of AMI topology and communication properties; and (iii) verifying the compliance of AMI configuration with security control guidelines. The efficacy and scalability of the tool have been evaluated in real and synthetic test networks.