equivalent to τ0 and cτ1 and cτ2 are stronger than cτ0. After a careful inspection of cτ1 and

cτ2, we found the trigger condition is tj. l

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

Example 27. Let us consider the example given in Fig. 6.5. Consider the datapath shown in Fig. 6.5(a). The input in1 (an input that determines the loop bound) and count (loop variable) are inputs to the comparator and the output determines whether the loop body will be executed or not. We consider only the relevant part of the datapath to explain the effect of a downgrade attack. The datapath is modified as shown in Fig. 6.5(b) to introduce the attack. Specifically, an extra constant (i.e., in2) is introduced and is multiplexed with in1.

The output of the multiplexer depends on the trigger condition of the HT. If the trigger condition is True, the loop will iterate in2 times instead of in1 times. The value of the loop

bound is changed based on the trigger condition. l

Algorithm 7: Detect DG Attack (τ0, T1) Input: τ0,T1

Result: Instance of the downgrade (Trojan trigger condition)

1 ccomb =ϕ; //combined condition of traces

2 foreachτi PT1 do

3 //check ifcτi is stronger condition thancτ0

4 if (cτi Ñcτ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 downgrade attack is found in T1”.

9 else

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

#define nb 64

for(int i=0; i < nb; i++){

stmt[i*4] = ret[i*4];

} }

(a)

#define nb 64

nb = tj? 32 : nb;

for(int i=0; i < nb; i++){

stmt[i*4] = ret[i*4];

} }

(b)

Figure 6.6: (a) C Code from AES before adding tj, (b) Representative RTL-C after downgrade attack

Since the functionality has changed in this attack, our equivalence checking method will report a possible non-equivalence between the C-FSMD and the RTL-FSMD. In addition to that, the traces for which equivalence could not be found by the method will also be reported. These traces are corresponding to the block where functional changes are made by the tool. An attacker in the foundry or a rogue user can activate the Trojan after a predefined amount of time or by a specific input sequence. With the careful inspection of this information, the user can pinpoint the Trojan inserted by the HLS tool.

(a) (b)

!(i<nb) S1

S2

S3

S4 i=0 nb = 64

i < nb

stmt[i*4]= ret[i*4]

i = i + 1

t1

t2

t3

t4

t5 i=0

!tj/nb=64

stmt[i*4]= ret[i*4]

i = i + 1 tj/nb=32

i < nb

!(i < nb)

Figure 6.7: An example to illustrate the effect of downgrade attack: (a)C-FSMD (M0) obtained from the input C (Figure 6.6(a)) (b) RTL-FSMD (M1) obtained from the RTL-C (Figure6.6(b))

### 6.5.2 Detection

Downgrade attack (DG) compromises the circuit behaviour only when the Trojan is acti- vated. As long as the Trojan trigger is not activated, the design produces correct results and the Trojan stays undetected. We use our equivalent checker tool to detect the HT trigger condition for DG. In a DG attack, the number of traces in M0 and M1 are different due to the HT trigger condition. Specifically,M1 contains more traces than that ofM0. The overall downgrade attack detection mechanism is presented in Algorithm7. Algorithm7is invoked in Algorithm5 when our equivalent checker could not find equivalent of a trace ofτ0 of M0

inM1 in two scenarios (in line13and in line15). In the former case (line 13), the respective condition of executions have some overlapping but are not equivalent but the data trans- formations are equivalent. In the latter case (line 15)), both conditions of executions and the data transformations are not equivalent. In Algorithm7, we first identify a set of traces τi in the RTL-FSMD for which the condition of execution is stronger (stronger condition

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

is indicated by implication) than that τ0. Then, we check if the union of the condition of executions of all these traces ccomb turns out to be equivalent to the condition of executions of cτ0. This indicates that some spurious traces may be added to the RTL-FSMD by the attacker for implementing the DG attack. By a careful analysis of the traces involved in ccomb, we can figure out the spurious HT trigger condition of the downgrade attack, and the value of the loop counter is changed.

i = 0 nb =64

(a) s1

s1

stmt[0] = ret[0]

stmt[4] = ret[4]

stmt[63*4] = ret[63*4]

(b) i = 0 t1

t1

stmt[0] = ret[0]

stmt[4] = ret[4]

stmt[31*4] = ret[31*4]

tj/nb =32

. . .

i = 0

(c) t1

t1

stmt[0] = ret[0]

stmt[4] = ret[4]

stmt[63*4] = ret[63*4]

!tj/nb =64

. . .

Figure 6.8: An example to illustrate the effect of downgrade attack: (a) Trace of τ00 from C- FSMD obtained after unrolling (nb = 64) (b) Trace ofτ10from RTL-FSMD obtained after unrolling (nb = 32) (c) Trace of τ11 from RTL-FSMD obtained after unrolling (nb = 64)

Example 28. Consider the input C-code and the corresponding RTL-C (after HLS tool inserts Trojan) as shown in Fig. 6.6(a) and Fig. 6.6(b), respectively, and their corre- sponding FSMDs are shown Fig. 6.7(a) and Fig. 6.7(b), respectively. The traces of the respective behaviours are shown in Fig. 6.8. Specifically, the C-FSMD has one trace and the RTL-FSMD has two traces. During equivalence checking between traces in M0 and M1, the equivalence of τ00 could not be found. But, the Algorithm will select τ10 (or τ11) and Algorithm 7 will be called in line 13 (or line 15). Since cτ10 and cτ11 are stronger than cτ00 and pcτ10_cτ11q ” cτ00, the Algorithm 7 will report a possible DG attack. After a careful in- spection of the data transformation and condition of execution of of τ10 and τ11, we identify

Experimental Results

that the hardware Trigger condition tj and the value of loop count (variable) is decided by tj. The loop executes a reduced number of rounds (from 64 to 32) in case of HT activated.

In addition to loop count, the actual operations are also affected by the modification of the

loop count. l