FuCEFuzzing+Concolic执行引导的可综合硬件设计中的特洛伊木马检测

版权申诉

115 浏览量 2022-01-16 16:42:36 上传评论收藏 902KB PDF 举报

资源推荐

资源详情

资源评论

FuCE: Fuzzing+Concolic Execution guided Trojan Detection in Synthesizable

Hardware Designs

MUKTA DEBNATH

∗

, Indian Statistical Institute, India

ANIMESH BASAK CHOWDHURY

∗

, New York University, USA

DEBASRI SAHA, A.K. Chowdhury School of IT,University of Calcutta, India

SUSMITA SUR-KOLAY, Indian Statistical Institute, India

High-level synthesis (HLS) is the next emerging trend for designing complex customized architectures for applications such as

Machine Learning, Video Processing. It provides a higher level of abstraction and freedom to hardware engineers to perform hardware

software co-design. However, it opens up a new gateway to attackers to insert hardware trojans. Such trojans are semantically more

meaningful and stealthy, compared to gate-level trojans and therefore are hard-to-detect using state-of-the-art gate-level trojan

detection techniques. Although recent works [

] have proposed detection mechanisms to uncover such stealthy trojans in

high-level synthesis (

HLS

) designs, these techniques are either specially curated for existing trojan benchmarks or may run into

scalability issues for large designs. In this work, we leverage the power of greybox fuzzing combined with concolic execution to

explore deeper segments of design and uncover stealthy trojans. Experimental results show that our proposed framework is able to

automatically detect trojans faster with fewer test cases, while attaining notable branch coverage, without any manual pre-processing

analysis.

Keywords

: Hardware Trojan, High-level Synthesis, Greybox fuzzing, Symbolic Execution, Test-pattern generation and Fault Simulation

1 INTRODUCTION

In recent times, hardware designers are increasingly using commercial-o-the-shelf (

COTS

) third-party intellectual

property (3PIP) for designing complex architectures [

]. For ease of automated design space exploration and functional

verication, designers are adopting

HLS

framework like SystemC, synthesizable C/C++. As the designs have become

increasingly more complex, chip designers build complex system-on-chips using 3PIPs of required functionalities and

integrate them in-house. Post integration, these system-on-chips are outsourced to o-shore fabrication facilities. This

typical chip design ow has enabled 3PIP vendors to maliciously inject stealthy bugs at a higher abstraction level

that can later be exploited by the attacker to cause malfunction. Thus, verifying the security aspects of such 3PIPs is

primarily important for the in-house integrator apart from ensuring correct functionality.

Hardware Trojans at high-level synthesized designs have been recently explored in [

], where the attacker injects

malicious functionality either by leaking crucial information or corrupt nal output of design-under-test (

DUT

Although there exists a plethora of work to detect hardware trojans at register-transfer level (

RTL

) or gate-level designs,

these detection mechanisms are biased towards certain types of gate-level trojans. The trojans inserted at a higher

abstraction level are semantically meaningful and stealthy, but dicult for the defender to precisely detect any abnormal

functionality. An attacker can manifest a trojan by simply adding an

RTL

statement that uses hardware blocks designed

for other functionalities. This motivates performing security testing on high-level synthesized designs.

∗

Equal contribution while at Indian Statistical Institute

Authors’ addresses: Mukta Debnath, mukta_t@isical.ac.in, Indian Statistical Institute, Kolkata, India; Animesh Basak Chowdhury, abc586@nyu.edu,

New York University, New York, USA; Debasri Saha, debasri_cu@yahoo.in, A.K. Chowdhury School of IT,University of Calcutta, Kolkata, India; Susmita

Sur-Kolay, ssk@isical.ac.in, Indian Statistical Institute, Kolkata, India.

arXiv:2111.00805v1 [cs.CR] 1 Nov 2021

ii Mukta Debnath, Animesh Basak Chowdhury, Debasri Saha, and Susmita Sur-Kolay

In this article, we propose a scalable trojan detection framework based on fuzzing and concolic execution (

FuCE

combines greybox fuzzing [

] and concolic execution [

] in a synergistic way to alleviate the downsides of those two

approaches in standalone mode. We show that prior state-of-the-art trojan detection works are heavily conned to the

type and functionality of trojans, and fail on subtly modied trojan behavior. Our primary contributions in this paper

are two-fold:

(1)

a hybrid test generation approach combining the best of both worlds: greybox fuzzing and concolic testing — our

proposed framework complements both the techniques extenuating the problems associated with standalone

approaches;

(2)

to the best of our knowledge, ours is the rst work combining fuzzing with concolic testing to reach deeper

segments of HLS designs without hitting the scalability bottleneck.

The rest of the paper is organized as follows: Section 2 outlines the background and the prior related works in the

area of trojan detection. Section 3 describes the current limitations and challenges using state-of-art techniques. In

Section 4, we propose our

FuCE

framework and show the ecacy of results in Section 5. Section 6 presents an empirical

analysis of the results and concluding remarks appear in Section 7.

2 BACKGROUND

2.1 Overview of Hardware Trojan

For decades, the silicon chip was considered as the root-of-trust of a complex system. The assumption was that the

hardware blocks and modules are trustworthy and functions are exactly as specied in the design documentation.

However, at the turn of this millennium, researchers have extended the attack surface to the underlying hardware,

and showed that it can be tampered to gain privileged information and/or launch denial-of-service attacks. This has

disrupted the root-of-trust assumption placed on hardware. The core philosophy of hardware trojan is to insert a

malicious logic in the design and bypass the functionality verication of the design. The malicious logic is activated by

the attacker’s designed input. Since the last decade, hardware trojan design and detection have been extensively studied

in the eld of hardware security. Security researchers have proposed numerous trojan threat models and novel ways of

detecting them. In [

], the authors have shown hardware trojans can be inserted in various levels of the chip design

life-cycle. Thus, security testing of a design becomes extremely important before being passed on to the next stage.

2.2 Threat model

We have outlined our threat model in Figure 1. We assume in-house designers and engineers are trusted entities who

are primarily responsible for developing complex system-on-chip (

SoC

) modules. A number of third-party hardware

IPs are procured from third-party vendors for developing such complex SoC design. However, 3PIPs are untrusted (not

developed in-house) and may have hidden backdoors and vulnerabilities. Therefore, it is important for the in-house

designers to locate the presence of malicious functionalities in such 3PIPs. For validation purpose, we assume that the

in-house designers have access to functionally correct cycle accurate behavioural model of the SoC design (in the form

of C++/Simulink model). Our threat model is in line with several earlier works such as [19, 20].

2.3 Security Testing

In the software community, security testing is one of the mandated steps adopted by the practitioners to analyze and

predict the behaviour of the system with unforeseen inputs. This has helped develop robust software that are immune

FuCE: Fuzzing+Concolic Testing iii

Hardware

IP 1

Hardware

IP N

Integrated SoC/

Hardware IP

(Verilog/

SystemC)

Golden model

(C++/Matlab

simulink)

Vulnerability

Detection

Framework

SoC/IP

integrator

Verification and

Validation engineer

Hardware

IP 2

I/P

O/P

ResponseQuery

Third party IP

vendors

(Untrusted)

In-house

Designers

(Trusted)

Fig. 1. Threat model showing untrusted third-party IPs are used for developing customized complex system-on-chip modules

against a variety of attacks like buer-overow [

], divide by zero [

], arithmetic overow [

]. We describe next two

well-known security testing methodologies that are widely used for the same:

2.3.1 Greybox fuzzing. Fuzz testing is a well known technique in software domain for detecting bugs. Greybox

fuzzing [

] involves instrumenting the code segments at the point-of-interest, and generate interesting test vectors

using evolutionary algorithms. Instrumentation injects markers in the design code which post compilation and execution

can track whether a test-case has reached the marker location. A tness function is used in order to evaluate the quality

of a test-vector. Typically, greybox fuzzing is used to improve branch-pair coverage [

] of the design, therefore the

codes are annotated at every basic block. A test-vector is regarded as interesting, if it reaches a previously unexplored

basic block, or hits it for a unique number of times. The fuzz engine maintains a history-table for every basic block

covered so far, and retains interesting test vectors for further mutation/crossover. The test generation process completes

once the user-dened coverage goal is achieved. There exists a plethora of works [

] that have improved the

performance of greybox fuzzing by augmenting various program analysis techniques. Popular coverage-guided greybox

fuzzing (

CGF

) engine like American fuzzy lop (

AFL

) [

] have been able to detect countless hidden vulnerabilities in

well-tested softwares.

2.3.2 Concolic Testing. Concolic testing [

] is a scalable way of performing symbolic execution on a program with

certain inputs considered concrete, and the rest are symbolic inputs. Symbolic execution in general suers from

scalability issues since the number of path constraints generated, are exponential in terms of the number of conditional

statements. In order to avoid costly computations, concolic execution executes the program along the path dictated by

concrete input and fork execution at branch points. The path constraints generated in concolic execution have reduced

the number of clauses and variables, thereby making it easier for solvers and can penetrate deep into complex program

checks. Driller [31] and symbolic executer (S2E) [9] are examples of engines adopting this approach.

2.4 Testing for Hardware Trojan detection

Testing based trojan detection is a well studied problem in the recent past. In earlier works [

], authors have

assumed that the trojan netlist contain a rare logic value and/or switching activity at certain nodes. Therefore, the test

generation was tuned to excite such nodes in a netlist. Later, researchers used concolic testing approaches to detect

trojans in behavioural level

RTL

designs [

]. The objective of performing concolic testing is to penetrate into

iv Mukta Debnath, Animesh Basak Chowdhury, Debasri Saha, and Susmita Sur-Kolay

deeper conditional statements of a HDL program to expose the trojan behaviour. Although the techniques seem to work

well on trojan benchmarks [

], employing concolic testing without an ecient search heuristic and a target of interest

to cover, results in multiple SAT solver calls taking considerable time for test vector generation. With recent success of

coverage-guided greybox fuzzing in software domain, it has been recently adopted in [

] for detecting trojans

in hardware design. Concolic test generation for trojan detection in high level designs have only been proposed recently

in [20, 21]. We summarize works related to ours in Table 1.

Table 1. Works on Test-based Trojan Detection in Hardware designs

Work Abstraction level Technique used Benchmarks Golden-model available?

Chakraborty et al. [7] Gate level Guided ATPG ISCAS85, ISCAS89 ✓

Banga et al. [4] Gate level Novel DFT ISCAS89 ✓

Saha et al. [28] Gate level Genetic algorithm + SAT formulation ISCAS85, ISCAS89 ✓

Chowdhury et al. [5] Gate level ATPG binning + SAT formulation ISCAS85, ISCAS89, ITC99 ✓

Huang et al. [15] Gate level Guided ATPG ISCAS85, ISCAS89 ✓

Liu et al. [25] Gate level Genetic algorithm + SMT formulation TrustHub [33] ✓

Ahmed et al. [3] Register transfer level Concolic testing TrustHub [33] ✓

Ahmed et al. [2] Register transfer level Greedy concolic testing TrustHub [33] ✓

Cruz et al. [13] Register transfer level ATPG + Model checking TrustHub [33] ✓

Liu et al. [24] Register transfer level Parallelism + concolic testing TrustHub [33] ✓

Pan et al. [27] Register transfer level Reinforcement learning TrustHub [33] ✓

Le et al. [19] HLS/SystemC Guided greybox fuzzing S3C [34] ✓

Bin et al. [20] HLS/SystemC Selective symbolic execution S3C [34] ✓

FuCE (Ours) HLS/SystemC Greybox fuzzing + Concolic Execution S3C [34] ✓

2.5 Trojan detection in high-level design

With high level synthesis becoming the new trend for designing customized hardware accelerators, only few works [

] have studied hardware trojan and security vulnerabilities in

HLS

designs and proposed preliminary countermeasures

to detect them. In prior work[

], Trojan inserted in high-level design is called synthesizable hardware Trojan (SHT) as

it gets manifested as malicious backdoor in the hardware design. Therefore, the problem of Trojan detection in low

level RTL design can be appropriately abstracted as nding SHT in high-level design. Till date, [

] and [

] have

systematically addressed the problem of Trojan detection in HLS designs. In [

], the authors have tuned the software

fuzzer

AFL

[

] for S3C Trojan benchmark characteristics and showed that their technique outperforms the vanilla

AFL

The modied

AFL

called AFL-SHT (

AFL-SHT

), introduces program-aware mutation strategy to generate meaningful

test vectors. In [

], the authors identify the additional overhead of concolic testing from usage of software libraries, and

have restricted the search space within the conditional statements of design. They named their automated prototype as

SCT-HTD (

SCT-HTD

), based on

S2E

[

]. In the next section, we focus on studying the Trojan characteristic embedded

in high-level synthesized design and evaluate the ecacy of existing detection techniques.

3 LIMITATIONS AND CHALLENGES

We present our motivating case-study on a real-time nite state machine implementation. We use a system controller

design mimicking a typical hardware functionality and highlight limitations of existing techniques to discover the

trojan behavior.

FuCE: Fuzzing+Concolic Testing v

3.1 Motivating case-study

Listing 1. Motivating example

1 int co nt ro ll er ( int stateA , int st ateB )

2 {

3 un si gn ed l ong l ong cy cle =0 , inpu t = 101 ;

4 boo l sw it ch A = FA LSE ;

6 st ateA += in put ; stat eB -= input ;

7 if( stateA != 23978 || s tateB != 5 687)

8 exit ( 0) ;

10 while ( in put ){

11 if( st ateA == 23 978 && s ta teB == 5 678 && s wi tchA == FA LSE ) // Branch 1

12 {

13 sw it chA = TRUE ; cycle ++ ;

14 swap ( sta teA , stat eB ) ;

15 if( cycle >= 2^20 -1 ) // Troja n

16 {

17 sw it chA = FA LSE ;

18 swap ( sta teA , stat eB ) ;

19 }

20 }

21 else if ( sw it ch A == TRUE ) // B ranch 2

22 {

23 s ta teA += 100 ; stat eB -= 100 ;

24 if ( s tateA == 2 3978 && st ateB == 56 78) // Br anch 3

25 sw it chA = FA LSE ;

26 }

27 sc anf (" \n% d", inpu t ) ;

28 }

29 }

In Listing 1, we have a code-snippet of a typical controller accepting state information

stateA

and

stateB

. The

controller rst checks if the

stateA

and

stateB

are set to the values 23978 and 5678, respectively (line 7). Once the

guard condition is satised, it enters a while loop, and check for the values of

stateA

stateB

and

switchA

. The loop

traversed for the rst time, satises

𝐵𝑟𝑎𝑛𝑐ℎ

1 (line 11) and swaps the values of

stateA

and

stateB

, setting

switchA

TRUE. In subsequent iterations,

𝐵𝑟𝑎𝑛𝑐ℎ

2 is always satised as

switchA

= TRUE (line 21), resulting in updating the

values of

stateA

and

stateB

. It also checks whether

stateA

and

stateB

have reached the pre-dened values (line 24).

If so, then

switchA

is set to FALSE. At the end, the controller accepts an input from the user for performing further

action.

We insert a Trojan code at line 15 where we compare the current value of

cycle

with a very large number. The

attacker intends to skip the functionality of Branch 2, and provide a false impression to the user that the controller

is working by accepting inputs, however skipping Branch 2 and not performing any operations. We explain it with

the help of a state-transition diagram in Figure 2. Here, we observe that as soon as the

cycle

reaches the value of

−

switchA

is maliciously set to FALSE and the values of

stateA

and

stateB

are swapped instead of the expected

updates in Branch 2. Thus, the loop body repeatedly executes Branch 1 and maliciously increments

cycle

after accepting

input from the user. The Trojan resembles closely to the “ticking time-bomb" or “sequential Trojan" behaviour where

剩余22页未读，继续阅读

评论收藏

内容反馈

版权申诉

易小侠

粉丝: 6453
资源: 9万+

FuCE Fuzzing+Concolic执行引导的可综合硬件设计中的特洛伊木马检测_FuCE Fuzzing+Concolic

最新资源

FuCE Fuzzing+Concolic执行引导的可综合硬件设计中的特洛伊木马检测_FuCE Fuzzing+Concolic

Cobalt Strike下载

北京邮电大学计算机考研复试笔试资料

计算机系统-笔记-HUN2021级

cs1.6老版本供下载

合成孔径雷达的经典成像算法cs(matlab)仿真代码（吐血整理，内容全，注释全）

港大CS（MSC）面试整理

合成孔径雷达RD CS OmegaK算法点目标仿真.rar

计算机科学导论原书第二版答案.zip

Cobalt-Strike-4.5

cobaltstrike4.3.zip

在dataGridView的列中出现日历选择控件的类型

541118 深入理解计算机系统（原书第三版）课程ppt

运用html+css+js三件套实现动态圣诞树

iconfont.woff

复刻CS第一人称射击游戏Demo

软件技术方案(完整资料).doc.pdf

棉花库设计规范用电.pdf

cs-training.csv

国科大数据挖掘大作业2018交通拥堵预测

计算机系统结构实验报告.pdf

简易LCR测量仪.pdf

Upstream-2023-Global-Automotive-Cybersecurity-Report

计算机组成与系统结构课后答案全(清华大学出版社袁春风主编)

模糊C均值聚类算法及实现 (3).pdf

CobaltStrike五大插件带你起飞：巨龙拉冬、LSTR、欧拉、梼杌、谢公子的插件

企业数据交互接口系统联调测试报告.doc

cst中文教程

最新资源