Security has become a major concern across a number of classes of hardware design, and formal verification is proving to be an effective technology for ensuring that these systems are fully secure.
Security in this context can refer to protection against malicious attack or unintended operation brought about by an external influence. It may relate to the reading of some secret data within a device by a non-authorized third party (confidentiality) or a change in device execution through an unintended input (integrity). Whatever the effect, testing for hardware vulnerabilities is complex and error prone.
Security protection is provided through the use of a number of mechanisms, from the simple encryption of a secret key to protected regions within a device, and linked to trusted virtual environments in software, such as with ARM’s TrustZone® technology. While various mechanisms have been exploited to target software vulnerabilities, hardware security verification is relatively new and requires exhaustive code analysis.
Modern semiconductor designs have been found vulnerable from invasive physical access (for example, de-packaging or deep probe insertions) and logical access (for example, extracting information using misconfigured on-chip debug ports, scan paths, electromagnetic radiation or power consumption). With the growing complexity of modern SoCs operating multi-access software platforms, multiple stakeholders with mixed trust levels share often resources on the same SoC. Providing this functionality while also maintaining platform integrity is often the core issue for security systems and their verification.
A few examples of common vulnerabilities might include:
For many of these situations, the general verification approach is to identify the vulnerable area and its trusted accessibility options and then to ensure, in an exhaustive fashion, that no other access mechanisms exist.
An easy example is a protected key within a device that should be read in an encrypted form when addressed through one specific output port. This detail needs to be specified and the design analyzed for sources of vulnerability. Then a full verification of the design, to see if the key may be accessed through any of these vulnerabilities, needs to take place.
Formal techniques are particularly good at tracking signals exhaustively through a design, and understanding all the possible paths a signal might take. It is also easy with Formal to simply ask the question of the form: “can this data register be read through any port except this one, on any sequence of control signals?” and have it test every possible option without an engineer having to specify a test for every option. Formal is an ideal technology for this purpose and, not surprisingly, security solutions are emerging that leverage formal platforms.
Some of these security solutions make use of data tagging techniques and, indeed, it is possible for a Formal knowledgeable engineer to create a small set of security properties that can tag a security key held in a specific register and then check that there is no unexpected leakage of information of the key to any output. Leakage can occur, for example, through a specialized debug interface, by a memory read for software access, or down a scan path in an unexpected fashion.
Of course security experts can create a more refined set of security properties based on methods used to attack a device, and their knowledge is invaluable when looking for new methods in which a chip may be hacked.