Towards Secure, Privacy-Preserving, Verifiable Cyberphysical Systems

For this project, we are building tools and verification techniques that check modern cyberphysical systems (CPSs) and Internet of Things (IoT) systems for correctness in order to decrease the likelihood of behavior that may lead to various vulnerabilities, including those related to security.   In particular, we intend to create a suite of verification tools for design-time, compile-time, and run-time checking of these systems.  Some of these tools will be software-oriented, but others will explore hardware-support for checking correct execution of deployed systems.  As part of this work, we intend to also examine the correctness of existing CPS/IoT systems, including the software designed for these systems and the underlying functioning of these platforms.  During the first year of this project, we have been developing a suite of litmus tests and corresponding testing framework to stress and verify the correctness of consistency guarantees in real IoT platforms.  Additionally, we created a static analysis tool to evaluate the correctness of real applications created for home IoT platforms.