Hardware Security Verification Example: CWE-1251

Common Weakness Enumeration (CWE) is a community-developed list of software and hardware weakness types which 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 CWE to a security rule which you can include in your simulation regression runs.

“The product's architecture mirrors regions without ensuring that their contents always stay in sync. Having mirrored regions with different values might result in the exposure of sensitive information and/or other consequences, including loss of access control.

Due to architectural and performance constraints, one might need to duplicate a resource. The most common example of doing this in computer architecture is the concept of cache, which keeps a "local" copy of the data element in memory, because the time to access the memory (which is located far off from the computing core) is significantly longer compared to the time it takes to access a local copy (cache). Thus, keeping a local copy of some distant entity provides significant performance improvement. Unfortunately, this improvement also comes with a downside, since the product needs to ensure that the local copy always mirrors the original copy truthfully. If they get out of sync somehow, the computational result is no longer true."

This CWE overlaps with the functional requirement to keep two resources in sync and this should be addressed in the functional verification plan. Radix Security Rules can be used to ensure no illegal data access when resources are not in sync.

Assuring that, for example, data in a cache location is equal to data in memory can be done using functional SystemVerilog assertions such as:

NO_UPDATE: assert always (@ posedge clk) (update not in progress) => (core0.dcache[flush_dst] == nvm.mem[flush_dst]);

Depending on the actual design implementation there may be several vulnerabilities to verify. Here let’s consider that data in a duplicated resource must not flow to a location that is user accessible while an update of the resource controlling the data is in progress. This can be modelled as information flow verification.

In this example, consider the hypothetical SoC below:

In this SoC, there are 3 processors, core0, core1 & core2, running user code. For performance reasons, there is one main Memory Management Unit (MMU) and one shadow MMUs. The main MMU handles memory accesses by core0 and the shadow MMU handles memory accesses from core1 & core2. Updates to the main MMU is done by the tmcu and then the main MMU updates the shadow MMU through messages on the interconnect. If the accessible address range for the un-trusted cores is updated in the main MMU, there is a time when the three processors may have access to different memory ranges.

Threat Model

A malicious agent running on core2 may be able to access memory locations outside its allowed range because the shadow MMU does not yet have the same configuration as the main MMU. If core2 can flood the interconnect with traffic and delay the update request, the update to the shadow MMU may be delayed, extending the time available for access.

Security Requirement

No access to memory through the shadow MMU should be allowed while an update is in progress.

Radix Security Rules

The requirement can be expressed as an information flow verification problem i.e.:

• Data from the memory protected by the shadow MMU should not flow to the processors while an update of the MMU is in progress.
• Data from either of the cores should not flow to the memory protected by the shadow MMU while an update of the MMU is in progress

Using the Tortuga Logic Radix no-flow operator “=/=>” we can write the following security rules:

Verification

Using the security rules above, the Tortuga Radix tool will build a security model 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