Security data path verification
First Claim
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.
0 Assignments
0 Petitions
Accused Products
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.
-
Citations
15 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. - View Dependent Claims (2, 3, 4, 5)
-
-
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. - View Dependent Claims (7, 8, 9, 10)
-
-
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. - View Dependent Claims (12, 13, 14, 15)
-
Specification