Security data path verification

• US 9,922,209 B1
• Filed: 09/19/2016
• Issued: 03/20/2018
• Est. Priority Date: 04/22/2013
• Status: Active Grant

• Current Assignee: Cadence Design Systems Incorporated (Cadence Group)
• Original Assignee: Cadence Design Systems Incorporated (Cadence Group)
• Inventors: Purri, Victor Markus, Campos, Caio Arajo Teixeira, Bjrk, Magnus, Loh, Lawrence, Coelho, Claudionor Jose Nunes
• Primary Examiner(s): Memula, Suresh
• Application Number:
  US15/269,919
• Time in Patent Office: 547 Days
• Field of Search: 716136
• CPC Class Codes: G06F 21/71 to assure secure computing or processing of information
• 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]
• CPC Class Codes: G06F 30/30 Circuit design
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

A formal verification approach verifies data access and data propagation paths in a circuit design by proving the unreachability of path cover properties of the circuit design. A security path verification system receives an original circuit model of a circuit design, along with parameters identifying a first location within the circuit design that is a source of tainted data and a second location within the circuit design that is coupled to the first location. The security path verification system also receives a selection of portions of the circuit design to be excluded from the verification analysis. Using an abstracted version of the exclude portions, the security verification system generates a second circuit model of the circuit design for use in determining whether the tainted data can reach the second location from the first location within the circuit design.

Claims

1. A computer implemented method for security verification of an electronic circuit, the method comprising:

accessing a first set of parameters identifying a first location within the electronic circuit that is a source of tainted data and a second location within the electronic circuit that is coupled to the first location;

accessing a second set of parameters identifying a third location within the electronic circuit; and

verifying whether the tainted data can reach the second location within the electronic circuit from the first location within the electronic circuit by propagating through the third location within the electronic circuit.

2. The method of claim 1, wherein the tainted data comprises unsecured, data or control information, generated at the first location and that appears as data or control information arriving at the second location.

3. The method of claim 1, wherein the tainted data comprises secured, data or control information, generated at the first location and that appears as data or control information arriving at the second location.

4. The method of claim 1, further comprising using formal verification in verifying whether the tainted data can reach the second location from the first location by propagating through the third location.

5. The method of claim 4, further comprising:

accessing a first circuit model of the electronic circuit;

generating a second circuit model of the electronic circuit by at least partially duplicating the first circuit model one or more times; and

verifying, using the second circuit model, whether the tainted data can reach the second location within the electronic circuit from the first location within the electronic circuit.

6. A non-transitory computer-readable storage medium having stored thereupon computer program code that, when executed by a micro-processor, causes the microprocessor of a computing system to perform a set of acts for security verification of an electronic circuit, the set of acts comprising:

accessing a first set of parameters identifying a first location within the electronic circuit that is a source of tainted data and a second location within the electronic circuit that is coupled to the first location;

accessing a second set of parameters identifying a third location within the electronic circuit; and

verifying whether the tainted data can reach the second location within the electronic circuit from the first location within the electronic circuit by propagating through the third location within the electronic circuit.

7. The non-transitory computer-readable storage medium of claim 6, wherein the tainted data comprises unsecured, data or control information, generated at the first location and that appears as data or control information arriving at the second location.

8. The non-transitory computer-readable storage medium of claim 6, wherein the tainted data comprises secured, data or control information, generated at the first location and that appears as data or control information arriving at the second location.

9. The non-transitory computer-readable storage medium of claim 6, wherein the set of acts further comprises using formal verification in verifying whether the tainted data can reach the second location from the first location by propagating through the third location.

10. The non-transitory computer-readable storage medium of claim 9, wherein the set of acts further comprising:

accessing a first circuit model of the electronic circuit;

generating a second circuit model of the electronic circuit by at least partially duplicating the first circuit model one or more times; and

verifying, using the second circuit model, whether the tainted data can reach the second location within the electronic circuit from the first location within the electronic circuit.

11. An apparatus for security verification of a circuit design, comprising:

one or more modules, at least one of which comprises at least one microprocessor including one or more processor cores executing one or more threads in a computing system;

a non-transitory computer accessible storage medium storing thereupon program code that includes a sequence of instructions that, when executed by the at least one micro-processor or processor core of a computing system, causes the at least one micro-processor or processor core at least to;

access a first set of parameters identifying a first location within the electronic circuit that is a source of tainted data and a second location within the electronic circuit that is coupled to the first location;

access a second set of parameters identifying a third location within the electronic circuit; and

verify whether the tainted data can reach the second location within the electronic circuit from the first location within the electronic circuit by propagating through the third location within the electronic circuit.

12. The apparatus of claim 11, wherein the tainted data comprises unsecured, data or control information, generated at the first location and that appears as data or control information arriving at the second location.

13. The apparatus of claim 11, wherein the tainted data comprises secured, data or control information, generated at the first location and that appears as data or control information arriving at the second location.

14. The apparatus of claim 11, wherein the program code further includes the sequence of instructions that, when executed by the at least one micro-processor or processor core of the computing system, further causes the at least one micro-processor or processor core to use formal verification in verifying whether the trained data can reach the second location from the first location.

15. The apparatus of claim 14, wherein the program code further includes the sequence of instructions that, when executed by the at least one micro-processor or processor core of the computing system, further causes the at least one micro-processor or processor core to:

access a first circuit model of the electronic circuit;

generate a second circuit model of the electronic circuit by at least partially duplicating the first circuit model one or more times; and

verify, using the second circuit model, whether the tainted data can reach the second location within the electronic circuit from the first location within the electronic circuit.