SYSTEM, METHOD AND COMPUTER-ACCESSIBLE MEDIUM FOR SECURITY VERIFICATION OF THIRD PARTY INTELLECTUAL PROPERTY CORES

• US 20160098565A1
• Filed: 12/03/2015
• Published: 04/07/2016
• Est. Priority Date: 10/03/2014
• Status: Active Grant

• Current Assignee: New York University
• Original Assignee: New York University
• Inventors: KARRI, RAMESH, VEDULA, VIVEKANANDA, RAJENDRAN, JEYAVIJAYAN, DHANDAYUTHAPANY, ARUNSHANKAR
• Granted Patent: US 10,083,303 B2
• Time in Patent Office: Days
• US Class Current: 1/1
• CPC Class Codes: G06F 21/56 Computer malware detection or handling, e.g. anti-virus arrangements
• CPC Class Codes: G06F 21/577 Assessing vulnerabilities and evaluating computer system security
• CPC Class Codes: G06F 21/76 in application-specific integrated circuits [ASIC] or field-programmable devices, e.g. field-programmable gate arrays [FPGA] or programmable logic devices [PLD]

Abstract

An exemplary system, method and computer-accessible medium for detecting the presence of a Trojan(s) in a circuit(s), can include, for example, receiving information related to a property(s) configured to determine the presence of the Trojan(s), and determining the presence of the Trojan(s) based on the property(s) and a design(s) of the circuit(s) using a bounded model checking tool.

Claims

1. A non-transitory computer-accessible medium having stored thereon computer-executable instructions for determining a presence of at least one Trojan in at least one configuration, wherein, when a computer arrangement executes the instructions, the computer arrangement is configured to perform procedures comprising:

receiving electronic data related to at least one property; and

determining the presence of the at least one Trojan based on the electronic data, the at least one property and at least one design of the at least one configuration using a bounded model checking (BMC) engine.

2. The computer-accessible medium of claim 1, wherein the at least one design includes a software description of the at least one configuration.

3. The computer-accessible medium of claim 1, wherein the determination procedure includes generating at least one Boolean formula using the BMC engine.

4. The computer-accessible medium of claim 3, wherein the computer arrangement is further configured to assign particular values to the at least one Boolean formula using a satisfiability solving engine.

5. The computer-accessible medium of claim 4, wherein the computer arrangement is further configured to generate an indication of the presence of the at least one Trojan if the at least one Boolean formula evaluates to 1 using the particular values.

6. The computer-accessible medium of claim 1, further comprising at least one bound.

7. The computer-accessible medium of claim 6, wherein the determination procedure is further based on the at least one bound.

8. The computer-accessible medium of claim 6, wherein the at least one bound is a particular number of clock cycles.

9. The computer-accessible medium of claim 1, wherein the at least one property includes a detection that the at least one Trojan leaks at least one secret.

10. The computer-accessible medium of claim 1, wherein the at least one property includes a detection that the at least one Trojan leaks at least one subset of the at least one secret.

11. The computer-accessible medium of claim 1, wherein the at least one property includes a detection that the at least one Trojan is triggered over a plurality of clock cycles.

12. The computer-accessible medium of claim 1, wherein the at least one property includes a detection of at least one of at least one direct polarity and at least one indirect polarity.

13. The computer-accessible medium of claim 1, wherein the at least one configuration includes at least one circuit.

14. The computer-accessible medium of claim 1, wherein the computer arrangement is further configured to determine assignments to an input of the configuration over a plurality of clock cycles using the at least one property.

15. The computer-accessible medium of claim 14, wherein the determination procedure utilize a set of inputs over the clock cycles that violate the at least one property.

16. The computer-accessible medium of claim 1, wherein the at least one property includes a strict avalanche criterion property.

17. The computer-accessible medium of claim 16, wherein the computer arrangement is further configured to determine the strict avalanche criterion property.

18. The computer-accessible medium of claim 17, wherein the computer arrangement determines the strict avalanche criterion property using at least two seeds for a pseudo random number generator.

19. The computer-accessible medium of claim 1, wherein the computer arrangement is further configured to generate a plurality of states that satisfy the at least one property using the BMC engine.

20. The computer-accessible medium of claim 19, wherein the computer arrangement determines the presence of the at least one Trojan based on the states.

21. The computer-accessible medium of claim 1, wherein the computer arrangement is further configured to generate at least one witness that violates the at least one property using the BMC engine.

22. The computer-accessible medium of claim 21, wherein the computer arrangement determines the presence of the at least one Trojan based on the at least one witness.

23. The computer-accessible medium of claim 1, wherein the computer arrangement is further configured to generate at least one temporal logic design of the at least one configuration using the BMC checking engine.

24. The computer-accessible medium of claim 1, wherein the computer arrangement is further configured to determine the presence of the at least one Trojan based on the at least one temporal logic design.

25. A method for determining a presence of at least one Trojan in at least one configuration, comprising:

receiving electronic data related to at least one property; and

using a computer hardware arrangement, determining the presence of the at least one Trojan based on the electronic data, the at least one property and at least one design of the at least one configuration using a bounded model checking (BMC) engine.

26. A system for determining a presence of at least one Trojan in at least one configuration, comprising:

a computer hardware arrangement configured to;

receiving electronic data related to at least one property; and

determine the presence of the at least one Trojan based on the electronic data, the at least one property and at least one design of the at least one configuration using a bounded model checking (BMC) engine.