System and method for securing web application code and verifying correctness of software
AssigneeArmorize Technologies, Inc.
InventorsYao-Wen Huang, Fang Yu, Chung-Hung Tsai, Christian Hang, Der-Tsai Lee, Sy-Yen Kuo
Life of this patent
Estimating the term…
Abstract
Methods, software tools and systems for analyzing software applications, e.g., Web applications, are described. A software application to be analyzed is transformed into an abstract representation which preserves its information flow properties. The abstract interpretation is evaluated to identify vulnerabilities using, for example, type qualifiers to associate security levels with variables and/or functions in the application being analyzed and typestate checking. Runtime guards are inserted into the application to secure identified vulnerabilities.
Claims23
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, wherein said abstract interpretation preserves said software application's information flow properties;
- verifying a correctness of safety states of the abstract interpretation;
- identifying vulnerabilities in said software application;
- and
- securing said vulnerabilities in said software application,
- wherein said step of verifying the correctness of safety states further comprises the step of:
- using bounded model checking to verify said correctness of said safety states, and
- further wherein said step of using bounded model checking to verify said correctness of said safety states further comprises the steps of:
- generating an assertion based on said abstract interpretation;
- testing said assertion to identify counterexamples;
- and
- negating counterexamples until said assertion becomes unsatisfiable.
A non-transitory computer-readable medium containing program instructions which, when executed by at least one processor, perform the steps of:
- statically generating an abstract interpretation of a software application which approximates runtime states of said software, wherein said abstract interpretation preserves said software application's information flow properties;
- verifying a correctness of safety states of the abstract interpretation;
- identifying vulnerabilities in said software application;
- and
- securing said vulnerabilities in said software application,
- wherein said step of verifying the correctness of safety states further comprises the step of:
- using bounded model checking to verify said correctness of said safety states, and
- further wherein said step of using bounded model checking to verify said correctness of said safety states further comprises the steps of:
- generating an assertion based on said abstract interpretation;
- testing said assertion to identify counterexamples;
- and
- negating counterexamples until said assertion becomes unsatisfiable.
A method for analyzing a software application performed by at least one processor comprising the steps of:
- 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.
A non-transitory computer-readable 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.
Dependencies are inferred from the claim text.