NASA SBIR 2007 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER: 07-1 X1.02-8523
SUBTOPIC TITLE: Reliable Software for Exploration Systems
PROPOSAL TITLE: Efficient Techniques for Formal Verification of PowerPC 750 Executables

SMALL BUSINESS CONCERN (Firm Name, Mail Address, City/State/Zip, Phone)
Aries Design Automation, LLC
6157 N Sheridan Rd, Suite 16M
Chicago, IL 60660 - 5818
(773) 856-6633

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
Miroslav Velev
miroslav.velev@aries-da.com
6157 N Sheridan Rd, Suite 16M
Chicago, IL 60660 - 5818
(773) 856-6633

Expected Technology Readiness Level (TRL) upon completion of contract: 6 to 7

TECHNICAL ABSTRACT (Limit 2000 characters, approximately 200 words)
We will develop an efficient tool for formal verification of PowerPC 750 executables. The PowerPC 750 architecture is used in the radiation-hardened RAD750 flight-control computers that are utilized in many space missions. The resulting tool will be capable of formally checking: 1) the equivalence of two instruction sequences; and 2) properties of a given instruction sequence. The tool will automatically introduce symbolic state for state variables that are not initialized and for external inputs. We bring a tremendous expertise in formal verification of complex microprocessors, formal definition of instruction semantics, and efficient translation of formulas from formal verification to Boolean Satisfiability (SAT). We will also provide formally verified definitions of the PowerPC 750 instructions used in the project, expressed in synthesizable Verilog; these definitions could be utilized for formal verification and testing of PowerPC 750 compatible processors, for FPGA-based emulation of PowerPC 750 executables, as well as in other formal verification tools to be implemented in the future.

POTENTIAL NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
The benefits to NASA will include state-of-the-art SAT-based technology for formal verification of PowerPC 750 executables. The PowerPC 750 architecture is used in the radiation-hardened RAD750 flight-control computers that are utilized in many space missions, including Deep Impact and the Mars Reconnaissance Orbiter. NASA will benefit from such a tool by being able to: 1) ensure that compiler optimizations have not introduced bugs in an executable, e.g., by checking for equivalence two versions of the code produced by different compilers or by the same compiler but with different optimizations, such that one of the sequences could be compiled without optimizations; 2) formally verify properties of code sequences that are written directly in assembly language for performance reasons; and 3) formally verify properties of executables provided by other organizations that do not supply the source code in order to protect their IP. As a secondary deliverable, NASA will get synthesizable Verilog definitions of the PowerPC 750 instructions used in the project; these definitions could be utilized for formal verification and testing of PowerPC 750 compatible processors, for FPGA-based emulation of PowerPC 750 executables, and for implementation of internal formal verification tools in the future.

POTENTIAL NON-NASA COMMERCIAL APPLICATIONS (Limit 1500 characters, approximately 150 words)
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 for the PowerPC architecture, utilizing formal reasoning to ensure robustness to software obfuscations of malicious intent.

NASA's technology taxonomy has been developed by the SBIR-STTR program to disseminate awareness of proposed and awarded R/R&D in the agency. It is a listing of over 100 technologies, sorted into broad categories, of interest to NASA.

TECHNOLOGY TAXONOMY MAPPING
Architectures and Networks
Autonomous Control and Monitoring
Autonomous Reasoning/Artificial Intelligence
Computer System Architectures
Expert Systems
Guidance, Navigation, and Control
On-Board Computing and Data Management
Operations Concepts and Requirements
Pilot Support Systems
Radiation-Hard/Resistant Electronics
Simulation Modeling Environment
Software Development Environments
Testing Facilities
Testing Requirements and Architectures


Form Generated on 09-18-07 17:50