Automated behavior computation for software analysis and validation

Software systems can exhibit massive numbers of execution paths, and even comprehensive testing can exercise only a small fraction of these. It is no surprise that systems experience errors and vulnerabilities in use when many executions are untested. Computations over the functional semantics of programs may offer a potential solution. Structured programs are expressed in a finite hierarchy of control structures, each of which corresponds to a mathematical function or relation. A correctness theorem defines transformation of these structures from procedural logic into nonprocedural, as-built specifications of behavior. These computed specifications enumerate behavior for all circumstances of use and cover the behavior space. Automation of these computations affords a new means for validating software functionality and security properties. This paper describes theory and implementation for loop behavior computation in particular, and illustrates use of an automated behavior computation system to validate a miniature looping program with and without embedded malware.