Efficient Techniques for Formal Verification of PowerPC 750 Executables, Phase II

The capability to automatically generate a symbolic simulator for an ISA, given a formal definition of its semantics, will dramatically increase the potential for commercialization of the proposed technology. All companies that either manufacture microprocessors or develop IP of microprocessors, as well as all their clients, will be potential users. As embedded microprocessors are increasingly used in safety critical applications, it will become the norm to formally verify the executables for such applications. The immediate non-NASA commercialization will target the members of Power.org, an organization whose purpose is to develop, enable, and promote PowerPC Architecture technology. Power.org has over 40 member companies. The PowerPC architecture is used in many safety-critical embedded systems. Non-NASA customers of this technology will similarly be able to use the tool to formally verify the equivalence of two instruction sequences, and to formally check properties for a given executable. Furthermore, non-NASA customers will be able to use the tool to detect security vulnerabilities in programs, thus ensuring their robustness to security attacks, as well as to detect malicious intent in executables. The last application will allow the technology to be used in sophisticated virus scanners, utilizing formal reasoning to ensure robustness to software obfuscations of malicious intent. More »