Security data path verification

• US 9,449,196 B1
• Filed: 04/22/2013
• Issued: 09/20/2016
• Est. Priority Date: 04/22/2013
• Status: Active Grant

• Current Assignee: Jasper Design Automation, Inc.
• Original Assignee: Jasper Design Automation, Inc.
• Inventors: Purri, Victor Markus, Campos, Caio Arajo Teixeira, Bjrk, Magnus, Coelho, Claudionor Jose Nunes, Loh, Lawrence
• Primary Examiner(s): Memula, Suresh
• Application Number:
  US13/867,341
• Time in Patent Office: 1,247 Days
• Field of Search: 716/106, 716/136
• US Class Current: 1/1
• 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 a circuit design, the method comprising:

receiving at first circuit model of the circuit design;

receiving one or more 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;

receiving an indication of a portion of the circuit design to be modeled as a black box, the portion located along one more transmission paths between the first and second locations within the circuit design;

generating an abstracted version of the portion of the circuit design;

generating a second circuit model of the circuit design by modifying the first circuit model with the abstracted version of the portion of the circuit design; and

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

2. The method of claim 1, further comprising:

receiving one or more parameters identifying a third location within the circuit design, wherein

verifying whether the tainted data can reach the second location within the circuit design from the first location within the circuit design comprises verifying, using the second circuit model, whether the tainted data can reach the second location within the circuit design from the first location in the circuit design by propagating through the third location in the circuit design.

3. The method of claim 2, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in the circuit design comprises using formal verification.

4. The method of claim 3, further comprising:

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

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

5. The method of claim 1, further comprising:

receiving one or more parameters identifying a third location within the circuit design, wherein

verifying whether the tainted data can reach the second location within the circuit design from the first location within the circuit design comprises verifying, using the second circuit model, whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in the circuit design.

6. The method of claim 5, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in the circuit design comprises using formal verification.

7. The method of claim 6, further comprising:

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

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

8. The method of claim 1, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location in the circuit design comprises using formal verification.

9. The method of claim 1, wherein the abstracted version of the portion of the circuit design includes a plurality inputs and a plurality of outputs, and the abstracted version is configured to couple any of the plurality of inputs to any of the plurality of outputs.

10. The method of claim 9, wherein the second circuit model is configured to introduce a delay between one or more inputs of the plurality of inputs and one or more outputs of the plurality of outputs, the delay having a value corresponding to a propagation delay between one input of the plurality of inputs and one output of the plurality of outputs.

11. The method of claim 9, wherein the second circuit model is configured to have a range of delay between two bounds, a lower bound being zero or more clock cycles, and an upper bound being greater than zero and less than infinity clock cycles, between the one input of the plurality of inputs and the one output of the plurality of outputs.

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

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

14. A non-transitory computer-readable storage medium containing computer program code for security verification of a circuit design, the code comprising code for:

receiving a first circuit model of the circuit design;

receiving one or more 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;

receiving an indication of a portion of the circuit design to be modeled as a black box, the indicated portion located along one more transmission paths between the first and second locations within the circuit design;

generating an abstracted version of the portion of the circuit design;

generating a second circuit model of the circuit design by modifying the first circuit model with the abstracted version of the portion of the circuit design; and

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

15. The non-transitory computer-readable storage medium of claim 14, the plurality of acts further comprising:

receiving one or more parameters identifying a third location within the circuit design, wherein

verifying whether the tainted data can reach the second location within the circuit design from the first location within the circuit design comprises verifying, using the second circuit model, whether the tainted data can reach the second location within the circuit design from the first location in the circuit design by propagating through the third location in the circuit design.

16. The non-transitory computer-readable storage medium of claim 14, the plurality of acts further comprising:

receiving one or more parameters identifying a third location within the circuit design, wherein

verifying whether the tainted data can reach the second location within the circuit design from the first location within the circuit design comprises verifying, using the second circuit model, whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in the circuit design.

17. The non-transitory computer-readable storage medium of claim 14, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in the circuit design comprises using formal verification.

18. The non-transitory computer-readable storage medium of claim 17, the plurality of acts further comprising:

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

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

19. The non-transitory computer-readable storage medium of claim 14, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in the circuit design comprises using formal verification.

20. The non-transitory computer-readable storage medium of claim 19, the plurality of acts further comprising:

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

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

21. A system for security verification of a circuit design, comprising:

non-transitory memory storing thereupon program code that comprises a sequence of instructions;

a processor or a processor core that executes one or more threads of execution of a computing system, wherein the sequence of instructions executed by the processor or processor core causes the processor or processor core at least to receive a first circuit model of the circuit design;

receive one or more 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;

receive an indication of a portion of the circuit design to be modeled as a black box, the portion located along one more transmission paths between the first and second locations within the circuit design;

generate an abstracted version of the portion of the circuit design;

generate a second circuit model of the circuit design by modifying the first circuit model with the abstracted version of the portion of the circuit design; and

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

22. The system of claim 21, wherein the non-transitory memory stores the program code, and the program code includes further instructions that when executed by the processor or processor core, cause the processor or processor core to receive one or more parameters identifying a third location within the circuit design, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location within the circuit design comprises verifying, using the second circuit model, whether the tainted data can reach the second location within the circuit design from the first location in the circuit design by propagating through the third location in the circuit design.

23. The system of claim 21, wherein the non-transitory memory stores the program code, and the program code includes further instructions that, when executed by the processor or processor core, cause the processor or processor core to receive one or more parameters identifying a third location within the circuit design, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location within the circuit design comprises verifying, using the second circuit model, whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in he circuit design.

24. The system a claim 21, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in the circuit design comprises using formal verification.

25. The system of claim 24, wherein the non-transitory memory stores the program code, and the program code includes further instructions that, when executed by the processor or processor core, cause the processor or processor core to generate a third circuit model of the circuit design by at least partially duplicating the first circuit model one or more times;

and verity, using the third circuit model, whether the tainted data can reach the second location within the circuit design from the first location within the circuit design.

26. The system of claim 21, wherein verifying whether the tainted data can reach the second location within the circuit design from the first location in the circuit design without propagating through the third location in the circuit design comprises using formal verification, and the non-transitory memory stores the program code that includes further instructions that, when executed by the processor or processor core, cause the processor or processor core to generate a third circuit model of the circuit design by at least partially duplicating the first circuit model one or more times;

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