Thought Leadership

How Formal Techniques Can Keep Hackers from Driving You into a Ditch, Part 1 of 2

By Joe Hupcey III

[Preface: everywhere it refers to automobiles in this post, you can also swap in “X-Ray machine”, “pacemaker”, and “aircraft”]

The dark side of our connected future is here: from the comfort of a living room sofa, security researchers were able to remotely disable the brakes and transmission of a new Jeep Cherokee — literally driving the vehicle into a ditch (Hackers Remotely Kill A Jeep On The Highway – With Me In It, Wired, 7-21-15). Another group of researchers were able to hack into a car’s braking and other critical systems via the digital audio broadcast (DAB) infotainment system (“Now car hackers can bust in through your motor’s DAB RADIO”, The Register, 7-24-2015). In this form of attack, multiple vehicles could be affected simultaneously.

wired -- jeep in a ditch -- IMG_0724-1024x768
Security Researcher Charlie Miller attempts to reverse out of a ditch after its brakes were remotely disabled. Source: Wired Magazine

Fortunately no one has been hurt in these experiments, and manufacturers have been quick to respond with patches. But these two stories (and a growing number of others like them) demonstrate just how insecure today’s automobile electronics are.

So what can be done to prevent this?

First, I’m not here to argue that there is a single “silver bullet”.  To combat the numerous direct and side channel attacks there needs to be multiple, overlapping solutions to provide the necessary defense in depth. That said, the #1 priority is to secure 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.

So how exactly am I defining the “root of trust”? I assert that in the near future the root of trust will effectively be an encryption key – a digital signature for each vehicle — that will be encoded into the electronics of every vehicle. Hence, I argue that the data packets transiting the interior networks of the vehicle will need to be “signed” with the vehicle’s signature and decrypted by the receiving sensor packs/Engine Control Units (ECUs)/radios/etc.

That’s right: encrypt all packets in all the interior data networks. Every. Single. One.

Is this overkill? Look again at the picture of the Jeep in the ditch.

Unfortunately, most automobiles being sold today cannot support this proposal since popular bus protocols like CAN and LIN simply do not have the bandwidth or protocol architecture to support this.  However, real time packet encryption/decryption is certainly possible with the increasingly popular Automotive Ethernet standard (whose early adopters include BMW, Hyundai, and Volkswagen). In such an advanced system, the automaker would embed a unique encryption key in each vehicle in the factory (exactly like set-top-box and game console makers do today). The key would be stored in a secure memory element of some sort – a separate memory chip or a register bank inside a system on a chip (SoC)). As such, D&V engineers will need to verify that this secure storage can’t be compromised.

So what’s the best verification methodology to ensure that this secure storage can’t be (A) read by an unauthorized party or accidentally “leak” to the outputs; or (B) be altered, overwritten, or erased by the bad guys?

Unfortunately, the classical approach of employing squads of “white hat” hackers to try and crack the system drastically decreases in effectiveness as circuit complexity increases. Similarly, even a really well designed constrained-random simulation environment is not exhaustive either. Consequently, a mathematical, “formal” analysis is required. The good news is that my group has been successful partnering with customers to develop exactly this type of solution. I’ll explain in part 2 of this series …

Until then, keep your eyes on the road and your hands up on the wheel; and I look forward to hearing your comments.

Joe Hupcey III

 

P.S. I grant there are ways to isolate software processes from each other to forestall hacking (indeed, my colleagues down the hall in Mentor’s Embedded Systems Division coach customers on how to do this every day.) However, I assert that only a sound hardware-based solution based on securely stored encryption keys will establish a secure root of trust, as well as give consumers peace of mind.

In a somewhat related note, I predict that in the near future computers/phone/tablets will start implementing and promoting hardware switches to physically disconnect their built-in microphones and cameras. Similarly, just like all cars now have air bag shutoff switches, there should also be a mechanical switch on the dashboard that disconnects all the vehicle’s external antennas. Granted this will not completely eliminate clever, unforeseen side channel attacks; but it will go a long way. Besides, the marketing value will be fantastic.

 

Comments

5 thoughts about “How Formal Techniques Can Keep Hackers from Driving You into a Ditch, Part 1 of 2
  • You will still be liable for any recall/injuries en’masse 15+ years from now for cars, 25+ for commercial vehicles. Whatever security HW/SW you design today will be as secure as an Apple2e eventually.

  • Paul: I see both your points in operating in tandem: it’s critical that automakers, et.al. enable secure maintenance flows with today’s best practices with digital signatures, etc., and effective “air gaps” will also be required to isolate the “Apple 2e” controls from being the source of trouble.

    That said, I agree at a certain point in the security “arms race” the given car/piece of equipment/system will become impractical to patch. At a minimum you’d might be able to replace an ECU or other “now impossible to secure” part; the worst case would be forced retirement of the whole vehicle.

  • A real life case just came up that reflects my earlier comment, “at a minimum you’d might be able to replace an ECU or other ‘now impossible to secure’ part”. Apparently the only way to secure the key fob data link of certain models of luxury cars is to replace the RFID chips in the keys and transponders at significant expense: http://goo.gl/6QGGnT

Leave a Reply

This article first appeared on the Siemens Digital Industries Software blog at https://blogs.sw.siemens.com/verificationhorizons/2015/08/05/how-formal-techniques-can-keep-hackers-from-driving-you-into-a-ditch-part-1-of-2/