This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring
Technical Paper
2016-01-0126
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
The Runtime Verification ECU (RV-ECU) is a new development platform for checking and enforcing the safety of automotive bus communications and software systems. RV-ECU uses runtime verification, a formal analysis subfield geared at validating and verifying systems as they run, to ensure that all manufacturer and third-party safety specifications are complied with during the operation of the vehicle. By compiling formal safety properties into code using a certifying compiler, the RV-ECU executes only provably correct code that checks for safety violations as the system runs. RV-ECU can also recover from violations of these properties, either by itself in simple cases or together with safe message-sending libraries implementable on third-party control units on the bus. RV-ECU can be updated with new specifications after a vehicle is released, enhancing the safety of vehicles that have already been sold and deployed.
Currently a prototype, RV-ECU is meant to eventually be deployed as global and local ECU safety monitors, ultimately responsible for the safety of the entire vehicle system. We describe its overall architecture and implementation, and demonstrate monitoring of safety specifications on the CAN bus. We use past automotive recalls as case studies to demonstrate the potential of updating the RV-ECU as a cost effective and practical alternative to software recalls, while requiring the development of rigorous, formal safety specifications easily sharable across manufacturers, OEMs, regulatory agencies and even car owners.
Recommended Content
Authors
Citation
Daian, P., Shiraishi, S., Iwai, A., Manja, B. et al., "RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring," SAE Technical Paper 2016-01-0126, 2016, https://doi.org/10.4271/2016-01-0126.Also In
References
- Charette Robert N This car runs on code IEEE Spectrum 46.3 2009 3
- Shiraishi Shinichi and Abe Mutsumi Automotive system development based on collaborative modeling using multiple adls ESEC/FSE 2011 (Industial Track) 2011
- Vellequette Larry P. Fiat Chrysler recalls 1.4 million vehicles to install anti-hacking software http : / / www . autonews . com / article /20150724/OEM11/150729921/fiat-chryslerrecalls - 1 . 4 - million - vehicles - to -install-anti-hacking
- Hetzner Christiaan VW ordered to recall 2.4 million cars in Germany with cheat software http : / / www . autonews . com / article / 20151015 / COPY01 / 310159986 / vw - ordered -to-recall-2-4-million-cars-in-germanywith-cheat-software
- Reuters Toyota recalls 625,000 cars over software malfunction http : / / www . dw . com / en / toyota - recalls - 625000 - cars - over -software-malfunction/a-18585121
- Associated Press Ford Recalls 432,000 Cars Over Software Problem http : / / www . dailyfinance . com / 2015 / 07 / 02 / ford -recalls-cars-software-problem/
- Associated Press Honda recalling 143,000 Civics, Fits to fix faulty software http : / / bigstory . ap . org / article / 2f5f75fd91e64ec6bde06bacf9824867/hondarecalling - 143000 - civics - fits - fix -faulty-software
- Beech Eric GM recalls nearly 52,000 SUVs for inaccurate fuel gauge http://www.reuters. com/article/2014/05/03/us- gm- recallsuv-idUSBREA4209C20140503
- Klayman Ben Chrysler recalls 18,092 Fiat 500L cars for transmission issue http : / / www . reuters . com / article / 2014 /03 / 17 / us - chrysler - usrecall -idUSBREA2G0PU20140317
- Shiraishi Shinichi , Mohan Veena , and Marimuthu Hemalatha Test Suites for Benchmarks of Static Analysis Tools ISSRE 15 Industry Track NIST 2015
- Baier Christel and Katoen Joost-Pieter Principles of model checking 26202649 MIT press Cambridge 2008
- Engler Dawson and Musuvathi Madanlal Static Analysis Versus Software Model Checking for Bug Finding In VMCAI Springer 2004 191 210
- Java Path Finder http : / / babelfish . arc . nasa.gov/trac/jpf 2014 05 17
- NuSMV Home Page http://nusmv.fbk.eu/ 2014 05 17
- UPPAAL: Academic Home http : / / www . uppaal.org/ 2014 05 17
- Havelund Klaus and Rosu Grigore Preface: Volume 55, Issue 2 Electronic Notes in Theoretical Computer Science 55.2 2001 287 288
- Emerson E. Allen and Clarke Edmund M. Characterizing Correctness Properties of Parallel Programs Using Fixpoints Proceedings of the 7th Colloquium on Automata, Languages and Programming Springer-Verlag 1980 169 181 3-540-10003-2
- Havelund Klaus and Rosu Grigore Monitoring Programs Using Rewriting 16th IEEE International Conference on Automated Software Engineering (ASE 2001) 26-29 November 2001 Coronado Island, San Diego, CA, USA IEEE Computer Society 2001 135 143 0-7695-1426-X 10.1109/ASE.2001.989799
- Pnueli Amir and Zaks Aleksandr PSL Model Checking and Run-Time Verification Via Testers FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton Canada August 21-27, 2006 Proceedings Misra Jayadev , Nipkow Tobias , and Sekerinski Emil 4085 Lecture Notes in Computer Science Springer 2006 573 586 3-540-37215-6 10.1007/11813040_38
- Bauer Andreas , Leucker Martin , and Schallhart Christian The Good, the Bad, and the Ugly, But How Ugly Is Ugly? Runtime Verification, 7th International Workshop, RV 2007 Vancouver, Canada March 13, 2007 Revised Selected Papers Sokolsky Oleg and Tasiran Serdar 4839 Lecture Notes in Computer Science Springer 2007 126 138 978-3-540-77394-8 10.1007/978-3-540-77395-5_11
- Barringer Howard , Havelund Klaus , Rydeheard David E. , and Groce Alex Rule Systems for Runtime Verification: A Short Tutorial Run-time Verification, 9th International Workshop, RV 2009 Grenoble, France June 26-28, 2009 Selected Papers 2009 1 24 10.1007/978-3-642-04694-0_1
- Chen Feng and Rosu Grigore Parametric Trace Slicing and Monitoring Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009 York, UK March 22-29, 2009 Proceedings Kowalewski Stefan and Philippou Anna 5505 Lecture Notes in Computer Science Springer 2009 246 261 978-3-642-00767-5 10.1007/978-3-642-00768-2_23
- Barringer Howard and Havelund Klaus Internal versus External DSLs for Trace Analysis -(Extended Abstract) Runtime Verification - Second International Conference, RV 2011 San Francisco, CA, USA September 27-30, 2011 Revised Selected Papers 2011 1 3 10.1007/978-3-642-29860-8_1
- Kim Moonjoo , Lee Insup , Sammapun Usa , Shin Jangwoo , and Sokolsky Oleg Monitoring, Checking, and Steering of Real-Time Systems Electr. Notes Theor. Comput. Sci. 70.4 2002 95 111 10.1016/S1571-0661(04)80579-6
- Bodden Eric , Hendren Laurie J. , Lam Patrick , Lhoták Ondrej , and Naeem Nomair A. Collaborative Runtime Verification with Trace-matches Runtime Verification, 7th International Workshop, RV 2007 Vancouver, Canada March 13, 2007 Revised Selected Papers Sokolsky Oleg and Tasiran Serdar 4839 Lecture Notes in Computer Science Springer 2007 22 37 978-3-540-77394-8 10.1007/978-3- 540- 77395-5_3
- Chen Feng and Rosu Grigore Mop: an efficient and generic runtime verification framework Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007 October 21-25, 2007 Montreal, Quebec, Canada Gabriel Richard P. , Bacon David F. , Lopes Cristina Videira , and Steele Guy L. Jr. ACM 2007 569 588 978-1-59593-786-5 10.1145/1297027.1297069
- Stolz Volker and Bodden Eric Temporal Assertions using AspectJ Electr. Notes Theor. Comput. Sci. 144.4 2006 109 124 10.1016/j.entcs.2006.02.007
- Seyster Justin , Dixit Ketan , Huang Xiaowan , Grosu Radu , Havelund Klaus , Smolka Scott A. , Stoller Scott D. , and Zadok Erez Aspect-Oriented Instrumentation with GCC Run-time Verification - First International Conference, RV 2010 St. Julians, Malta November 1-4, 2010 Proceedings 2010 405 420 10.1007/978-3-642-16612-9_31
- Dam Mads , Jacobs Bart , Lundblad Andreas , and Piessens Frank Security Monitor Inlining for Multithreaded Java Genoa: Proceedings of the 23rd European Conference on ECOOP - Object-Oriented Programming 2009 546 569 978-3-642-03012-3
- Aktug Irem , Dam Mads , and Gurov Dilian Provably Correct Runtime Monitoring FM ’08: Proceedings of the 15th int. symposium on Formal Methods Turku, Finland 2008 262 277 978-3-540-68235-6
- Erlingsson Úlfar and Schneider Fred B. SASI enforcement of security policies: a retrospective NSPW ’99: workhop on New security paradigms 2000 87 95 1-58113-149-6
- Cirstea Horatiu , Moreau Pierre-Etienne , and de Oliveira Anderson Santana Rewrite Based Specification of Access Control Policies Electron. Notes Theor. Comput. Sci. 234 2009 37 54 1571-0661 http://dx.doi.org/10.1016/j.entcs.2009.02.071
- de Oliveira Anderson Santana , Wang Eric Ke , Kirchner Claude , and Kirchner Hélène Weaving rewrite-based access control policies FMSE’07: Proceedings of the ACM workshop on Formal Methods in Security Engineering 2007 71 80
- Falcone Yliès , Currea Sebastian , and Jaber Mohamad Runtime verification and enforcement for Android applications with RVDroid Runtime Verification Springer 2013 88 95
- ProofObjects: Working with Explicit Evidence in Coq http : / / www . cs . cornell . edu /~clarkson / courses / sjtu / 2014su / terse / ProofObjects.html 2015 09 1
- How I discovered CCS Injection Vulnerability (CVE-2014-0224) http : / / ccsinjection . lepidum . co . jp / blog / 2014 - 06 - 05 / CCS -Injection- en/index.html 2014 05 15
- Formalizing 100 theorems in Coq 2015 09 1
- CompCert - The CompCert C Compiler http: //compcert.inria.fr/compcert-C.html 2015 09 1
- Leroy Xavier The CompCert C Verified Compiler 2012
- Krebbers Robbert , Leroy Xavier , and Wiedijk Freek Formal C semantics: CompCert and the C standard Interactive Theorem Proving Springer 2014 543 548
- Zhou Rui , Min Rong , Yu , Qi Li Chanjuan , Sheng Yong , Zhou Qingguo , Wang Xuan , and Li Kuan-Ching Formal verification of fault-tolerant and recovery mechanisms for safe node sequence protocol Advanced Information Networking and Applications (AINA), 2014 IEEE 28th International Conference on IEEE 2014 813 820
- Kropf Thomas Introduction to formal hardware verification Springer Science & Business Media 2013
- Behrens Diogo , Weigert Stefan , and Fetzer Christof Automatically tolerating arbitrary faults in non-malicious settings Dependable Computing (LADC), 2013 Sixth Latin-American Symposium on IEEE 2013 114 123
- Kane Aaron Runtime Monitoring for Safety-Critical Embedded Systems 2015
- Pike Lee , Goodloe Alwyn , Morisset Robin , and Niller Sebastian Copilot: a hard real-time runtime monitor Runtime Verification Springer 2010 345 359
- Petroni Nick L Jr , Fraser Timothy , Molina Jesus , and Arbaugh William A Copilot-a Coprocessor-based Kernel Runtime Integrity Monitor USENIX Security Symposium San Diego, USA 2004 179 194
- Pellizzoni Rodolfo , Meredith Patrick , Caccamo Marco , and Rosu Grigore Bus-MOP: a run-time monitoring framework for PCI peripherals Tech. rep. Technical report University of Illinois at Urbana-Champaign 2008
- Pellizzoni Rodolfo , Meredith Patrick , Caccamo Marco , and Rosu Grigore Hardware run-time monitoring for dependable cots-based real-time embedded systems Real-Time Systems Symposium, 2008 IEEE 2008 481 491
- Greenberg Andy Hackers Remotely Kill a Jeep on the HighwayWith Me in It http : / / www . wired . com / 2015 / 07 / hackers - remotely -kill-jeep-highway/
- Miller Charlie and Valasek Chris Remote Exploitation of an Unaltered Passenger Vehicle www . illmatics . com / Remote % 20Car % 20Hacking.pdf 2015 08 14
- Remote Exploitation of an Unaltered Passenger Vehicle https://www.youtube.com/watch?v=OobLb1McxnI
- Salane Douglas Are Large Scale Data Breaches Inevitable? Cyber Infrastructure Protection 9 2009
- National Highway Traffic Safety Administration Consumer Advisory: Toyota Owners Advised of Actions to Take Regarding Two Separate Recalls 2010 http : / / www . nhtsa . gov/CA/02-02-2010
- National Highway Traffic Safety Administration Part 573 Safety Recall Report 15V-461 2015 https://www-odi.nhtsa.dot.gov/acms/cs/jaxrs/download/doc/UCM483036/RCLRPT-15V461-9407.pdf
- National Highway Traffic Safety Administration RECALL Subject : Inverter Failure may cause Hybrid Vehicle to Stall - NHTSA 2015 http : / / www - odi . nhtsa . dot . gov / owners / SearchResults ? searchType = ID & targetCategory=R&searchCriteria.nhtsa_ ids=15V449000
- National Highway Traffic Safety Administration RECALL Subject : Side-Curtain Rollover Air Bag Deployment Delay - NHTSA 2014 http : / / www - odi . nhtsa . dot . gov / owners / SearchResults ? refurl = email & searchType = ID & targetCategory = R & searchCriteria.nhtsa_ids=14V237
- Chicago Sun Times Ford recalls 432,000 cars because of software problem 2015 http : / / chicago . suntimes . com / business / 7 / 71 / 740316 / ford - recalls -software-problem
- RECALL Subject : Incorrect Yaw Rate/FMVSS 126 - NHTSA 2015
- National Highway Traffic Safety Administration RECALL Subject : Inaccurate Fuel Gauge Reading - NHTSA 2014 http : / / www - odi . nhtsa . dot . gov / owners / SearchResults ? searchType = ID & targetCategory=R&searchCriteria.nhtsa_ ids=14V223000
- BBC News Jaguar recalls 18,000 cars over ’faulty’ cruise control 2011 http://www.bbc.com/news/business-15410253
- Sokolsky Oleg and Tasiran Serdar Run-time Verification, 7th International Workshop, RV 2007 Vancouver, Canada March 13, 2007 Revised Selected Papers 4839 Lecture Notes in Computer Science Springer 2007 978-3-540-77394-8