Biblio

Industrial control systems are changing from monolithic to distributed and interconnected architectures, entering the era of industrial IoT. One fundamental issue is that security properties of such distributed control systems are typically only verified empirically, during development and after system deployment. We propose a novel modelling framework for the security verification of distributed industrial control systems, with the goal of moving towards early design stage formal verification. In our framework we model industrial IoT infrastructures, attack patterns, and mitigation strategies for countering attacks. We conduct model checking-based formal analysis of system security through scenario execution, where the analysed system is exposed to attacks and implement mitigation strategies. We study the applicability of our framework for large systems using a scalability analysis.

The proliferation of Internet-of-Things (IoT) devices within homes raises many security and privacy concerns. Recent headlines highlight the lack of effective security mechanisms in IoT devices. Security threats in IoT arise not only from vulnerabilities in individual devices but also from the composition of devices in unanticipated ways and the ability of devices to interact through both cyber and physical channels. Existing approaches provide methods for monitoring cyber interactions between devices but fail to consider possible physical interactions. To overcome this challenge, it is essential that security assessments of IoT networks take a holistic view of the network and treat it as a "system of systems", in which security is defined, not solely by the individual systems, but also by the interactions and trust dependencies between systems. In this paper, we propose a way of modeling cyber and physical interactions between IoT devices of a given network. By verifying the cyber and physical interactions against user-defined policies, our model can identify unexpected chains of events that may be harmful. It can also be applied to determine the impact of the addition (or removal) of a device into an existing network with respect to dangerous device interactions. We demonstrate the viability of our approach by instantiating our model using Alloy, a language and tool for relational models. In our evaluation, we considered three realistic IoT use cases and demonstrate that our model is capable of identifying potentially dangerous device interactions. We also measure the performance of our approach with respect to the CPU runtime and memory consumption of the Alloy model finder, and show that it is acceptable for smart-home IoT networks.