This content is not included in
your SAE MOBILUS subscription, or you are not logged in.
How Formal Techniques Can Keep Hackers from Driving You into a Ditch
Technical Paper
2016-01-0066
ISSN: 0148-7191, e-ISSN: 2688-3627
Annotation ability available
Sector:
Language:
English
Abstract
The number one priority in vehicle security is to harden the root-of-trust; from which everything else - the hardware, firmware, OS, and application layer’s security - is derived. If the root-of-trust can be compromised, then the whole system is vulnerable. In the near future the root-of-trust will effectively be an encryption key - a digital signature for each vehicle - that will be stored in a secure memory element inside all vehicles. In this paper we will show how a mathematical, formal analysis technique can be applied to ensure that this secure storage cannot (A) be read by an unauthorized party or accidentally “leak” to the outputs or (B) be altered, overwritten, or erased by unauthorized entities. We will include a real-world case study from a consumer electronics maker that has successfully used this technology to secure their products from attacks 24/7/365.
Note that the techniques and solutions described herein are focused exclusively on digital circuitry specified in a register transfer level (RTL) language, such as Verilog or VHDL - i.e. the most fundamental level of digital design. This paper does not go into any physical design and verification issues or related “side-channel” attacks, nor do we address firmware or higher level software security best practices.
Recommended Content
Citation
Hupcey, J. and Ramirez, B., "How Formal Techniques Can Keep Hackers from Driving You into a Ditch," SAE Technical Paper 2016-01-0066, 2016, https://doi.org/10.4271/2016-01-0066.Also In
References
- Hackers Remotely Kill A Jeep On The Highway - With Me In It Wired 7 21 15 http://www.wired.com/2015/07/hackers-remotely-kill-jeep-highway/
- Now car hackers can bust in through your motor's DAB RADIO The Register 7 24 2015 http://www.theregister.co.uk/2015/07/24/car_hacking_using_dab/
- Whitepaper Automotive Ethernet: An Overview https://www.ixiacom.com/sites/default/files/resources/whitepaper/ixia-automotive-ethernet-primer-whitepaper_1.pdf
- John Aynsley UVM Verification Primer Duolos website June 2010 https://www.doulos.com/knowhow/sysverilog/uvm/tutorial_0/
- Using Formal Methods to Verify Complex Designs IBM Haifa Research Lab 2007 https://www.research.ibm.com/haifa/projects/verification/RB_Homepage/papers/wp_formal_verification_1.pdf
- Formal Verification, Wikipedia https://en.wikipedia.org/wiki/Formal_verification