Patent ID: 8381242

Claim:
A method, comprising: using a static analysis, analyzing a software program to determine whether the software program accesses a secure resource for a computer system without verification that the secure resource can be accessed by the software program, wherein analyzing the software program comprises: determining whether a verification check is missing for an access by the software program to the secure resource; mapping every secure resource to a data flow fact instantiated at one or more call sites for procedure calls within the software program, the data flow facts for each secure resource including a method fact corresponding to a method accessing the secure resource and a verification fact corresponding to a verification checker that corresponds to the secure resource; propagating the data flow facts through a call graph of the software program; killing a method fact corresponding to a secure resource in response to entry into a predetermined method corresponding to a secure resource; killing a verification fact corresponding to a verification checker that corresponds to a secure resource; for any access to a secure resource where both a method fact corresponding to a predetermined method corresponding to the secure resource and a verification fact corresponding to a verification checker that corresponds to the secure resource are not killed at the access, determining that a verification check is missing for the access by the software program to the secure resource; and in response to an access by the software program to the secure resource without verification that the secure resource can be accessed by the software program, outputting a result indicative of the analyzing.