Safety Assurance of Cyber-Physical Systems Through Secure and Verifiable Information Flow Control

Abstract:

Today's cyber-physical systems such as cars and airplanes are rapidly transforming into complex, networked computing systems that electronically control physical systems. Unfortunately, the increased complexity often leads to bugs and security vulnerabilities, and the network connectivity opens up these vulnerable systems to remote software attacks. In order to address the increasing security concern, this project aims to develop mechanisms and tools to provide provable security assurance for safety-critical functions of cyber-physical systems. In particular, the project studies an autonomous vehicle as a primary example, and develops techniques that enable designers to obtain a quantitative guarantee for collision avoidance even when parts of the system cannot be trusted. The intellectual merits include designing architecture that ensures safety-critical functions are not maliciously affected by untrusted parts, developing verification methods to prove security properties of both hardware and software, and developing and analyzing collision avoidance algorithms and their safety assurance. The project's broader significance and importance include its societal impact on enabling provably secure safety-critical cyber-physical systems as well as its educational activities that will train a new generation of scientists and engineers who are capable of operating across multiple disciplines. To achieve its goal, this project takes an integrated approach to co-design all major components of a system, including hardware, software, and safety-critical control algorithms, through synergistic collaborations across multiple disciplines. The project re-designs hardware architecture and software programs in order to tightly control untrusted information flows including timing interference. The information flow properties of both hardware and software are verified at design time using novel security type systems. This new hardware/software foundation ensures that safety-critical control operations are based on trustworthy information flows and cannot be affected by untrusted information from potentially malicious sources such as the Internet. At the same time, the project co-develops collision avoidance algorithms and analyzes their safety assurance properties by leveraging the information flow guarantees from the underlying hardware/software platform. Overall, this project is expected to provide a new foundation for building cyber-physical systems with strong and verifiable safety assurance.