Three security rules to use when verifying secure processor IP.
By Ruud Derwig and Nicole Fern
Security in modern systems is of utmost importance. Device manufacturers are including multiple security features and attack protections into both the hardware and software design. For example, the Synopsys DesignWare ARC Processor IP includes many security functions in its SecureShield feature set. End-product system security, however, cannot be guaranteed by using a secure processor alone. The final product security results not only from using proven, secure hardware components. Configuration, integration and additional software have to be taken into account as well. When integrating a secure processor into a chip and developing the software for it, security vulnerabilities can still be introduced. Verifying the absence of these security vulnerabilities in systems comprised of hardware and software is a complex effort. Tortuga Logic’s Radix-S, which employs patented information flow tracking technology to enable verification of security objectives based around the concepts of confidentiality and integrity, can help verify that designers have integrated and programmed security features correctly with minimal disruption to existing verification workflows.
Security verification of ARC processor debug lock functionality and MPU configuration
System integrators who use processor IP must ensure that they configure and manage the protection and security features correctly, and that they do not introduce vulnerabilities. Evaluating the security of complex, highly combined hardware-software systems and ensuring these systems are free from vulnerabilities is hard as most verification tools target functional, not security, verification. Tortuga Logic and Synopsys have collaborated to demonstrate a novel security verification methodology enabling several system-level security objectives for the ARC Processor to be verified using Radix-S in conjunction with the existing simulation infrastructure consisting of VCS and MetaWare.
These security objectives resulted in the creation and verification of three security rules. Two are based on threat models related to secure debug and one verifies the absence of software errors during configuration of the ARC memory protection unit (MPU). These rules can be easily applied to other projects. Below, we describe how these security rules are specified and verified during hardware/software simulation of ARC processors.
Verifying secure debug locked mode
Debug mode provides increased controllability and observability for both hardware and software testing; however, access to design internals poses a security risk. To ensure debug functionality can only be accessed by authorized users, ARC processors provide the option to configure secure debug features, including a locking/unlocking mechanism (Figure 1). Synopsys provides an example unlock module based on a simple challenge response protocol. Designers typically replace the example and define custom unlock logic to provide the security necessary to address specific threat models or to integrate the processor secure debug into a larger SoC secure debug design.
Figure 1: Secure debug in ARC EM Processor
Designers should verify that the lock functionality implements the expected behavior and that no unexpected information flows occur when the debug access port is in locked mode. When in locked mode the debugger should not be able to access 1) processor registers, or 2) processor data memory.
Radix-S can verify that a specific ARC configuration satisfies this assumption when in locked mode by creating two security rules to track the flow of the processor registers and data memory to the debug port. These rules are written using Tortuga Logic’s Sentinel language. A unique feature of Sentinel is the ability to express security requirements related to information flows in the design, which is essential for efficiently expressing and verifying confidentiality and integrity properties for design assets. The “no-flow” operator (=/=>) is the basic building block used to create rules for tracking information flows between design signals. The Sentinel keywords “when” and “unless” exist to specify conditions which must be met before flow tracking is performed, and conditions under which flows between signals are allowed, respectively.
Security Rule #1: CPU register contents should never flow to the debug interface when the debug access port is in locked mode.
u_regfile_2r2w.$all_outputs when (!dbg_unlock) =/=> dbg.$all_outputs
u_regfile_2r2w is the module that implements the ARC EM register file. dbg_unlock is the unlock signal from Figure 1, and dbg is the debug module itself. The “$all_outputs” keyword is shorthand for describing the set of all output signals for a particular module instance in the design hierarchy. Rule #1 will fail if register file contents flow to debug module outputs when debug is in locked mode.
Security Rule #2: Data memory should never flow to the debug interface when the debug access port is in locked mode.
dccm_data_out when (!dbg_unlock) =/=> dbg.$all_outputs
Rule #2 will fail if data memory contents (dccm_data_out) can exit the debug access port while debug is in locked mode. Note that ARC processors feature single cycle access data closely coupled memories (DCCM for data and ICCM for instructions). Radix-S can verify both Rule #1 and #2 as part of the existing test flow in an ARC-based system to provide assurance that the debug port does not leak internal processor information when in locked mode. Designers can write additional Radix-S Sentinel rules to verify the custom unlock module itself.
Verifying software initialization of secure memory regions
ARC SecureShield technology can partition memory into secure and normal regions which should remain completely isolated. Figure 2 shows two ways of realizing such a split into a normal execution environment and a trusted execution environment (TEE). The left-side diagram shows a single processor TEE, where a single CPU executes both the trusted and the non-trusted applications, isolated from each other by secure and normal CPU privilege levels enforced by an MPU. On the right, a traditional approach shows that each environment has its own, private CPU and other resources like memory or cryptographic accelerators. This approach is called a “hosted TEE” since the normal application processor acts as a host for the TEE CPU. For example, cryptographic keys residing in secure memory used to encrypt confidential information should not be accessible by unprivileged programs. Unprivileged programs should only have access to normal memory, and the data in secure memory should never end up in normal memory.
Figure 2: Trusted Execution Environments on a single (left) or dedicated (right) processor
In this case study, the threat model covers malicious unprivileged programs running in normal mode with access to normal memory regions only—enforced by the ARC MPU. Malicious software will try to identify and exploit mistakes made during the configuration of the memory regions to extract sensitive information from programs executing in secure mode (Figure 3). Because Radix-S provides a concise mechanism for describing information flow properties, designers can verify specific memory protection configurations and easily adapt as design requirements evolve. Moreover, the rules do not check the MPU control registers directly but instead check the higher-level property that data from secure memory should not end up in normal memory. Therefore, not only a specific misconfiguration error would be checked, but any error that could lead to data leaking from secure to normal memory.
Figure 3: Potential Security Violation—Flows between isolated memory regions
The ARC’s SecureShield MPU can be programmed to enforce memory regions with different access privileges. This way, “secure” programs can be isolated from “normal” programs. In this case study, two data memory regions are created:
Radix-S verifies the isolation of these two memory regions by creating a Sentinel rule tracking the flow of information from the output of the data memory to the input of the data memory (in between the data will flow through the ARC processor as software is executing). Security Rule #3 will fail if information flows through the path shown as a red dashed line in Figure 4. One important aspect of Sentinel rules is that information flows are tracked over time through arbitrary combinational and sequential logic transformations. Data from secure memory can be pipelined or combined with other data inside the ARC processor and Rule #3 will still detect if any versions of the secure data are written into the normal data region.
Security Rule #3: Data from secure memory region should never flow to normal memory region.
dccm_data_out when (dccm_data_addr >= 0x800000 && dccm_data_addr < 0x802000) =/=> dccm_data_in
unless (dccm_data_addr >= 0x800000 && dccm_data_addr < 0x802000)
Rule #3 states that the output data from the data memory module (dccm_data_out) is tracked when reading from the secure address range and the rule will fail if this information propagates to the input of the data memory module (dccm_data_in) unless the data is entering the memory during a write to the secure region. This extra check of the address range for secure information that arrives at dccm_data_in is necessary because secure software can read data from the secure region and then write data back to secure memory. Rule #3 can detect software configuration errors made during the setup of the secure and normal memory regions. To test this assertion, Synopsys and Tortuga Logic tested Rule #3 in a design that configured the secure region to be 32 bytes shorter than expected. Because of this mistake, any sensitive privileged data written to the last 32 bytes of the secure region could be read by programs executing in normal mode.
Radix-S provides multiple views to easily see the information flow and any rule failures. For example, the Path View in Figure 4 shows information flow from the rule source to destination signal. The information flow is presented graphically as a path through time and design hierarchy. The Path View for Rule #3 shows data read from secure memory (from dccm_data_out) flowing through the ARC processor before it re-enters the data memory module during a write (through dccm_data_in) to normal memory, causing the rule to fail. Path View provides valuable insight into the root cause of rule failures and makes the security analysis more efficient.
Figure 4: Radix-S Path View—a complete information flow path demonstrating rule failure
Conclusion
Tortuga Logic’s Radix-S security verification platform with Synopsys’ ARC Processor IP offers a powerful solution for the complex problem of hardware-software security verification. The Synopsys ARC processor IP, with its SecureShield technology, enables designers to develop a TEE. The TEE guarantees code and data protection for confidentiality and integrity, providing the ability to share system resources to process trusted and non-trusted code. However, ensuring the security of the whole system requires the analysis of both the hardware and software. Radix-S is a powerful tool for ARC customers to identify and prevent any security vulnerabilities that are introduced by configuring and integrating the processor in their design, or by the platform and application software that is executed on it. Tortuga Logic’s Radix-S software provides the capability to verify the security of any ARC Processor-based design with the consideration of hardware integration and the software running on top of it. Improper programming of the ARC Processor can lead to security vulnerabilities, and Radix-S can detect these vulnerabilities during standard functional verification. Radix-S can be used as the basis for a true hardware SDL that enables designers to build secure, high-quality processor-based systems.
For more information, read this in-depth white paper: Configure, Confirm, Ship: Build Secure Processor-Based Systems with Faster Time-to-Market.
Ruud Derwig is a senior staff engineer at Synopsys.
Nicole Fern is a senior hardware security engineer at Tortuga Logic.
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
Leave a Reply