Security Software for Autonomous Vehicles
Proof assistants are a programming technique for writing trustworthy software in which the programmer writes not only the program code but also a mathematical proof of the code’s correctness. An automated proof checker can then either verify that the code is correct or show where the proof is wrong.
Ross A. Knepper and J. Gregory Morrisett, Computer Science, are working to design this software assurance for autonomous vehicles (AVs), which are complex cyberphysical systems (CPS). Examples of these systems include self-driving cars, automated drones for inspection and surveillance, and rescue robots for disaster recovery.
Programs that interact with the real world through sensors and actuators must make many assumptions about noisy sensors, physics, human users, and other circumstances that cannot be controlled by the program. Knepper and Morrisett propose the development of three tools to implement and prove complex AV codes correct for noisy, real-world operations. These tools equip AVs to handle increasingly complex interactions. The project will lead to advances in software assurance of many kinds of AVs and multi-CPS systems and will enable the building of all kinds of safe AVs for real-world deployment, even under adverse conditions. Inter-operability of diverse AV systems will also be improved, which will aid in coordination, for example among first-responders.