Collaborative Research: CSR: VERITAS: Secure Vehicular Systems through Intelligent Information Flow Verification

Modern vehicles rely on small computers, sensors, and software that constantly share information with one another to support driving, navigation, safety, and passenger services. As vehicles become increasingly connected and autonomous, unintended information flows can create security vulnerabilities that threaten both safety and reliability. This project will develop technologies for identifying, monitoring, and verifying information flows among vehicle components, helping ensure that critical functions remain protected even when individual subsystems are compromised. This makes everyday driving safer for ordinary people and helps keep cars working the way drivers expect. By enabling engineers to detect and address vulnerabilities earlier in the design process, the research will contribute to safer, more secure, and more trustworthy transportation systems. The project will develop a scientific foundation for information flow verification in complex vehicular systems through three integrated research thrusts. The first thrust will create a configurable digital twin platform that combines physical vehicle dynamics with customizable hardware, software, sensing, and communication components to explore realistic operating scenarios and automatically extract information flow requirements. The second thrust will develop scalable verification methods that combine formal verification, compositional reasoning, abstraction refinement, reinforcement learning, and large language models to analyze system-level information flows. The third thrust will evaluate these methods through a progression from synthetic benchmarks to realistic case studies. Together, these advances will establish new foundations for automated verification of large-scale cyber-physical systems. The project will generate publicly available datasets, benchmarks, formal specifications, software tools, and collections of real-world information flow vulnerabilities to support future research and education. The resulting methods will benefit not only transportation systems but also other critical infrastructures that rely on coordinated sensing, computation, communication, and control, including industrial automation, electric power systems, and smart city technologies. Research outcomes will be disseminated through open-source releases, publications, tutorials, workshops, and community outreach activities. Educational activities will integrate project results into university courses, undergraduate research, and workforce training programs, helping prepare future engineers with expertise in vehicle security, formal verification, artificial intelligence, and trustworthy cyber-physical systems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.