Static analysis for verification of software program access to secure resources for computer systems

1. A computer program product, comprising:

a non-transitory computer readable storage medium having computer readable program code embodied therewith, the computer readable program code comprising:

computer readable program code configured to, using a static analysis, analyze 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 the analysis of 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, data flow facts for each secure resource including a method fact corresponding to a method accessing the secure resource and an authorization 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 an authorization fact corresponding to a verification checker that corresponds to a secure resource; and

for any access to a secure resource where both a method fact corresponding to a predetermined method corresponding to the secure resource and an authorization 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

computer readable program code configured to, 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, output a result indicative of the analyzing.

2. The computer program product of claim 1 , wherein the software program includes one or more of the following: source code, byte code, library modules, application code, or object code.

3. The computer program product of claim 1 , where the verification is authentication.

4. The computer program product of claim 1 , where the verification is authorization.

5. The computer program product of claim 1 , wherein the analysis is performed for any and all accesses to secure resources made in the software program.

6. The computer program product of claim 1 , wherein the analysis is performed prior to the execution of the software program on the computer system.

7. The computer program product of claim 6 , further comprising computer readable program code configured to prevent the software program from executing on the computer system 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.

8. The computer program product of claim 1 , wherein the computer system is one of the following: a client system, a server, or a mobile device.

9. A computer program product, comprising:

a non-transitory computer readable storage medium having computer readable program code embodied therewith, the computer readable program code comprising:

computer readable program code configured to, using a static analysis, analyze 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 the analysis of the software program comprises:

determining whether a verification check is present for an access by the software program to the secure resource but where the verification check is invalid due to at least one of a reference to the secure resource or a method of access to the secure resource changing between verification by the verification check and access to the secure resource by the software program;

for execution of a verification checker corresponding to a selected secure resource, using a points-to graph corresponding to the software program, recording a reference to the selected secure resource and recording a mode of access to the selected secure resource; and

for a subsequent access to the selected secure resource, determining whether one or both of the reference to the selected secure resource or the mode of access to the selected secure resource has been modified from the recorded reference to the selected secure resource and the recorded mode of access to the selected secure resource; and

in response to a modification of the one or both of the reference to the selected secure resource or the mode of access to the selected secure resource, determining that the verification check corresponding to the selected secure resource is invalid; and

computer readable program code configured to, 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, output a result indicative of the analyzing.

10. The computer program product of claim 9 , wherein the software program includes one or more of the following: source code, byte code, library modules, application code, or object code.

11. The computer program product of claim 9 , where the verification is authentication.

12. The computer program product of claim 9 , where the verification is authorization.

13. The computer program product of claim 9 , wherein the analysis is performed for any and all accesses to secure resources made in the software program.

14. The computer program product of claim 9 , wherein the analysis is performed prior to the execution of the software program on the computer system.

15. The computer program product of claim 14 , further comprising computer readable program code configured to prevent the software program from executing on the computer system 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.

16. The computer program product of claim 9 , wherein the computer system is one of the following: a client system, a server, or a mobile device.

17. An apparatus, comprising:

at least one memory comprising computer code; and

at least one processor,

wherein the computer code, when executed by the at least one processor, cause the apparatus to perform at least the following:

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; and

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.

18. The apparatus of claim 17 , wherein the apparatus is the computer system.

19. The apparatus of claim 17 , wherein the apparatus is distinct from the computer system.

20. The apparatus of claim 17 , wherein the analyzing is performed prior to the execution of the software program on the computer system.

21. The apparatus of claim 17 , wherein the computer system is one of the following: a client system, a server, or a mobile device.

22. An apparatus comprising:

at least one memory comprising computer code; and

at least one processor,

wherein the computer code, when executed by the at least one processor, cause the apparatus to perform at least the following:

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 present for an access by the software program to the secure resource but where the verification check is invalid due to at least one of a reference to the secure resource or a method of access to the secure resource changing between verification by the verification check and access to the secure resource by the software program;

for execution of a verification checker corresponding to a selected secure resource, using a points-to graph corresponding to the software program, recording a reference to the selected secure resource and recording a mode of access to the selected secure resource; and

for a subsequent access to the selected secure resource, determining whether one or both of the reference to the selected secure resource or the mode of access to the selected secure resource has been modified from the recorded reference to the selected secure resource and the recorded mode of access to the selected secure resource; and

in response to a modification of the one or both of the reference to the selected secure resource or the mode of access to the selected secure resource, determining that the verification check corresponding to the selected secure resource is invalid; 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.

23. The apparatus of claim 22 , wherein the apparatus is the computer system.

24. The apparatus of claim 22 , wherein the apparatus is distinct from the computer system.

25. The apparatus of claim 22 , wherein the analyzing is performed prior to the execution of the software program on the computer system.