System, method and computer-accessible medium for security verification of third party intellectual property cores

Patent metadata

Field	Value
Publication number	US-2016098558-A1
Application number	US-201514874794-A
Country	US
Kind code	A1
Filing date	Oct 5, 2015
Priority date	Oct 3, 2014
Publication date	Apr 7, 2016
Grant date	—

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.

First claim

What is claimed is:

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 . 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.

20 . 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.

Assignees

• Univ New York

Inventors

• Vedula Vivekananda
• Rajendran Jeyavijayan
• Dhandayuthapany Arunshankar
• Karri Ramesh

Classifications

• G06F2221/034

  Test or assess a computer or a system · CPC title

• G06F21/55 Primary

  Detecting local intrusion or implementing counter-measures · CPC title

• G06F21/71

  to assure secure computing or processing of information · CPC title

• G06F21/72 Primary

  in cryptographic circuits · CPC title