Advertisement

Design Techniques for Hardware Trojans Prevention and Detection at the Register-Transfer Level

  • Hassan Salmani
Chapter
  • 566 Downloads

Abstract

Outsourcing design development and extensive usage of untrusted intellectual properties make modern complex designs highly susceptible to hardware Trojan insertion at the register-transfer level. As existing pre-silicon verification techniques are not designed toward hardware Trojans, there is need for hardware Trojan prevention and detection techniques at the register-transfer level to ensure the trustworthiness of designs. This chapter reviews and discusses some of proposed techniques for hardware Trojan prevention and detection at the register-transfer level.

3.1 Hardware Trojan Prevention at the Register-Transfer Level

3.1.1 Dual Modular Redundant Schedule at High-Level Synthesis

Dual Modular Redundant (DMR) schedule during High-Level Synthesis (HLS) has been proposed to ensure security against hardware Trojans at the register-transfer level [3]. The technique targets hardware Trojans in third-party intellectual properties (3PIPs) that only cause computational output value change (and produces no other impact). Only a third-party vendor is considered untrustworthy, and an adversary or rogue designer only in the third-party house can manipulate the modules/IPs such as decoders, comparators, and multipliers.

Conversion of a circuit behavioral description into its corresponding register-transfer level structure is accomplished through HLS which involves the process of design space exploration (DSE) that includes evaluation of alternative candidate design solutions based on objectives such as area and delay. The conversion process involves multiple subprocesses such as scheduling, allocation, and binding. The process of DSE becomes convoluted with the involvement of an auxiliary variable called loop unrolling factor for control-data flow graph (CDFG) applications as it adds an extra dimension to explore based on conflicting user constraints of area and delay. Loop unrolling plays an important significance in dictating the final area and delay of a design.

Figure 3.1 presents the flow for low-cost security aware high-level synthesis solution for hardware Trojan secured datapath [3]. The aim of proposed approach is to explore the design space of a hardware Trojan Secured DMR schedule comprising of candidate solutions for DMR schedule resource configurations (architecture), candidate loop unrolling factor, and candidate vendor assignment procedure, all hybrid encoded.
Fig. 3.1

The flow for low-cost security aware high-level synthesis solution for hardware Trojan secured datapath [3]

A solution for Trojan secured DMR schedule is an optimal X i where {X i } = {N(R1), N(R2), …, N(R d ), U, P v }, while exploring the design space of a given CDFG and satisfying conflicting user constraints and minimizing the overall cost. X i indicates a resource set of a particular particle solution with unrolling and allocation procedure information; N(R1), N(R2), …, N(R d ) indicates the number of instances of resource type ‘1’, …,‘d’; U indicates the unrolling factor; and P v indicates vendor allocation procedure type. The problem is formulated as minimizing Hybrid \(Cost(A^{DMR}_T, T^{DMR}_E)\), for optimal {X i }, subjected to \(A^{DMR}_T < A_{cons}\) and \(T^{DMR}_E < T_{cons}\) and hardware Trojan security. \(A^{DMR}_T\) indicates the total area of a DMR design; A cons indicates the user-specified area constraint; \(T^{DMR}_E\) indicates the total execution time of a DMR design; and T cons indicates the user specified execution time constraint. The loop unrolling transformation duplicates the body of the loop multiple times controlled by U (The unrolling factor) to expose additional parallelism that may be available across loop iterations. P v is the vendor allocation procedure capable of holding only a binary value (where P v  = ‘1’ indicates all operations of a specific unit being strictly assigned to resources of the same vendor type, for example, all operations of original unit strictly assigned to the same vendor V1 and all operations of duplication to the other vendor V2; while P v  = ‘0’ indicates alternate vendor assignment to operations in a control step of a unit). The variable P v is crucial for hardware Trojan secured schedule optimization, as both P v  = ‘0’ and P v  = ‘1’ provide vendor distinctness in DMR design resulting in hardware Trojan security.

For hardware Trojan detection in 3PIPs that only change computational output value (and produces no other impact), minimum two distinct third-party vendors are required. Even if the IPs from two different vendors have different timing, but functional similarity of two distinct IPs, allow for comparison at the DMR output. In the proposed approach we only require two distinct vendors for generating a hardware Trojan secured schedule. The technique optimizes the cost of solution by regulating the internal allocation process of two distinct vendors within DMR schedule through a variable P v during exploration. Imposing a diverse set of 3PIP vendors as security constraints during allocation step for similar operations in DMR design during HLS provides detection of malicious output. The technique simultaneously explores an optimal schedule and optimal U combination for a low-cost hardware Trojan security aware DMR schedule using the Particle Swarm Optimization (PSO) algorithm.

To obtain a hardware Trojan secured DMR schedule, its corresponding DMR schedule is first obtained. The complete duplication is done for all the unrolled operations of the CDFG based on U. Once operations of the CDFG are unrolled, then both the operations of original unit and duplicate unit are concurrently scheduled based on the information of the schedule architecture (N(R1), N(R2), …, N(R d )) in the candidate design solution (X i ). This enables to determine the final delay \(C^{DMR}_T\). The DMR logic uses a specific vendor allocation rule to design a hardware Trojan secured schedule. The vendor allocation rule states that two distinct vendors are required for operation assignment in DMR such that the similar operations v of original unit (W OG ) and v′ of duplicate unit (W DP ) are assigned to the distinct vendors. This enables hardware Trojan detection as for cases where no sub-IP exists, it is highly unlikely that different hardware Trojans in different 3PIPs will produce identical wrong outputs. The distinct vendor assignment rule for hardware Trojan detection can be realized in various ways; therefore, the PSO algorithm is used to obtain the most optimal distinct vendor allocation.

3.1.2 Proof-Carrying Hardware

It is possible to express properties of systems in the form of logical statements, and then use theorem provers to prove or disprove the properties of systems expressed as logical statements. The proof-carrying hardware (PCH) framework integrates interactive theorem prover and SAT solvers (shown in Fig. 3.2) to verify security properties of register-transfer level designs [1]. The approach is based on the proof-carrying code (PCC). In PCC, a software customer provides safety properties and untrusted software vendor develops safety proof for these properties. Afterwards, the vendor submits the customer a PCC binary file that includes the formal proof of the safety properties encoded along with the executable code of the software. The customer then validates the PCC binary file using its own proof checker.
Fig. 3.2

Working procedure of the PCH framework [1]

Note that the PCH framework does not provide protection against hardware Trojans whose behaviors and attributes are not captured by the set of security properties. Furthermore, there is also an assumption that the attacker has detailed knowledge of the design to identify critical registers and modify them in order to carry out the attack.

In PCH framework, Hoare-logic style reasoning is used to prove the correctness of the RTL code and implementation is carried out using the Coq proof assistant. Coq is indeed a formal proof management system that provides a formal language to write mathematical definitions, executable algorithms, and theorems, as terms in the Gallina specification language, together with an environment for semi-interactive development of machine-checked proofs. In its original implementation, Coq does not recognize hardware description languages and security properties expressed in a natural language. The PCH framework integrates the semantic translation of HDLs and informal security specifications to the Calculus of Inductive Construction (CIC). In the PCH framework, an IP customer provides both functional specifications and a set of security properties to an IP vendor. The functional specifications are materialized into HDL codes. Then the HDL codes and security properties are translated to CIC. Proofs are constructed for security theorems and the transformed HDL code. The HDL code and proof for security properties are combined into a trusted bundle and delivered to the IP customer. The IP customer first generates the formal representation of the design and security properties in CIC. The translated code, combined with formal theorems and proofs, was quickly validated using the proof checker in Coq platform.

3.2 Hardware Trojan Detection at the Register-Transfer Level

3.2.1 Control-Flow Subgraph Matching

A verification approach is proposed to detect hardware Trojan at the register-transfer level by exploiting an efficient control-flow subgraph matching algorithm [2]. For a process P of a design under verification (DUV) at RTL, a control-flow graph (CFG) for P is a tuple CFG(P) = (B, E, ρ, s, e) where B = b1, …, bn is the finite set of basic blocks, that is, sequences of consecutive instructions without any branch; E ⊆ B × B is the finite set of edges between the blocks such that (b1, b2) ∈ E if and only if b2 can be executed after b1 in at least one of the possible executions of the process P; ρ : E → (0, 1] is the function such that ρ(b1, b2) is the probability that b2 follows b1 during an execution of P; s, e ∈ B are the first and last basic blocks, respectively.

Figure 3.3 presents the overview of the proposed approach. The inputs are the design under verification (DUV) and a hardware Trojan library at the register-transfer level. Three scenarios of hardware Trojans insertion at RTL are considered: (1) an in-house rogue designer intentionally hides malicious behavior in the RTL modules before design verification and synthesis steps; (2) third-party RTL modules provided by untrusted parties have already been manipulated and contain hardware Trojans; and (3) a hardware Trojan might be automatically inserted by a computer-aided design tool used for design syntheses and analyses. Considering the different hardware Trojan insertion scenarios, a hardware Trojan library is developed based on known hardware Trojan triggers and their camouflaged variants. The hardware Trojan triggers are classified in three categories: cheat code, dead machines, and time bombs as samples of them are shown in Fig. 3.4.
Fig. 3.3

Hardware Trojan detection at the register-transfer level using control-flow subgraph matching [2]

Fig. 3.4

Examples of the CFGs of hardware Trojan triggers in the proposed hardware Trojan library. The dashed boxes represent the instructions (in pseudo-code) inserted in the basic blocks associated to the nodes. In case of a node with two outgoing edges, the left and the right edges correspond to the case in which the branching condition evaluated in the node is true and false, respectively [2]. (a) Cheat code. (b) Dead machine. (c) Ticking time bomb

A cheat code is a value (or sequence of values) that enables the payload upon observation. Figure 3.4a presents an example of CFG of a cheat code’s trigger based on two processes. A dead machine activates the hardware Trojan when specific state-based conditions are met. It can be indeed considered a generalization of cheat code hardware Trojans to realize more complex conditions for hardware Trojan activation. Figure 3.4b shows a possible implementation. A ticking time bomb enables the payload when a certain number N of clock cycles has been counted. In fact, if N is sufficiently high, dynamic methods require long simulations, while formal approaches face the state explosion problem. Figure 3.4c illustrates the CFG of a possible implementation of this trigger based on two processes. The hardware Trojan library includes a basic implementation and a configuration file for each of the aforementioned hardware Trojan triggers. The basic implementation is the simplest form of the trigger’s code. The configuration file makes the triggers parametric using extension directives and confidence directives. The extension directives are used to automatically modify the CFG of the trigger’s basic implementations. This would make it possible for the hardware Trojan detection technique to stay resilient against various implementation of one hardware Trojan trigger. The confidence directives are used to define the structural characteristics of the trigger’s CFG. The detection algorithm checks the structural characteristics to determine a confidence value and to avoid false positive, after a possible instance of a HT is found in the DUV.

After establishing the hardware Trojan library, the extraction algorithm is executed. The extraction algorithm creates the CFG for the RTL DUV for each process included in the DUV. The algorithm generates the CFGs of the triggers and payloads included in the HT library as well. In this way, both the structures of the DUV and the HTs are represented with graph-based models that highlight their execution paths and simplify the detection of HTs. In the following, the detection algorithm identifies the HTs by using a subgraph isomorphism algorithm. First, it looks for the parts of the CFG of the DUV that match the CFGs extracted from the triggers of the HT library. Afterward, it analyzes the matched instances to provide confidence values that help discard the false positives. The confidence values take into account the structural characteristics of the CFGs and the related payloads.

Some hardware Trojans can be similar to actual legal code, so it is necessary to give a confidence value for each match returned by the detection algorithm. Four characteristics are considered to determine the confidence value of the match: (c1) presence of variables, (c2) presence of the reset logic, (c3) average distance of the probabilities of the match and the corresponding pattern, and (c4) degree of dependence between the match and the most affine payload. The c1 verifies if the match uses some variables in the same way of the corresponding pattern. For example, in the case of time bomb, it checks if there is a variable used as a counter in the match, but not necessarily with the same name of one in the trigger. The c2 checks if the match has a reset logic similar to the reset logic of the pattern. For example, in the case of time bomb, it checks if a variable (counter) is reset whenever the DUV is reset. The c3 calculates the distance between the probabilities of traversing each edge in the match and the expected probabilities for traversing the corresponding edges in the pattern; nearer are the probabilities, more is likely that the match is a real instance of the pattern. The c4 verifies if there are shared variables, that is, registers, between the match and one of the payloads specified in the HT library. To determine final confidence level (β), the four values are linearly combined as β = α1 × c1 + α2 × c2 + α3 × c3 + α4 × c4 where α i depends on the trigger and \(\sum \nolimits _{i} \alpha _i = 1\).

3.3 Conclusions

This chapter reviewed some major works in hardware Trojan prevention and detection at the register-transfer level. Some techniques have suggested the incorporation of various vendors at a fine granularity to prevent hardware Trojan activation. Some have relied on the existence of a hardware Trojan library and searched into a design data/control graph to find subgraphs may match possible hardware Trojans. Embedding security properties into circuit development for later checking has been also recommended with assumption that hardware Trojans behaviors and attributes are known. While the techniques are successful in their goals, their limitations in scalability to large design yet require thorough analyses as they may incur significant area, power, and performance overhead. Further, their evaluation time may considerably increases as designs become larger and more complex. One share assumption among many hardware Trojan detection techniques is the need for a hardware Trojan library that is a challenging issue.

References

  1. 1.
    E. Love, Y. Jin, Y. Makris, Proof-carrying hardware intellectual property: a pathway to trusted module acquisition. IEEE Trans. Inf. Forensics Secur. 7(1), 25–40 (2012)CrossRefGoogle Scholar
  2. 2.
    L. Piccolboni, A. Menon, G. Pravadelli, Efficient control-flow subgraph matching for detecting hardware Trojans in RTL models. ACM Trans. Embed. Comput. Syst. 16(5s), 137:1–137:19 (2017)Google Scholar
  3. 3.
    A. Sengupta, S. Bhadauria, S.P. Mohanty, TL-HLS: methodology for low cost hardware Trojan security aware scheduling with optimal loop unrolling factor during high level synthesis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 36(4), 655–668 (2017)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Hassan Salmani
    • 1
  1. 1.EECS DepartmentHoward UniversityWashington, DCUSA

Personalised recommendations