System and method for securing web application code and verifying correctness of software

1. A method for statically analyzing a software application performed by at least one processor comprising the steps of:

statically generating an abstract interpretation of said software application which approximates runtime states of said software application by providing a type qualifier for each variable associated with at least one function within said software application and by providing a precondition for each of said at least one function within said software application, wherein said abstract interpretation preserves said software application's information flow properties; and

verifying a correctness of safety states of the abstract interpretation using bounded model checking to: generate an assertion based on said abstract interpretation;

test said assertion to identify counterexamples; and

negate counterexamples until said assertion becomes unsatisfiable; and

evaluating said type qualifiers and said preconditions to identify vulnerabilities in said software application.

2. The method of claim 1 , further comprising the step of:

inserting statements into, or modifying existing statements within, said software application to secure vulnerabilities which are identified as a result of said verifying step.

3. The method of claim 2 , wherein said step of inserting or modifying statements further comprises the step of:

inserting at least one of said statements at each location associated with an insecure variable.

4. The method of claim 2 , wherein said step of inserting or modifying statements further comprises the step of:

inserting at least one of said statements at a subset of locations associated with an insecure variable.

5. The method of claim 4 , wherein said subset of locations is determined by:

determining a minimum fixing set associated with vulnerabilities identified by said verifying step.

6. The method of claim 1 , wherein said type qualifier associates a security class with each corresponding variable.

7. The method of claim 1 , wherein said at least one function includes sensitive functions in said software application.

8. The method of claim 7 , wherein said software application is a Personal Home Page (PHP) application and said sensitive functions include an exec( ) function, which executes system commands, and an echo( ) function, which generates outputs.

9. The method of claim 1 wherein said steps of generating and verifying are performed without running said software application.

10. A computer-readable storage medium containing program instructions which, when executed by at least one processor, perform the steps of:

statically generating an abstract interpretation of said software application which approximates runtime states of said software application by providing a type qualifier for each variable associated with at least one function within said software application and by providing a precondition for each of said at least one function within said software application, wherein said abstract interpretation preserves said software application's information flow properties;

verifying a correctness of safety states of the abstract interpretation using bounded model checking to:

generate an assertion based on said abstract interpretation;

test said assertion to identify counterexamples; and

negate counterexamples until said assertion becomes unsatisfiable; and

evaluating said type qualifiers and said preconditions to identify vulnerabilities in said software application.

11. The computer-readable storage medium of claim 10 , further comprising the step of: inserting statements into, or modifying statements within, said software application to secure vulnerabilities which are identified as a result of said verifying step.

12. The computer-readable storage medium of claim 11 , wherein said step of inserting or modifying statements further comprises the step of:

inserting at least one of said statements at each location associated with an insecure variable.

13. The computer-readable storage medium of claim 11 , wherein said step of inserting or modifying statements further comprises the step of: inserting at least one of said statements at a subset of locations associated with an insecure variable.

14. The computer-readable storage medium of claim 13 , wherein said subset of locations is determined by: determining a minimum fixing set associated with vulnerabilities identified by said verifying step.

15. The computer-readable storage medium of claim 10 , wherein said type qualifier associates a security class with each corresponding variable.

16. The computer-readable storage medium of claim 10 , wherein said at least one function includes sensitive functions in said software application.

17. The computer-readable storage medium of claim 16 , wherein said software application is a Personal Home Page (PHP) application and said sensitive functions include an exec( ) function, which executes system commands, and an echo( ) function, which generates outputs.

18. A method for statically analyzing a software application performed by at least one processor comprising the steps of:

statically generating type qualifiers and preconditions for variables and functions, respectively, within said software application;

identifying insecure information flows using said type qualifiers and preconditions;

calculating counterexample traces for the identified insecure information flows;

determining root causes of errors using said counterexample traces; and

determining patching points for said software application based on said root causes of errors.

19. A computer-readable storage medium device that contains program instructions stored thereon which, when executed by at least one processor, perform the steps of:

generating a representation of a target software program which is an approximation of runtime states of said target software program which impact security of said target software program;

wherein said representation includes type qualifiers which represent variables in said target software program and preconditions which represent functions in said target software program;

wherein each of said type qualifiers associates a security class with a corresponding variable in said target software program;

verifying a correctness associated with at least some of said runtime states of said target software program using a bounded model checking technique; and

outputting information associated with security vulnerability in said target software program based on said verifying step.