As cars become electric, they are also adding self-driving, driver warning systems, and even the latest video games. Automakers have found that their focus on traditional mechanical engineering provides little help when the car is defined by software and limited by the operating system hiding the hardware.
Put another way, modern automobiles are now a “software problem”. And as anyone at p0wn2own, or DEFCON can tell you, if it’s a software problem it’s a security problem.
So, what does automotive cyber resilience mean, exactly?
Automotive cyber resilience means isolating and quickly recovering in response to a wide range of automotive threats including accidental things such as software or hardware faults or intentional things such as attempted thefts or cyber sabotage. It is not possible to predict all the things that could fail, but we can put software into buckets that don’t affect each other when something goes wrong.
Automobile systems must minimise the exposed area for potential attacks and then limit the damage an attack can do if it does get through. This means using strong software to encapsulate legacy systems, while also using zero-trust methods to manage and remotely update them.
The following requirements are critical: the code defining and restarting the other codes must work to prevent catastrophic disruption; containers that prevent faults from propagating must have formal guarantees; required hardware resources must be restricted and formally backed, and devices must possess remote manageability and be supported by isolated and verified systems.
The above requirements aren’t optional and cannot be done in half measures. Specifically, the software patterns developed in the 1990s were built for computers that were used and managed by humans who knew what they were doing. Performance was chosen over stability and that legacy persists in every single widely used System in use today. This includes microkernel systems which are safer than their monolithic peers but are still tested using traditional unverified methods.
There are new techniques, however, which bring hope. Recent advances in formal verification mean that bodies of code as large as 10L lines can (with much effort) be fully-proven to be correct. The first and still best example of this is the seL4 Microkernel developed at the University of New South Wales. Used correctly, it can create hardened sandboxes that truly isolate unproven code and prevent faults from propagating. Although formal verification has been utilised to guarantee security in defence organisations, this ability to scale it up to industrial use is new and profound.
It's clear that new techniques and technologies are required to provide an updated approach to managing modern vehicles and other critical, interconnected devices. Formal Methods allows us to prove that software will function as designed. It unambiguously proves that code doesn’t have buffer overruns, null pointer reference, or many other errors that commonly occur with other software.
Formal methods-backed application management and services are the only sustainable means of enabling full cyber resilience, and in turn, a more secure framework that can withstand cyber threats and disruption. The result is devices, vehicles, and infrastructure that survive attacks and software errors while allowing for them to be controlled, monitored, and updated by only approved parties.
The evolution of transportation demands a new approach to security and safety, one where cyber resilience prevails where the risks are assessed, and the threats are monitored continuously. By leveraging formal methods, automotive products can function as intended but can also withstand cyber-attacks, faults, and other errors while continuing to operate normally. Looking forward, formally verified microkernels such as seL4 will become required in automotive and many other industrial platforms. Consequently, the future will see safer roads, populated by vehicles that are resilient and secure against cyber threats.
Author details: Boyd Multerer, CEO and founder, Kry10
