Abstract
Vehicle-to-Vehicle (V2V) communications is a “connected vehicles” standard that will likely be mandated in the U.S. within the coming decade. V2V, in which automobiles broadcast to one another, promises improved safety by providing collision warnings, but it also poses a security risk. At the heart of V2V is the communication messaging system, specified in SAE J2735 using the Abstract Syntax Notation One (ASN.1) data-description language. Motivated by numerous previous ASN.1 related vulnerabilities, we present the formal verification of an ASN.1 encode/decode pair. We describe how we generate the implementation in C using our ASN.1 compiler. We define self-consistency for encode/decode pairs that approximates functional correctness without requiring a formal specification of ASN.1. We then verify self-consistency and memory safety using symbolic simulation via the Software Analysis Workbench.
Author supplied keywords
Cite
CITATION STYLE
Tullsen, M., Pike, L., Collins, N., & Tomb, A. (2018). Formal verification of a vehicle-to-vehicle (V2V) messaging system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10982 LNCS, pp. 413–429). Springer Verlag. https://doi.org/10.1007/978-3-319-96142-2_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
