Transcription
Hardware Trojan Detection through Information Flow SecurityVerificationAdib Nahiyan, Mehdi Sadi, Rahul Vittal, Gustavo Contreras, Domenic Forte and Mark TehranipoorDepartment of Electrical and Computer Engineering, University of Florida, Gainesville, FloridaEmail: {adib1991, mehdi.sadi, rahulvittal, gustavokcm}@ufl.edu, {dforte, tehranipoor}@ece.ufl.eduAbstract—Semiconductor design houses are increasingly becomingdependent on third party vendors to procure IPs and meet time-tomarket constraints. However, these third party IPs cannot be trustedas hardware Trojans can be maliciously inserted into them by untrustedvendors. While different approaches have been proposed to detect Trojansin third party IPs, their limitations have not been extensively studied.In this paper, we analyze the limitations of the state-of-the-art Trojandetection techniques and demonstrate with experimental results howto avoid them. We then propose a Trojan detection framework basedon information flow security (IFS) verification. Our framework detectsviolation of IFS policies caused by Trojans without the need for white-boxknowledge of the IP. We validate the efficacy of our proposed techniqueusing benchmarks from trust-hub and demonstrate that it does not sharethe limitations of the previously proposed Trojan detection techniques.I. I NTRODUCTIONToday’s system-on-chips (SoCs) usually contain tens of IP cores(digital and analog) performing various functions. To lower R&D costand speed up the development cycle, the SoC design houses typicallypurchase most of the IP cores from third-party (3P) vendors [1]. Thisraises a major concern toward the trustworthiness of 3PIPs because3PIP vendors can insert malicious components (known as hardwareTrojans) in their IPs [2]. This issue has gained significant attentionas a Trojan inserted by a 3PIP vendor can create backdoors in thedesign through which sensitive information can be leaked and otherpossible attacks (e.g., denial of service, reduction in reliability, etc.)can be performed [3].Detection of Trojans in 3PIP cores is extremely difficult as thereis no golden version against which to compare a given IP coreduring verification. In theory, an effective way to detect a Trojanin an IP core is to activate the Trojan and observe its effects, buta Trojan’s type, size, and location are unknown, and its activationcondition is most likely a rare event. A Trojan can be, therefore, wellhidden during the normal functional operation of the 3PIP supplied asregister transfer level (RTL) code. A large industrial-scale IP core caninclude thousands of lines of code. Identifying the few lines of RTLcode in an IP core that represent a Trojan is an extremely challengingtask [4].Different approaches have been proposed to validate that an IP doesnot perform any malicious function, i.e., an IP does not contain anyTrojan. Existing Trojan detection techniques can be broadly classifiedinto structural and functional analysis, logic testing, formal verification, information flow tracking and runtime validation. Structuralanalysis employs quantitative metrics to mark signals or gates withlow activation probability as suspicious signals that may be a part ofa Trojan [6] [7]. In [8], authors have proposed a technique namedunused circuit identification (UCI) to find the lines of RTL code thathave not been executed during simulation. These unused lines ofcodes can be considered to be part of a malicious circuit. However,these techniques do not guarantee Trojan detection and authors in [9]have demonstrated that hardware Trojans can be designed to defeatUCI technique.Functional analysis based approaches [10] [11] rely on functionalsimulation to find suspicious regions of a IP which have similarcharacteristics of a hardware Trojan. Authors in [10] have proposeda technique named Functional Analysis for Nearly-unused CircuitIdentification (FANCI) which flags nets having weak input-to-outputdependency as suspicious. In [11], authors have proposed a techniquecalled VeriTrust to identify nets that are not driven by functionalinputs as potential trigger inputs of a hardware Trojan. However, in[12] authors have shown that a Trojan can be designed to bypass bothof these detection techniques.Some recent works have utilized formal methods and informationflow tracking (IFT) based techniques to detect Trojans. Authorsin [13] have proposed a technique to formally verify maliciousmodification of critical data in 3PIP by hardware Trojans. Anothersimilar approach has been proposed in [14] which formally verifiesunauthorized information leakage in 3PIPs. In [15] authors have proposed the concept of proof-carrying code (PCC) to formally validatethe security related properties of an IP. Commercial tools, e.g., Jaspersecurity path verification tool [16] can identify information leakagecaused by design bugs and/or hardware Trojans. Authors in [17]have used information flow tracking to detect Trojans in 3PIP cores.These state-of-the-art techniques have been shown to be effective indetecting various types of Trojans. However, all of these techniquesshare some inherent limitations which can be exploited to bypasstheir detection capabilities.In this paper, we present the first comprehensive analysis ofIFT/formal Trojan detection techniques. Also, we propose a novelframework to detect Trojans in 3PIPs addressing the shortcommingsof previously proposed techniques. Our proposed framework is basedon information flow security (IFS) verification which detects violationof IFS policies due to Trojans. Once we detect the presence of aTrojan, we extract its triggering condition. In this paper, we focus onutilizing our framework for Trojan detection. However, it can alsobe used to detect IFS violations unintentionally introduced by designmistakes or by CAD tools [20]. We summarize our contribution asfollows: We analyze the limitations of the recent Trojan detection techniques for 3PIP ([13] [14] [16] [15]) and demonstrate how theselimitations can be exploited to bypass their detection capabilities.We propose a IFS verification framework which detects violations of confidentiality and integrity policies caused by Trojan.The novelty of this approach is that it models an asset (e.g., a netcarrying a secret key) as a fault and leverages the automatic testpattern generation (ATPG) algorithm to detect the propagationof the asset.We propose a partial-scan ATPG technique to identifythe observe/control points through/from which an asset canbe leaked/influenced. Traditional full-scan ATPG and fullsequential ATPG cannot be used for this purpose.We propose a technique to differentiate between a valid asset
Trusted EntitiesRTL(Secure IP)SoCRTL(3PIP)SynthesisGate LevelNetlistFirm IP(3PIP)DfTInsertionPhysicalLayoutGDSIIDfT InsertedNetlistHard IP(3PIP)FabricationEndProductUntrusted EntitiesFigure 1: System-on-chip (SoC) design flow Note that, we consider the entities inside the green box in Figure1 as trusted while the entities inside the red box as rogue/untrusted.propagation path and a Trojan payload path.Our proposed technique can detect Trojan inserted by 3P vendors, e.g., design for test (DfT) vendors. This differentiates ourapproach from previously proposed techniques which cannotwork with DfT inserted netlist.We experimentally validate the efficacy of our proposed technique using 18 benchmarks from the trust-hub [19].B. Threat ModelIn this section, we present how the potential adversaries canimplant a hardware Trojan in a SoC design. We also briefly describetheir objectives and their capabilities. Finally, we present the typesof hardware Trojans covered by our threat model.1) Potential Adversaries: We consider that all the 3PIPs, i.e., soft,firm and hard IPs as untrusted. However, in this work, we mainlyfocus on the soft and the firm IPs. The third party vendors involvedin the SoC design flow (e.g., DfT insertion) are considered untrustedas well. We consider the SoC integrator and the CAD tools as trustedentities. Although we do not trust the foundry, Trojan inserted by thefoundry is out of scope of this paper. Trojans inserted by foundry canonly be detected by post-silicon verification techniques, whereas inthis paper we focus on Trojan detection in pre-silicon design stage.We assume that the third party vendors will insert the Trojanswhile the SoC integrator will try to detect them. We consider the SoCintegrator has black box knowledge of the IP purchased from the thirdparty vendors. That is, the SoC integrator only has the knowledge ofthe high level functionality of the IP. The 3PIP vendors have fullcontrol over their IP and can insert stealthy Trojans which wouldbe extremely difficult, if not impossible, to detect using traditionaltest and verification techniques. The other important players in SoCdesign flow are the third party vendors, e.g., DfT vendors who haveaccess to the whole SoC design and have the capability to incorporatestealthy malicious circuitry in the SoC.The objective of the adversaries is to implant Trojan in the SoCdesign through which sensitive information can be leaked and otherpossible attacks (e.g., denial of service, reduction in reliability, etc.)can be performed.2) Hardware Trojan Structure: The basic structure of a hardwareTrojan in a 3PIP can include two main parts, trigger and payload.A Trojan trigger is an optional part that monitors various signalsand/or a series of events in the SoC. Once the trigger detects anexpected event or condition, the payload is activated to perform amalicious behavior. Typically, the trigger is expected to be activatedunder extremely rare conditions, so the payload remains inactive mostof the time. When the payload is inactive, the SoC acts like a Trojanfree circuit, making it difficult to detect the Trojan [2].A Trojan can have a variety of possible payloads. In this paper,we will focus on payloads which leak secret information (violationof confidentiality) and/or allows an adversary to gain unauthorizedaccess to a privilege system (violation of integrity). Note that, mostTrojan payloads will either violate the confidentiality and/or theintegrity policies of the SoC.In this paper, we classify Trojan into two broad categories, Trojan type I: This type of Trojan delivers its payload throughthe valid asset propagation path. For example, RSA-T100 trusthub Trojan [19] leaks the private key through valid ciphertextThe rest of the paper is organized as follows. In the next section,we give the necessary background on SoC design flow and discussour threat model. In Section III, we analyze the limitations ofpreviously proposed Trojan detection technique and demonstrate withexperimental results how to exploit them. Section IV discusses ourproposed framework which consists of confidentiality verification,integrity verification and trigger condition extraction. We present ourresults in Section V. We discuss the limitations of our proposedapproach in Section VI. We conclude the paper with Section VII.II. P RELIMINARIES AND D EFINITIONSA. SoC Design FlowFigure 1 shows a typical SoC design flow. Design specification bythe SoC integrator is generally the first step. The SoC integrator thenidentifies a list of IPs necessary to implement the given specification.These IP cores are either developed in-house or purchased from3PIP vendors. If purchased, these 3PIP cores can be procured inthe following three forms [21], Soft IP cores are delivered as synthesizable register transfer level(RTL) written in hardware description language (HDL) such asverilog or vhdl.Firm IP cores are delivered as gate level implementation of theIP, possibly using a generic library.Hard IP cores are delivered as GDSII representations of a fullyplaced and routed design.After developing/procuring all the necessary soft IPs, the SoCdesign house integrates them to generate RTL specification of thewhole SoC. The RTL design goes through extensive functional testingto verify the functional correctness of the SoC and also to find anydesign bugs. SoC integrator then synthesizes the RTL descriptioninto a gate-level netlist based on a target technology library. Theymay also integrate firm IP cores from a vendor into this netlist. TheSoC integrator then integrates DfT structures to improve the design’stestability. However, in many cases, the DfT insertion is outsourcedto third party vendors who specialize in designing test and debugstructures, e.g., built-in self-test (BIST), compression structures, etc.In the next step, the gate-level netlist is translated into a physicallayout design. It is also possible to import IP cores from vendorsin GDSII layout file format and integrate them at this stage. Afterperforming static timing analysis (STA) and power closure, SoCintegrator generates the final layout in GDSII format and sends itout to a foundry for fabrication [2].2
We use the inclusive formal verification (IFV) tool of Cadence[22] to verify this property. The IFV tool returns that the assertionhas failed meaning that there exists information leakage from N1 toN23. This is a false positive result as there exists no informationflow from N1 to N23. The reason for this false positive result is thatthe IFV tool uses other input pins to make the logical value of N23equal to N1. This result illustrates that the technique proposed in[13], [14] would produce a large number of false positive results forany practical circuit.Limited Verification Capability: Another fundamental limitation ofany model checking technique is that a sequential circuit can beunrolled or verified only to a limited number of clock cycles, T . If theTrojan is designed in such a way so that its trigger gets activated afterT , then the Trojan would evade detection. In [13], [14] the authorsacknowledged this limitation and proposed a trivial solution that thedesign needs to be reset once the number of clock cycles exceeds T .This proposed solution however, does not provide adequate protection from Trojans. To demonstr
integrator has black box knowledge of the IP purchased from the third party vendors. That is, the SoC integrator only has the knowledge of the high level functionality of the IP. The 3PIP vendors have full control over their IP and can insert stealthy Trojans which would be extremely difficult, if not impossible, to detect using traditional test and verification techniques. The other .
