How Formal Techniques Can Keep Hackers from Leaving You in the Cold

While internet connected vehicles remain a popular target for hackers, the new breed of “smart” devices have the potential to invite the bad guys inside your home and force you to pay them to leave. Specifically, in a DefCon 2016 demo security researchers Andrew Tierney and Ken Munro showed how an internet connected thermostat could be taken over and reloaded with “ransomware”. Consequently, the bad guys could literally leave you in the cold until you pay up.

Fortunately this was just a proof of concept, but this story and a depressing large number of others like it demonstrate just how insecure today’s consumer electronic devices are.

So what can be done to prevent this?

First, as I’ve said before there is no single “silver bullet”. To combat the numerous direct and side channel attacks, multiple, overlapping solutions are needed 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”? It is an encryption key – a digital signature for each device – that will be encoded into the electronics of every “IoT” unit. Hence, I argue that before the device accepts any commands from the outside world, the private key stored in the device must be combined with the public key appended to the incoming data to authenticate its legitimacy. In such a system, just like set-top-box and game console makers do today, the smart thermostat manufacturer would embed a unique encryption key in each device in the factory. 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 rapidly decreases in effectiveness as circuit complexity increases. Similarly, even a really well designed constrained-random simulation environment is not exhaustive either. 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 smart thermostat 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 Design & Verification 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 SystemVerilog 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. a tool that can mathematically prove the confidentiality and integrity of your DUT’s “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 that the “root of trust” – i.e. the storage for the system’s encryption keys – cannot 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; and only an exhaustive formal analysis can verify this with mathematical certainly. 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 verify the integrity and confidentially of your secure storage.

Until next time, stay cool, or stay warm – whichever you prefer.

Joe Hupcey III

P.S. In a somewhat related note, I predict that in the near future such devices will start implementing and promoting hardware switches to physically disconnect their communications links. In the thermostat case, once the regular heating & cooling patterns were programmed in, the user could decide to disconnect the device from the internet. The user would only re-enable communications upon notification of a firmware upgrade from the manufacturer, or before embarking on a trip, etc. 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.

P.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 soon, to learn more feel free to contact me offline, or ask questions in the comments section below.

P.P.P.S. If you want to learn more about the underlying formal technology, on November 16 at 8am Pacific there will be a webinar on “Back to Basics with Formal Verification: How to Shorten Your Schedule with Interactive Formal Debug and Design Exploration“.  No worries if you miss the live broadcast — the presentation recording will be posted for later viewing.

Reference Links:

The Hacker News article on this: http://thehackernews.com/2016/08/hacking-thermostat.html

(1) Using Formal Methods to Verify Complex Designs, IBM Haifa Research Lab, 2007