DiSPEL: Distributed Security Policy Enforcement for Bus-based SoC

Security Policies refer to a set of guidelines, rules, or specifications that are designed to ensure the protection and integrity of assets within the SoC design. Security policies serve a significant part in determining the access, protection, and authentication requirements of different assets within the design. These policies typically represent instances of CIA (Confidentiality, Integrity, and Availability) needs at a higher level. Security policies are put in place to prevent unauthorized access, detect and mitigate potential security threats, and maintain the overall security posture of the system. They serve as actionable instructions for the SoC system architect and designer to implement security measures and countermeasures effectively, ensuring the confidentiality, integrity, and availability of critical assets within the SoC. Security policies in modern SoC designs are often complex and developed in an ad-hoc manner due to their inherent intricacies and undergo refinement and modification throughout the system development process based on security requirements and product needs.

The following taxonomy of security policy classes is presented in [16],[28] that, although not exhaustive, serve to demonstrate the range and variety of policies utilized in practice. Fig. 3 depicts a visual representation of the security policy classification recognized in practice.

• •

  Access Control:
  Access control policies represent the predominant class of security policies in SoC designs, governing the access permissions granted to different agents within the SoC at various stages of execution. An agent $A$, in this context, refers to a component that could be either software or hardware and present in any constituent IP within the SoC design. These access control policies serve as the fundamental ground for various additional policies, including integrity protection, information flow control, secure boot mechanisms, etc.

• •

  Information Flow:
  Information flow policies are employed to restrict the indirect inference of values of any secure asset. The values can be deduced by observing or snooping on intermediate computations or communications within IPs even when direct access is disabled. These policies restrict the flow of information between different components. In most cases, this class of policies is developed by combining access control policies with required auxiliary constraints. This ensures that sensitive information remains protected and inaccessible to unauthorized entities throughout the system.

• •

  Liveness:
  Liveness policies are designed to ensure that the implementation of protection mechanisms does not compromise the functionality of the system. This class of policies ensures that the system operates smoothly without facing any starvation during its execution. A typical liveness policy incorporates the response (grant or reject) mechanism following a request made by an IP for a resource. Violating such a policy can result in a livelock or deadlock situation, which can compromise the availability requirements of the system. By adhering to liveness policies, the system maintains its ability to perform its intended functions smoothly and continuously.

• •

  Time-of-Check vs. Time-of-Use (TOCTOU):
  TOCTOU policies aim to prevent the bypassing or spoofing of authentication mechanisms implemented for access control. These policies ensure that the authenticated agent is the one who is indeed accessing the asset for which it has been granted access. A crucial example of a Time-of-Check vs. Time-of-Use requirement arises in the context of firmware updates. In this scenario, the policy requires that the installed firmware during the updation process matches the previously authenticated firmware as mandated by the security engine. By enforcing TOCTOU policies, the system safeguards against unauthorized or tampered firmware, maintaining the integrity and security of the system’s critical components.

The subsequent categories provide a glimpse into the diverse requirements that need to be considered for on-chip communications in an SoC.

• •

  Message immutability: When an IP sends a message to another IP, then it is crucial that the message received by the receiver IP is precisely identical to the message sent by the sender IP.

• •

  Redirection and masquerade prevention: When an IP transmits a message to another IP, then it is essential that the message is successfully delivered to the receiver IP without any compromise. It should be infeasible for a potentially rogue IP to masquerade as the actual receiver IP or redirect to another IP other than the intended IP.

• •

  Non-observability: During transit, it is compulsory that a private message sent from one IP to another remains inaccessible to any other IP.

In many instances, security policies in SoC designs prioritize integration aspects over individual IPs. This approach means that the threat model mostly considers external attacks through software or the SoC interface with the system. However, the increasing adoption of 3rd party IPs offers a plug-and-play approach, allowing SoC design houses to meet tight time-to-market requirements using existing resources. As this trend continues, along with the static trust verification of IP designs, there arises a need to reevaluate and thoroughly analyze the trust model and assumptions underlying the current implementation of security policies in modern SoC designs.

In this work, we are focusing on enforcing different System Level Policies in any bus-based SoC.

The security of System-on-Chip (SoC) designs is contingent upon the trust assumptions made regarding the design components and entities involved in the supply chain. In the context of this paper, the trust model assumes an SoC integration house to be trusted which acquires third-party intellectual properties (3PIPs) from multiple vendors, each with varying levels of trustworthiness. In accordance with this trust model, the IPs themselves may not be deemed trustworthy; however, the bus wrappers and communication between the IP-level bus wrapper and the Security Policy Module are considered to be trusted. From the perspective of SoC integration, the inherent trust model assumes that IPs are acquired from the supply chain at the global level, while the specified components must be carefully planned and designed by the SoC integration house. IPs in modern SoCs are regularly categorized based on different levels of trust. Security Policies are implemented to confirm that untrusted entities do not adversely affect the secure assets or have the capability to endanger other system components.

Assumption 1: The currently proposed approaches assume the test and debug wrappers of the IPs to be trustworthy. In practice, the wrappers are designed in such a way that they are integrated into the SoC designs as infrastructure IPs to enable the debugging and testing tasks. Therefore, these test/debug wrappers have more stringent validation requirements than the conventional functional IPs in the SoC design. The wrappers are configured to monitor security-critical events and enforce the corresponding security policies.

Assumption 2: To achieve a secure architecture, designating certain components as trusted is crucial. If every component is susceptible to compromise, ensuring the overall system’s resilience becomes extremely challenging. SoC trust models aim to protect assets from malicious activities of entities which include IP vendors, SoC integration houses, foundries, test and validation facilities, etc. The underlying trust model assumes that the design components, such as Security Policy Module, Bus-level Wrappers, etc., specifically introduced for enforcing security policies are trusted, while individual IPs may be untrusted.

To ensure the effective protection of assets, designers must establish security policies outlining protection requirements while also understanding the capabilities of potential adversaries. The effectiveness of security mechanisms in SoC designs relies on the realism of the adversary model considered during the development of protection strategies. It is essential to acknowledge that adversaries can vary depending on the specific asset being safeguarded. For example, DRM keys might consider end users as potential adversaries, while system manufacturers could be seen as potential threats to the secrecy of sensitive information. The process of defining and categorizing potential adversaries involves careful consideration and creativity while considering the factors like the physical access adversaries have to the system and their ability to observe, control, modify, or reverse-engineer components. By taking these factors into account, designers can develop more targeted and robust security measures to address the specific threats faced by the system. This approach enhances the overall resilience and reliability of the SoC design. In this work, we considered the following threat models in the context of securing assets in an SoC:

• •

  Access Control Violation
  This threat model involves an adversary attempting to gain unauthorized access to the SoC, bypassing security measures or exploiting vulnerabilities to gain control over the system or access sensitive information.

• •

  Denial of Service (DoS)
  Adversaries in this threat model aim to disrupt or degrade the functionality of a bus-based SoC, rendering it unavailable or causing it to perform poorly. This can be achieved by flooding the system with excessive requests, exploiting resource limitations, introducing faults, etc.

• •

  Information Leakage
  This threat model focuses on adversaries attempting to extract sensitive information from the SoC, such as encryption keys, confidential data etc., propagated or leaked through any observable point such as primary outputs, DFT, or DFD infrastructures.

• •

  Side-Channel Leakage
  This threat model relies on the information obtained through side-channel leakage that allows an attacker to infer sensitive information by analyzing timing, power consumption, or electromagnetic emanation from the system. Such vulnerabilities can potentially expose critical information, making them a significant concern in SoC security.

• •

  Reverse Engineering
  This threat model involves adversaries attempting to reverse engineer the bus-based SoC to understand its internal workings, identify vulnerabilities, or extract proprietary information.

• •

  Tampering
  In this threat model, the attacker aims to disrupt or modify the connectivity service in a bus-based SoC, either physically or through remote means, to manipulate its behavior, compromise its integrity, or extract sensitive data.

It is important to note that extensive research has been conducted on specific attacks within these categories, but a detailed exploration of each model and attack is beyond the scope of this paper.

The early research during the 80s and 90s on security policies in a computing system was primarily focused on information security [1] and developing a framework for analyzing the information flow and defining access control ([2],[3]). However, the process of identifying and defining the policies was not found to be scalable for complex designs. Some researchers focused on developing languages to define security policies using formal representation. X. Li et al. [4] proposed a typed language called SAPPER which provides a synthesis framework for certain security policies. Some designers opted for other powerful languages, such as Property Specification Language or PSL ([15]), for defining and implementing security policies. Several researchers proposed another direction by representing security policies mapped to a specific class of Security Property. These properties can be tested statically using formal tools such as model checking [5], equivalence checking [6], and information flow tracking techniques ([7],[8],[10],[22]) for detecting information leakage, especially in cryptographic designs that cause confidentiality and integrity property violation. A technique named Gate-Level Information Flow Tracking (GLIFT) has been introduced to detect and measure illegal flows of a corrupted value at the Boolean level ([9]). Jin et al. [13, 14] proposed an analog on-chip neural network capable of detecting suspicious activity based on sensor measurements. Checking information flow helps to detect information leakage, which may infer the existence of Hardware Trojans [11].

There have been several works focused on developing security properties in the context of security verification and validation. These properties facilitate the verification of specific assumptions, requirements, conditions and the desired behaviors within a design. They formally describe the expected behaviors of the design concerning a particular security vulnerability. Evaluating the coverage of security properties can be used as a measure to assess the overall security of a SoC design. Authors in [21] proposed an automated property generation for information flow properties for hardware designs. Farzana et al. [19] created a database of security properties and generated equivalent assertions to verify them using appropriate tool sets ([20]) for identifying vulnerabilities in a design.

Ray et al. [16] discussed about incorporating security policies becoming an area of significant research activities with the advancements of modern SoC designs involving third-party IPs. The research directed towards incorporating a dedicated security IP for providing system-level protection for SoCs with untrusted IPs emerged as one of the viable solutions against diverse attacks. Wang et al. [17] proposed an infrastructure IP (IIPS) for SoC security architecture but limited to preventing low-level hardware security vulnerabilities. Basak et al. ([12, 18]) extended the IIPS framework and presented a microcontroller-based framework for implementing certain classes of security policies. Nath et al. ([26]) proposed Reconfigurable Security Policy Engine (RSPE), which can act as a smart security wrapper interfaced with the on-chip Design-for-Debug (DfD) interface for monitoring security-critical events and incorporating necessary mitigatory actions. Huang et al. [23] proposed an architecture called MSIPS that involves dedicated security IPs for enforcing security policies for protecting against H/W Trojan attacks, IP theft attacks, and some behavioral threats.

Existing mechanisms typically address threats occurring individually during runtime at either the architecture level or IP core level and incorporate dedicated security IPs to withstand a common set of security threats. However, the current methodologies lack the flexibility to represent different security requirements and define actionable specifications using a high-level formal representation for any bus-based design. Our proposed architecture is capable of generating a synthesizable centralized module with minimal overhead for enforcing security requirements through policies from given user specifications.

This section provides an overview of the experimental setup and analysis of the obtained results to evaluate the performance of the proposed framework. To assess its effectiveness, we selected the CEP (Common Evaluation Platform), an open-source SoC benchmark developed by MIT, as our testing and evaluation platform. The CEP benchmark comprises various components, including the Mor1kx OpenRISC processor, which acts as the Master IP, and a set of Slave IPs with diverse functionalities. These Slave IPs consist of several cryptographic modules, such as AES, DES3, RSA, MD5, and SHA-256, as well as digital signal-processing modules like DFT, IDFT, FIR, IIR, and a GPS module. Additionally, there are certain modules like JTAG, GPIO, UART, etc., which facilitate external communication with the user. However, it is important to note that these modules may serve as potential attack surfaces and are therefore considered untrusted IPs. Fig. 6 illustrates a basic block diagram of the SoC benchmark used in our experiment. We have categorized the Crypto and DSP modules along with the open-source RISC processor as the master IP and the potentially insecure IPs communicating through the AXI4 bus interconnect.

The enforcement of the security policy is illustrated in Fig. 7. It demonstrates that when the address range falls within a protected region, the Master is prevented from writing $write\_data$ to the designated location. The diagram shows a snapshot of the communication between the Master IP (Processor) as the sender and the Slave IP (Memory) as the receiver, with other slave IPs connected through the bus interconnect. We have provided a description of the bus transactions for each IP, along with the enforcement of a relevant security policy at the bus level. A centralized module monitors all observable bus signals and updates their values if they do not comply with the security mandates. The bus transaction begins with the master sending the write data to a valid address value (0x0001dfa8) in the memory as indicated by the $aw\_valid$ signal. However, the underlying security policy restricts the writing of data between the address range starting at 0x0001dfa4 and ending at 0x0001ffac in memory as it contains sensitive data. Hence, the centralized policy module modifies the current bus transaction by updating the $w\_data$ to 0x0000000 and setting the $w\_valid$ to 0, which will restrict the writing of data in memory. The IPs involved in the bus transaction with the updation of values in the read/write channel are marked with red signs, while the slave IPs not involved in the transaction and have no updation to the read/write channel are marked as green.

Table V represents a few example security policies applicable for either master or slave or both IPs and the policy representation in 3-tuple format with corresponding SystemVerilog construct for enforcement of each policy.

In the context of security verification, a security property serves as a statement to examine inferences, prerequisites, assumptions, and expected behaviors within a design. This statement can take the form of an assertion or a cover statement. Assertions are utilized to verify correct functioning and detect invalid events that may induce potential threats, while cover statements help in obtaining coverage information during the validation process of the design. Security properties can be categorized as immediate, checking specific scenarios at an instance of time, or concurrent, scrutinizing the behavior over a certain timeframe for the whole module. Concurrent assertions, being more potent, can express more complex events. Designers typically opt for assertion languages like PSL and SystemVerilog Assertions, which utilize logic representations at the temporal level like LTL and CTL ([24, 25]) to describe design behaviors. Various tools and methodologies are employed to verify the extracted security properties. Integrity properties, for instance, can be efficiently checked using model-checking tools, which excel in analyzing intricate systems to ensure correctness. In contrast, confidentiality properties are better assessed using information flow tracking and taint analysis techniques. These approaches can trace potential leaks of sensitive information to observable points within the design. Additionally, to examine properties related to secure design transformation, equivalence-checking tools are utilized, enabling verification of whether two designs exhibit identical behaviors.

Unlike non-synthesizable security properties, the proposed method incorporates DiSPEL tool that generates synthesizable RTL code in SystemVerilog. This enforces security policies for any bus-based SoC architecture. The synthesizable SystemVerilog code can be verified using simulation using any industry standard simulator, and it can also be verified on FPGA. The generated SystemVerilog code of the centralized module that enforces security policies inserted between the IPs and bus interconnect by the tool can be converted to a gate-level netlist using any standard EDA tools. Hence, the proposed architecture can be easily integrated into both ASIC and FPGA flow methodologies of any bus-based SoC design.

Let us discuss an illustrative example to differentiate between security policy and security property.
Security Requirement: The secret key (K) should not be leaked (partially or fully) through Ciphertext (ct).

The representative overhead values for the IPs were obtained by synthesizing them at a 250nm standard cell library using Synopsys Design Compiler. Table VII represents the overhead results in terms of area, delay, and power consumption for the centralized policy module implemented with different numbers of policies. Table VIII demonstrates the extra incurred overhead for different IPs with different numbers of IP-level policies implemented. The results clearly demonstrate that the overheads are generally minimal under default synthesis settings without constraints. In certain cases, the overall overheads are even reduced after re-synthesizing with the implementation of the security policy module due to internal heuristic optimizations. Hence, we can conclude that our proposed methodology, which enforces security requirements through policies in a generic bus-based SoC design, imposes minimal overheads and is practically feasible to implement.

The waveform analysis was a critical aspect of our experiment as it affirmed the effectiveness of enforcing a security policy that addresses the requirement of safeguarding private keys from untrusted IPs during transit. We generated the waveforms from the simulation using Synopsys VCS (Verilog Compiler Simulator) and employed a graphical user interface using DVE (Discovery Virtualization Environment) for viewing waveforms. For our experiment, we utilized Synopsys VCS Version: T-2022.06-SP2 and DVE Version: T-2022.06_Full64 for analyzing the waveforms. We have illustrated the successful enforcement of the security policies explained in Table V through representative timing diagrams of related bus signals for the IPs involved in Fig. 8. The demonstration clearly portrays that the private keys in the write channel of the AXI bus are only accessible to the intended AES IP but not exposed to untrusted IP.

The DiSPEL Tool provides the flexibility to meet design constraints, considering area, power, and delay overhead values. The tool employs a ranking scheme based on severity to prioritize policies. After synthesizing the centralized module and the updated IP modules with the policies enforced, the tool utilizes a feedback-based approach to verify if the constraints are satisfied. If the constraints are not met, the tool adopts an iterative process. It discards the bottom 10% of policies based on the score and performs re-synthesis to assess if the constraints are met in the subsequent iteration. This iterative process continues until the design constraints are successfully satisfied. Fig. 9 depicts multiple iterations for the SHA-256 module from our test SoC benchmark. The initial constraints were set to less than 5% allowed overhead for each area, power, and delay parameters. The designs are synthesized using 250nm standard cell library cells without any constraints. As shown in the figure, the initial synthesis resulted in violations of both power and delay overhead constraints. However, after discarding 10% of the policies and performing re-synthesis in the subsequent iterations, all the overhead constraints were eventually met for the module. The effectiveness of DiSPEL tool was further tested by applying time constraints-based synthesis and experimenting with different IP modules in multiple iterations until the allowed constraints were met.

The effectiveness of enforcing security policies can be demonstrated through simulation, while its correctness can be proved by formal verification. We have used Synopsys VCS (version: T-2022.06-SP2) for running the simulation tests for the overall SoC through bare metal code and unit-level simulation for each individual IP. The simulation results ensure the functional correctness of the design and allow for iterative design improvements and bug fixes if any violations are found.

We opted for one of the most commonly used formal verification tools in the semiconductor industry, namely Cadence JasperGold v2020.12, for verifying the correctness of the policies. We represented the policies in the form of SystemVerilog Assertions and analyzed them through JasperGold coverage analysis. We performed comprehensive validation of all the policies to ensure their compliance with the specified security requirements. Table IX illustrates the simulation status and formal verification results for an example access control security policy involving address range validation for crypto IPs of the SoC.