Don’t Have A Meltdown Over A Spectre In Your SoC

Security verification through formal analysis should be part of the verification plan for SoCs and IP blocks.


You may be concerned about last year’s widely published Spectre and Meltdown vulnerabilities affecting most processors. Are your phone and computer OK? Or more importantly, if you are designing or verifying a System on Chip (SoC), do you have a specter in your design? Let’s first look at what these two vulnerabilities are and how they may be affecting your system.

Both vulnerabilities are caused by hardware features designed to make programs run faster, such as speculative execution and caches. If a program has a branch, for example, “If A is true, compute function X, else compute function Y”, the processor will compute both functions in parallel and discard the result it does not need once it knows if A is true or not. This can become a problem because of protected memory and caching. Protected memory allows a program to keep its data private and it enables the operating system to prevent one program from seeing data belonging to another program. Before a program is accessing any data, a privilege check is done to determine if the process is allowed to read or write specific data. If the branch condition encountered in speculative execution is a privilege check, the process may access data before it knows if it is allowed to or not. If the privilege check fails, all protected data is discarded. But, the protected data is stored in the cache even if the process was not allowed to access the data in the first place. Attackers have then been able to use this information.

At a high level, the difference between Meltdown and Spectre is that Meltdown may allow a user program to access protected kernel space and Spectre breaks the isolation between programs and may allow a malicious program to trick another program into leaking data.

Spectre and Meltdown are arguably the most visible hardware security flaws found and one lesson learned is that you can no longer ignore security if you design an SoC. Even if your design is much less complex than a modern CPU and it will never be affected by Meltdown or Spectre or any other published hack it can still have security problems. Many hacks take advantage of software flaws but that doesn’t mean that hardware is secure or immune to security breaks.

Hardware design should be the first place to look when building a secure SoC or system. Hardware is usually viewed as secure by the software. The assumption is that computation like encryption and key storage can only be trusted to the hardware. However, if there are bugs or oversights in the architecture that can be utilized for unauthorized access, unlike in software, you can’t patch hardware. Your only option is to re-spin the chip and that does not fix all the systems already shipped that still have flaws.

If you think that security is not a requirement and that it won’t affect your design, think again. If your SoC has secure boot or handles financial data, it most likely includes an encryption block and very secret encryption keys that should not be accessible by anyone. In this case, it is pretty obvious you need to consider verifying the security aspects of your design. If the design is an IP block which doesn’t handle or store secret data, that doesn’t mean you can ignore security. You don’t know where the IP will be used and if it is integrated in a system it may provide an unintentional backdoor into the device.

Ensuring no specter is hiding in your SoC requires verification. Remember, “If it is not verified, it doesn’t work.” Hardware security verification should be “Formal and Formal:”

  • Formal Plan
  • Formal Verification

Security verification must be part of the verification plan and it should describe what security features to test and what data and modules are protected and who is and is not allowed to access it. For example, make sure access control on certain memory address ranges work as intended and that only secure masters can access secure slaves on an internal bus. A lot of testcases can be simulated but a large class of data propagation verification cannot be done with simulation. You simply can’t simulate what should not be allowed to happen.

To complete the hardware security verification, formal analysis is needed. Only formal tools can prove that data is secure. For example, one can prove that an encryption key can never reach any chip output under any circumstance. Another important scenario is to ensure that registers and protection signals cannot be unintentionally modified. If register access protection is configured at startup, only formal can prove that the configuration cannot be modified.

Verifying that there are no bugs in the hardware that cause secure data leaks will help you avoid a meltdown.

Leave a Reply

(Note: This name will be displayed publicly)