METHODS AND SYSTEMS FOR AUTOMATICALLY TESTING SOFTWARE

摘要

An automatic software testing machine may be configured to provide an advanced symbolic execution approach to software testing that combines dynamic symbolic execution and static symbolic execution, leveraging the strengths of each and avoiding the vulnerabilities of each. One or more software testing machines within a software testing system may be configured to automatically and dynamically alternate between dynamic symbolic execution and static symbolic execution, based on partial control flow graphs of portions of the software code to be tested. In some example embodiments, a software testing machine begins with dynamic symbolic execution, but switches to static symbolic execution opportunistically. In static mode, instead of checking entire programs for verification, the software testing machine may only check one or more program fragments for testing purposes. Thus, the software testing machine may benefit from the strengths of both dynamic and static symbolic execution.

主权项

1. A method comprising:
by a dynamic symbolic execution engine comprising one or more processors:
accessing software code to be automatically tested, the software code including multiple execution paths through multiple executable statements of the software code; andperforming a dynamic phase of an automatic test of the software code by performing dynamic symbolic execution of a first portion of the execution paths, the dynamic symbolic execution forking a separate symbolic executor for each execution path in the first portion, each forked symbolic executor generating a corresponding formula for the corresponding execution path; by a static symbolic execution engine comprising one or more processors:
determining that a second portion of the execution paths is devoid of non-statically interpretable executable statements; andperforming a static phase of the automatic test of the software code by performing static symbolic execution of the second portion of the execution paths in response to the determining that the second portion is devoid of non-statically interpretable executable statements, the static symbolic execution generating at least one formula that corresponds to all executable statements in the second portion of the execution paths; and by a solver module comprising one or more processors, generating a set of test cases for the software code by solving the formulas generated during the dynamic and static phases of the automatic test of the software code.