Hardware Security Verification Example: CWE-1263 Improper Physical Access Control

Common Weakness Enumeration (CWE) is a community-developed list of software and hardware weakness types that may cause Security issues. The list is maintained by the MITRE organization and can be found here: cwe.mitre.org

In my previous post, “Better Hardware Security Verification through CWE and Information Flow Checking” I introduced Information Flow Checking as a way to verify that you don’t have the weaknesses listed in the CWE database in your design.

Here, let’s look at a more detailed example of how you can translate a Hardware CWE to a security rule which you can include in your simulation regression runs.

The product is to be designed with access restricted to certain information, but it does not sufficiently protect against an unauthorized actor’s ability to access these areas.

Sections of a product intended to have restricted access may be inadvertently or intentionally rendered accessible when the implemented physical protections are insufficient. The specific requirements around how robust the design of the physical protection mechanism needs to be will depend on the type of product being protected. Selecting the correct physical protection mechanism and properly enforcing it through implementation and manufacturing is critical to the overall physical security of the product.

Depending on the actual design implementation there may be several vulnerabilities related to this CWE to verify. Here, we consider the case where a physical probing attack is being detected and we want to ensure mitigations are effective. This case can be modeled as an information flow verification problem.

In this example, consider the hypothetical SoC below:

The SoC has an anti-tamper detection circuit to detect if the device is de-capped. If the device is de-capped, then the memories will be zeroized so no information will be leaked to an attacker. The processors will also halt to avoid leaking any information about running programs.

Threat Model

An attacker may decap the device and probe internal signals to access sensitive data in memories or registers or observe the program running on the embedded processors.

Security Requirement

When physical tampering is detected e.g. by someone de-capping the device, the processors should stop and memories should be cleared i.e. zeroized to avoid sensitive data leakage.

Radix Security Rules

The requirements can be expressed as information flow verification problems i.e.:

  • Information (existing data before tampering) in SRAM must not flow back to the SRAM when tampering is detected.
  • Information from memory must not flow to the processors if tampering is detected

Using the Tortuga Logic Radix no-flow operator “=/=>” we can write the following security rules. Note: Rules are also required to verify that each processor is halted.

Verification

Using the security rules above, the Tortuga Radix tool will build a security monitor which when simulated together with the design will flag any violation of the rules. Using information flow security rules, over 80% of the MITRE Hardware CWEs can be verified by Radix.

To learn more about how to write security rule checks based on the Hardware CWE list, see our Radix Coverage for Hardware Common Weakness Enumeration (CWE) Guide.

Author

  • Security Application Engineer at Tortuga Logic: Anders Nordstrom is a Functional and Security Verification expert and ASIC design and verification professional with over 25 years of experience both as a design and verification engineer and from methodology development and customer support in the EDA field. Specialize in solving customer verification problems using formal verification tools. Hardware formal security verification expert. Architected Formal security verification tool, developed prototype, and deployed product at customers

Share on twitter
Twitter
Share on linkedin
LinkedIn