Novel Formal Methods for the Safety and Security of Cyber-Physical Systems

Abstract

The ongoing digital revolution is now augmenting physical processes with embedded controllers. This results in Cyber-Physical Systems (CPSs), where the physical and cyber worlds become one integrated system. There is a growing group of emerging industries (Internet of Things (IoT) devices, Unmanned Aerial Vehicles (UAVs), and 3D printers) that fall into grey areas where regulations may be lacking, and industry practice is inconsistent. Robust methods in the field of formal runtime assurance can be used to verify safety and security policies. They have lower resource overheads than traditional formal methods, appealing to designers with resource constraints. Runtime verification, an area within runtime assurance, verifies policies during the system’s execution and produces alerts if a policy is violated. For example, a smart watch alerting if it detects abnormal heart rhythm. For CPSs with the ability to take action, runtime enforcement is well suited to ensure safety and security policies are upheld. Runtime enforcement extends runtime verification with the ability to intervene before a violation occurs (important for safety critical systems where failure may cause loss of life). Existing runtime enforcement work has not considered the attacker’s perspective, which can undermine defensive strategies. Additionally, as CPSs become more capable, the need for scalable enforcement of multiple policies grows. This thesis presents a set of novel runtime assurance methods using runtime verification and runtime enforcement to verify safety and security. Firstly, we present formal models of abnormal heart rhythms detectable in Electrocardiograms (ECGs). Our approach has comparable performance to existing methods with the benefit of producing clinically explainable alerts. Secondly, we propose enforcer interchange to orchestrate sophisticated runtime enforcer attacks. We model a set of attacks on UAV communication and successfully launch these on a high fidelity drone simulator. Thirdly, we present a framework to compose runtime enforcers in parallel to defend against attacks on complex CPSs. We demonstrate improved scalability with (a set of) defensive policies for a 3D printer. In a constantly evolving technological landscape, designers are creating more capable CPSs. We present the aforementioned approaches to aid designers in the pursuit of safety and security.