Systematic Scanning for Malicious Source Code

For an organization that depends on software for important parts of its mission, safety and security flaws in such software are major concerns. Although there is a growing number of tools that can be helpful in identifying unintentionally inserted safety or security flaws, the possibility of intentionally inserted "flaws" or back doors can no longer be ignored. Fundamentally, an intentionally inserted back door can only be recognized by the fact that it does more rather than less of what it is supposed to do. For example, a function that is expected to only query the balance of a bank account, may also, as a side-effect under special circumstances that are unlikely to be encountered during testing, transfer money between accounts. To locate such hidden side-effects, it requires that the semantics of each function somehow be extracted from the source code and presented to a reviewer in a way that allows them to recognize inappropriate actions. In this paper we describe scanning technology that can automatically extract the pre- and post-conditions of every function in the system, including both direct and indirect effects of each function, and present these to a reviewer in human-comprehensible terms. For each external entry point into the system, the postconditions in particular may then be compared against the expected effects of the function, and where potentially inappropriate side- effects are identified, these effects may be traced down through the program to the point where they occur.