How Formal Techniques Can Keep Hackers from Driving You into a Ditch, Part 2 of 2
In Part 1 of this series, inspired by security researchers that were able take over a new Jeep and drive it into a ditch I asserted that in the future all vehicles will need to encrypt their internal control and data bus traffic with an encryption key. This 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, Design & Verification (D&V) engineers will need to verify that this secure storage can’t be compromised.
White hat hacking and constrained-random test benches don’t scale and aren’t exhaustive, so in this post I’ll describe how formal verification technology can be brought to bear.
First, the verification challenge here can be boiled down to two concerns:
(A) Confidentiality: can the key be read by an unauthorized party, or accidentally “leak” to the outputs?
(B) Integrity: can the key be altered, overwritten, or erased by the bad guys (or due to some unforeseen hardware or firmware bug)?
The only way to exhaustively verify (A) and (B) with only a few hours of compute time on common, low-cost servers is by employing formal verification technology. In a nutshell, “formal verification uses mathematical formal methods to prove or disprove the correctness of a system’s design with respect to formal specifications expressed as properties.”(1)
Returning to our automotive example, the “formal specification” is that (A) and (B) above can never happen, i.e. the key can only be read and edited by authorized parties through specific, secure pathways – anything else is a design flaw that must be fixed before going into production.
So what can D&V engineers do at the RTL level to employ formal technology to this verification challenge – especially if they have never used formal tools or have written System Verilog Assertions (SVA) before? Luckily Mentor has developed a fully automated solution that exhaustively verifies that only the paths you specify can reach security or safety-critical storage elements – i.e. to formally prove the confidentiality and integrity of your DUTs “root of trust”. The best part is that no knowledge of formal or property specification languages is required.
Specifically, using your RTL and cleartext, human and machine readable Tcl code to specify the secure / safety-critical storage and allowed access paths as input, the Questa Secure Check app automates formal technology to exhaustively verify the “root of trust” – i.e. the storage for the system’s encryption keys – can be read or tampered with via unauthorized paths.
To expedite the analysis and/or minimize formal compile and run time, the app supports “black boxing” of clearly extraneous IPs and paths to keep the focus on the secure channels alone. The result: an exhaustive proof of your design’s integrity and/or clear counterexamples showing how your specification can be violated.
In summary, only a sound hardware-based solution based on securely stored encryption keys will establish a true root of trust. Only an exhaustive formal analysis can verify this with mathematical certainly, and thus the Questa Secure Check app was created to help customers address this challenge.
I look forward to hearing your feedback and comments on what you are doing to address this challenge.
Keep your eyes on the road and your hands up on the wheel,
Joe Hupcey III
References:
(1) Using Formal Methods to Verify Complex Designs, IBM Haifa Research Lab, 2007
https://www.research.ibm.com/haifa/projects/verification/RB_Homepage/papers/mntrblgs_formal_verification_1.pdf
P.S. Shameless commercial pitch: the lead customer of the Questa Secure Check app is in the consumer electronics space, where their products are subject to world-wide attack, 24/7/365. Suffice to say that if Secure Check can help harden this customer’s system against determined, continuous attacks, it can help automakers, medical device manufacturers, smart phone designers, aircraft companies, etc. In advance of a new Verification Academy course on this topic coming out this autumn, to learn more feel free to contact me offline, or ask questions in the comments section below.
