"Function Extraction: A New Paradigm for Producing Secure Code"

Without secure computer codes, it is impossible to have a fully secure information processing system. This paper proposes the evolving technique of Function Extraction (FX) as part of a novel paradigm for the production of secure computer codes. FX is, in effect, the inverse of formal verification as it analyzes code to produce a mathematical specification of its behavior. This has the potential for identifying unwanted or unexpected behaviors and for analyzing unknown or "found"code artifacts such as malware. The effort is enabled by recent developments in loop analysis that allow invariant relations to be developed for loop bodies enabling the loop function to be discovered. The paper defines program behavior as a mathematical description of the effects of program execution on the environment in which the program runs and continues with a discussion of its current status. As FX is an evolving paradigm, areas in which work remains to be done are discussed and examples of the results of two prototype analyzers are given.