BLAST: Belling the Black-Hat High-Level Synthesis Tool

when the Trojan trigger tj is True. As a result, for every iteration, there will be one cycle of degradation. The bubble is inserted inside the loop which iterates ntaps time. Therefore,

total degradation will be ntaps cycles. l

/i = 0

(a) C-FSMD s1

s2

s3

s4

s5

s6

-/c = i < ntaps

c/sum = h[i] * z[i]

-/i = i + 1

-/c = i < ntaps

!c/return sum

/i = 0

(b) RTL-FSMD t1

t2

t3

t4

t5

t6

-/c = i < ntaps

c/t1 = h[i]

-/i = i + 1, t3 = t1 * t2 -/c = i < ntaps,

Sum += t3

!c/return sum

t7 tj/t2 = z[i]

!tj/t2 = z[i]

Figure 6.4: An example to illustrate the effect of degradation attack: (a) C-FSMD obtained from the input C (b) RTL-FSMD obtained from the RTL after HT insertion

The DA will be detected during equivalence checking of two FSMDs (between C-FSMD and RTL-FSMD). The DA changes the behaviour of the controller FSM. As a result, the number of traces has increased in the RTL-FSMD and the condition of execution of some traces has also changed. As a result, the equivalence of a few traces of C-FSMD could not be found in RTL-FSMD. In such a situation, we will analyze to find a set of traces in RTL-FSMD whose union is equivalent to the trace in C-FSMD. With further analysis of the condition of executions of those traces, the DA can be detected. In the following, we briefly discuss the equivalence checking method followed by the detection of DA.

### 6.4.2 C to RTL Equivalence Checking

The primary challenge in C to RTL equivalence checking is the abstraction gap between the C and the RTL codes. Therefore, RTL-FSMD is abstracted first from the RTL using Algorithm 1 in chapter 3. We also represent the input C using C-FSMD. How the FSMD model can be constructed from the input C is discussed in detail in .

BLAST: Belling the Black-Hat High-Level Synthesis Tool

Algorithm 5: Detect DA DG Attack (C, RTL)

Input: C is the input C to HLS, RTL is generated by a HLS tool from C Result: Equivalent, detect degradation or downgrade attack

1 M0 = constructFSMD (C);

2 M1 = RTL-FSMD Extraction(RTL);

3 T0 = findTrace(M0);T1 = findTrace(M1);

4 while(T0 ‰ϕ) do

5 τ0 = select a trace fromT0;

6 TC = getTestcase(τ0);

7 τ1 = getCorrespondingTrace(T1, TC);

8 if ppcτ0 ”cτ1q ^ psτ0 ”sτ1qqthen

9 //τ0 andτ1 are equivalent

10 removeTrace (τ1,T1);

11 else if {(cτ0 ^cτ1‰ ϕ) ^ psτ0 ”sτ1q}then

12 Detect DA Attack (τ0,T1);//Algorithm6

13 if (not DA) then

14 Detect DG Attack (τ0,T1);//Algorithm7

15 else if {(cτ0 ^cτ1 ‰ϕ)^ psτ0 ‰sτ1q} then

16 Detect DG Attack (τ0,T1);//Algorithm7

17 removeTrace (τ0,T0);

18 if (no DA or DG) then

19 Report “No attack is found”;

The Algorithm5is used to detect degradation and downgrade attacks. The equivalence checking method used here is adapted from Algorithm 2 in chapter 4. The algorithm examines whether the trace pairs of C-FSMD and RTL-FSMD are equivalent or not. In our method (Algorithm 5), we do not use the merging compatible (traces that have the same output) trace concept. The merged trace condition of execution is represented as the union of traces that are merged. As a result, the effect of HTs may not be shown. However, in the s adapted algorithm, we include techniques whose goal is to detect degradation attacks and downgrade attacks. The algorithmic steps are described briefly below.

1. Generate all traces in both the behaviours: All the traces of both behaviours input C (M0) and RTL-c (M1) have been extracted and assigned to the sets T0 and T1, respectively.

The tool Klee  has been used for this purpose. We have modified Klee’s source code to get the symbolic the data transformation (sτ) and the condition of execution (cτ) of a trace τ inM0 and M1.

2. Find potential corresponding traces between two behaviours: For checking the equivalence between M0 and M1, we need to check equivalence between the traces. A naive algorithm will take Opn2q comparison (n is the number of traces in a FSMD) to find the equivalence because it will compare each trace in M0 with all traces in M1 (to the worst case) to find the equivalence. To reduce complexity, a data-driven approach is taken to find the potential corresponding traces betweenT0 andT1. Klee gives a test case for each trace in a behaviour.

Hence, we know the values of input variables (test case) for each trace τ0 in T0. Now, we can runT1 with this test case and find the trace τ1 which is followed for this particular test case. Lines5-7of Algorithm 5implements this idea. This data-driven approach will reduce the complexity of equivalence checking to Opnq comparisons.

3. Equivalence checking of traces between two behaviours: Finally, the trace-wise equiva- lence of potential correspondent traces is checked using SMT solver Z3 in this work. A potential corresponding trace pair are equivalent if their respective condition of executions and data transformations are equivalent (in lines 8-10). If they are not equivalent(in lines 12-14), we check for possible instance of degradation or downgrade attacks.

### 6.4.3 Detection

We can detect degradation attacks with the help of the equivalence checker tool. The tool will give us the trace level equivalence between the C-FSMD and RTL-FSMD. As shown in , this bubble effectively creates an alternative trace in the behaviour with no effective operation inside it. Therefore, our objective is to identify such spurious traces in the RTL- FSMD. It may be noted that each of these traces is associated with a condition (i.e., the trigger of the Trojan) and those conditions are not present in the initial behaviour. During equivalence checking, therefore, the equivalent trace cannot be found for these traces. Let p:xqi ñqjy be one path from the state qi to qj in the RTL-FSMD in which the condition to enable the HT is incorporated by the attacker. In fact, there will be another parallel path (or a set of paths) from qi in RTL-FSMD which is associated with the negation of the trigger condition. It is, therefore, possible to find two (or a set of) traces in RTL-FSMD through qi and qj whose union will be equivalent to the corresponding trace in C-FSMD.

By analyzing the conditions of these traces, the HT trigger condition will be identified.

The overall degradation attack detection mechanism is presented in Algorithm 6. The Algorithm 6 invokes in line 12 of Algorithm 5 when the equivalence of τ0 of M0 and τ1 of

BLAST: Belling the Black-Hat High-Level Synthesis Tool

M1 cannot be shown because the respective condition of executions are not equivalent but their intersection is not NULL (i.e., there is some common condition of executions between them). In Algorithm 6, we first identify a set of traces in the RTL-FSMD M1 each of them has a stronger condition of execution than that ofτ0 of C-FSMDM0. The stronger condition of execution is indicated by implication in line 4 of the Algorithm 6. Then, we check if the union of condition of executions of all these traces turns out to be equivalent to thecτ0. This indicates that some spurious traces may be added in the RTL-FSMD by the attacker for implementing DA or DG attacks. A trace of C-FSMD can also be split into multiple traces in RTL-FSMD during scheduling as shown in . In such case, a possible DA attack will be detected which is false positive. Therefore, a careful manual inspection of the condition of executions of the traces will identify if any spurious HT trigger condition is added in the RTL-FSMD.

Algorithm 6: Detect DA Attack (τ0,T1) Input: τ0,T1

Result: Instance of the degradation (Trojan trigger condition)

1 ccomb =ϕ; //combined condition of traces

2 foreachτi PT1 do

3 check ifcτi is stronger condition than cτ0 and data transformations match

4 if ((cτi Ñcτ0 ^ sτi ”sτ0)) then

5 ccomb“ccomb_ cτi;

6 //check the union of the strong conditioncτi is equal to condition cτ0

7 if (ccomb”cτ0) then

8 Report “Possible degradation attack is found in T1”.

9 else

10 Report “No degradation attack is found in T1.”

Example 26. Consider the FSMDs in Fig. 6.4. During checking equivalence from the corresponding states pair xs1, t1y, the equivalence checking method (given as Algorithm 5) could not found any equivalence for a trace τ0 “ s1 Ñ s2 Ñ ps3 ÝÑc s4 Ñ s5 ÝÑc s6 Ñ s3qntaps Ñs1 of C-FSMD in Fig. 6.4(a) in the RTL-FSMD in Fig. 6.4(b). Then Algorithm 5 calls Algorithm 6 to check a possible instance of degradation attack. It found two traces τ1 “ t1 Ñ t2 Ñ pt3 ÝÑc t4 ÝÑtj t7 Ñ t5 Ñ t6 ÑÝc t3qntaps Ñ t1 and τ2 “ t1 Ñ t2 Ñ pt3 ÝÑc t4Ý!tjÑt5 Ñt6 ÝÑc t3qntaps Ñt1 in the RTL-FSMD such that union of these two traces are