Method and system for detecting hardware trojans and unintentional design flaws
View Patent ↗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.
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 that represent respective hardware structures related to one another by the hardware design, and wherein the hardware design includes gate-level information-flow tracking logic for the hardware structures represented by the variables,
wherein the gate-level information-flow tracking logic is associated in the hardware design with labels corresponding to each of the variables and one or more label propagation rules that specify under what conditions a value of one label should be propagated by the gate-level information-flow tracking logic to another label;
receiving one or more security properties expressed in a high-level security language for the gate-level information-flow tracking logic labels corresponding to the variables in the hardware design;
generating an information flow model, wherein generating comprises translating the one or more security properties expressed in the high-level security language into conditions that indicate whether the information flow model violates the one or more security properties;
performing a verification process using the information flow model and the label propagation rules to determine whether the information flow model violates the one or more security properties expressed in the high-level security language;
upon determining that the information flow model violates the one or more security properties, determining that an unintentional design flaw is identified in the hardware design; and
in response, generating a counterexample that identifies a security property violated by the unintentional design flaw in the hardware design during the verification process.
2. The method of claim 1 , further comprising designating the unintentional design flaw as a hardware Trojan.
3. The method of claim 2 , wherein the hardware Trojan is an insertion phase hardware Trojan, an abstraction level hardware Trojan, an activation mechanism hardware Trojan, an effects hardware Trojan, or a location hardware Trojan.
4. The method of claim 1 , wherein the generated counterexample identifies a location in the hardware for functional testing of a hardware Trojan.
5. The method of claim 1 , wherein generating the information flow model comprises generating, based on the one or more security properties, an ordering structure specifying a hierarchical order comprising at least two security levels.
6. The method of claim 5 , wherein the conditions that indicate whether the information flow model violates the one or more security properties uses the generated ordering structure.
7. The method of claim 6 , wherein the hierarchical order of the at least two security levels comprises a higher security level corresponding to a more restricted label specified in a first security property and a lower security level corresponding to a less restricted label specified in the first security property.
8. The method of claim 6 , further comprising generating the ordering structure as a security lattice.
9. The method of claim 1 , wherein translating the one or more security properties into conditions that indicate whether the information flow model violates the one or more security properties comprises generating one or more assertion statements in a hardware description language.
10. The method of claim 1 , wherein performing the verification process comprises using an electronic design automation tool.
11. A system comprising:
one or more computers and one or more storage devices storing instructions that are operable, when executed by the one or more computers, to cause the one or more computers to perform operations comprising:
receiving a hardware design specifying an implementation for information flow in a hardware configuration, wherein the hardware design comprises at least two variables that represent respective hardware structures related to one another by the hardware design, and wherein the hardware design includes gate-level information-flow tracking logic for the hardware structures represented by the variables,
wherein the gate-level information-flow tracking logic is associated in the hardware design with labels corresponding to each of the variables and one or more label propagation rules that specify under what conditions a value of one label should be propagated by the gate-level information-flow tracking logic to another label;
receiving one or more security properties expressed in a high-level security language for the gate-level information-flow tracking logic labels corresponding to the variables in the hardware design;
generating an information flow model, wherein generating comprises translating the one or more security properties expressed in the high-level security language into conditions that indicate whether the information flow model violates the one or more security properties;
performing a verification process using the information flow model and the label propagation rules to determine whether the information flow model violates the one or more security properties expressed in the high-level security language;
upon determining that the information flow model violates the one or more security properties, determining that an unintentional design flaw is identified in the hardware design; and
in response, generating a counterexample that identifies a security property violated by the unintentional design flaw in the hardware design during the verification process.
12. The system of claim 11 , wherein the operations further comprise designating the unintentional design flaw as a hardware Trojan.
13. The system of claim 12 , wherein the hardware Trojan is an insertion phase hardware Trojan, an abstraction level hardware Trojan, an activation mechanism hardware Trojan, an effects hardware Trojan, or a location hardware Trojan.
14. The system of claim 11 , wherein the generated counterexample identifies a location in the hardware for functional testing of a hardware Trojan.
15. One or more non-transitory computer storage media encoded with computer program instructions that when executed by one or more computers cause the one or more computers to perform operations comprising:
receiving a hardware design specifying an implementation for information flow in a hardware configuration, wherein the hardware design comprises at least two variables that represent respective hardware structures related to one another by the hardware design, and wherein the hardware design includes gate-level information-flow tracking logic for the hardware structures represented by the variables,
wherein the gate-level information-flow tracking logic is associated in the hardware design with labels corresponding to each of the variables and one or more label propagation rules that specify under what conditions a value of one label should be propagated by the gate-level information-flow tracking logic to another label;
receiving one or more security properties expressed in a high-level security language for the gate-level information-flow tracking logic labels corresponding to the variables in the hardware design;
generating an information flow model, wherein generating comprises translating the one or more security properties expressed in the high-level security language into conditions that indicate whether the information flow model violates the one or more security properties; and
performing a verification process using the information flow model and the label propagation rules to determine whether the information flow model violates the one or more security properties expressed in the high-level security language;
upon determining that the information flow model violates the one or more security properties, determining that an unintentional design flaw is identified in the hardware design; and
in response, generating a counterexample that identifies a security property violated by the unintentional design flaw in the hardware design during the verification process.