Method and System for Detecting Hardware Trojans and Unintentional Design Flaws

• US 20180032760A1
• Filed: 07/27/2017
• Published: 02/01/2018
• Est. Priority Date: 07/27/2016
• Status: Active Grant

• Current Assignee: Cycuity, Inc, Regents of the University of California (University of California)
• Original Assignee: Tortuga Logic Inc.
• Inventors: Hu, Wei, Kastner, Ryan, Oberg, Jason K.
• Granted Patent: US 10,719,631 B2
• Time in Patent Office: Days
• CPC Class Codes: G06F 21/556 involving covert channels, i.e. data leakage between processes inhibiting the analysis of circuitry or operation with measures against power attack G06F21/755
• CPC Class Codes: G06F 21/57 Certifying or maintaining trusted computer platforms, e.g. secure boots or power-downs, version controls, system software checks, secure updates or assessing vulnerabilities
• CPC Class Codes: G06F 21/577 Assessing vulnerabilities and evaluating computer system security
• CPC Class Codes: G06F 21/6218 to a system of files or objects, e.g. local or distributed file system or database
• CPC Class Codes: G06F 21/71 to assure secure computing or processing of information
• CPC Class Codes: G06F 21/78 to assure secure storage of data address-based protection against unauthorised use of memory G06F12/14; record carriers for use with machines and with at least a part designed to carry digital markings G06K19/00
• CPC Class Codes: G06F 2221/034 Test or assess a computer or a system
• CPC Class Codes: H04L 63/14 for detecting or protecting against malicious traffic
• CPC Class Codes: H04L 63/1433 Vulnerability analysis

Abstract

The present disclosure includes systems and methods relating to information flow tracking and detection of unintentional design flaws of digital devices and microprocessor systems. In general, in one implementation, a technique includes: receiving a hardware design specifying an implementation for information flow in a hardware configuration; receiving one or more labels annotating the hardware design; receiving one or more security properties specifying a restriction relating to the one or more labels for implementing an information flow model; generating the information flow model; performing verification using the information flow model, wherein verification comprises verifying whether the information flow model passes or fails against the one of more security properties; and upon verifying that the information flow model passes, determining that an unintentional design flaw is not identified in the hardware design.

Claims

1. A method performed by data processing apparatus, the method comprising:

receiving a hardware design specifying an implementation for information flow in a hardware configuration, wherein the hardware design comprises at least two variables relating to the information flow;

receiving one or more labels annotating the hardware design, wherein each of the one or more labels corresponds to a respective variable of the at least two variables;

receiving one or more security properties specifying a restriction relating to the one or more labels for implementing an information flow model;

generating the information flow model, wherein generating comprises translating the one or more security properties to automatically assign a respective label value to each of the one or more labels based on the one or more security properties;

performing verification using the information flow model, wherein verification comprises verifying whether the information flow model passes or fails against the one of more security properties; and

upon verifying that the information flow model passes, determining that an unintentional design flaw is not identified in the hardware design.

2. The method of claim 1, comprising:

upon verifying that the information flow model fails, determining that an unintentional design flaw is identified in the hardware design.

3. The method of claim 2, wherein the unintentional design flaw is a hardware Trojan.

4. The method of claim 3, wherein the hardware Trojan is characterized as one of:

insertion phase, abstraction level, activation mechanism, effects, or location.

5. The method of claim 2, comprising:

generating a counterexample that identifies the security property violated during performing verification.

6. The method of claim 5, wherein the generated counterexample enables functional testing and the unintentional design flaw is a hardware Tojan, the functional testing determining an exact behavior of the hardware Trojan.

7. The method of claim 1, wherein generating the information flow comprises generating, based on the security property, an ordering structure specifying a hierarchical order comprising at least two security levels.

8. The method of claim 7, wherein the automatically assigning is based on the generated ordering structure.

9. The method of claim 8, wherein the hierarchical order of the at least two security levels comprises a higher security level corresponding to a more restricted label specified in the security property and a lower security level corresponding to a less restricted label specified in the security property.

10. The method of claim 8, wherein the ordering structure is generated as a security lattice.

11. The method of claim 1, wherein the one or more security properties are received in a high-level security language.

12. The method of claim 1, wherein translating the one or more security properties comprises translating from the high-level security language to a hardware description language.

13. The method of claim 1, wherein performing verification comprises use of an electronic design automation tool.