Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
| العنوان: | Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System |
|---|---|
| المؤلفون: | Aaron Tomb, Lee Pike, Mark Tullsen, Nathan Collins |
| المصدر: | Computer Aided Verification ISBN: 9783319961415 CAV (2) |
| بيانات النشر: | Springer International Publishing, 2018. |
| سنة النشر: | 2018 |
| مصطلحات موضوعية: | Correctness, Computer science, Programming language, computer.internet_protocol, Symbolic simulation, 020206 networking & telecommunications, Data_CODINGANDINFORMATIONTHEORY, 02 engineering and technology, computer.software_genre, Symbolic execution, Formal specification, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Compiler, Abstract Syntax Notation One, computer, Memory safety, Formal verification |
| الوصف: | 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. |
| ردمك: | 978-3-319-96141-5 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_________::9b705a8833c80b494356566d356e963a https://doi.org/10.1007/978-3-319-96142-2_25 |
| حقوق: | OPEN |
| رقم الأكسشن: | edsair.doi...........9b705a8833c80b494356566d356e963a |
| قاعدة البيانات: | OpenAIRE |
| ردمك: | 9783319961415 |
|---|