Formal Modeling for Automated Security Analytics fo the Internet of Things

Abstract

The Internet of Things (IoT) has given us a notion of a smartly connected world, being driven by a network of embedded devices or “things”; observing, interacting and implementing feature(s) with minimal human intervention. The concept has received a wide acceptance and an express proliferation, giving birth to promising applications in all technological domains, ranging from common home and personal appliances to sophisticated and safety-critical systems. This explosive IoT growth, while promising a variety of innovative solutions and business benefits, has also raised serious security concerns, as also evident from a rising trend of IoT security-breach incidents. The embryonic IoT systems are composed of resource-starving devices, having diverse capabilities, cascaded functional dependencies, complex digital-to-physical couplings and, communicate using heterogeneous non-standardized protocols. These unique IoT security challenges are harboring a formidable threat-landscape, thus giving birth to a rich set of unrevealed attack techniques. Consequently, the traditional cyber-oriented methods fall short of perceiving and analyzing the IoT-specific security configurations and applicable attack vectors. This thesis applies the strengths of formal methods to plan, analyze, verify and strengthen the security of modern-day IoT systems, by systematically capturing their complex dependencies. Formal methods are well-established and time-tested techniques, employed to model complex systems as mathematical entities, and then use those models for rigorous mathematical analysis. Since these techniques are rooted to a strong mathematical foundation, they can be used to formally specify system descriptions, automatically analyze (or verify) those descriptions and also derive new descriptions, consistent with the reference model. The scope of this thesis is to use suitable formal techniques to (1) develop reusable models for generic IoT system and security specifications, and encode them using appropriate formalisms, (2) evaluate IoT systemlevel security configurations to automatically arrest mis-configurations, (3) formally model IoT-specific threats and analyze their applicability, beiii iv havior, probable paths (techniques) and suitable countermeasures for a given IoT-system configuration and, (4) precisely quantify and exhaustively verify the risks likelihoods for system-level IoT threats. The solutions proposed by the thesis are grouped under three formal frameworks, namely IoTChecker, IoTSAT and IoTRiskAnalyzer. Each of these frameworks serves to achieve unique yet complimentary thesis goals and are based on appropriate formal languages, suiting those goals. More specifically, the thesis employs ontologies, Satisfiability Modulo Theories (SMT) and probabilistic model checking, respectively, to develop these frameworks. The efficacy of the proposed approach is evaluated against real-world IoT products and their practically deployed system-level configurations. The formal models and automated analysis techniques, developed during this thesis, proved efficient and effective in pin-pointing subtle security mis-configurations, identifying unknown threat techniques and, ranking system-level configurations on the basis of quantitatively verified risk exposures. Consequently, the thesis offers generic, automation-driven and formally-glued IoT security models, which can be reused and extended to comprehend IoT system-level security, scrutinize IoT-specific threat propagation patterns, isolate the weakest security link(s) and, accordingly rationalize the security spendings.