Development of Verified Message Encoder/Decoder for Automotive V2V Communications
Presented as part of the 2017 HCSS conference.
ABSTRACT
The National Highway Traffic Safety Administration (NHTSA) Vehicle-to-Vehicle (V2V) communications proposal would enable V2V communications between automobiles, enabling a multitude of new crash-avoidance applications that, once fully deployed, could prevent hundreds of thousands of crashes every year. V2V messages are sent between vehicles using DSRC (Dedicated Short Range Communications), a two-way short- to- medium-range communications technology.
The addition of hardware and software for handling DSRC and V2V protocols clearly increases the attack surface of the vehicle. Ensuring that this software is free of vulnerabilities is paramount. (Both academic work and hobbyist demonstrations have shown the possibility of automobiles being hacked using vulnerabilities of other vehicle interfaces).
Galois has just completed a pilot project for NHTSA in which we generated mathematically verified C code, verifying both functional correctness and safety properties. We built high-assurance, mathematically verified decoders and encoders for the SAE J2735 Basic Safety Message (BSM) that are low-cost, reproducible, and reconfigurable (i.e., easily generating new proofs for additional functionality). A full proof was generated for the C code that encodes and decodes Part I (the non optional data) of the BSM.
Our project leveraged two tools that Galois previously built for the U.S. Government: the High-Assurance ASN.1 Workbench (HAAW) and the Software Analysis Workbench (SAW). In this talk we will discuss (1) some of the correct-by-construction features of our ASN.1 compiler and (2) the challenges and results of applying our SAW verification tool to the V2V encoder/decoder routines.
--
Dr. Mark Tullsen has been a research engineer at Galois for over 15 years. His research interests are functional programming, programming languages, compilers, domain specific languages, and security. He has been the Principle Investigator on a variety of Galois projects such as DETerrence (detecting malicious hardware), PICT (software development tools for capturing design intentions), FLAIR (mapping functional array languages to novel parallel architectures), and the Vehicle-To-Vehicle verification work presented here.
Dr. Tullsen received a Ph.D. in Computer Science from Yale University and a B.S. in Electrical Engineering & Computer Science from U.C. Berkeley.