NASA SBIR 2007 Solicitation

FORM B - PROPOSAL SUMMARY


PROPOSAL NUMBER: 07-2 X1.02-8523
PHASE 1 CONTRACT NUMBER: NNX08CB04P
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 Road, Suite 16M
Chicago, IL 60660 - 5818
(773) 856-6633

PRINCIPAL INVESTIGATOR/PROJECT MANAGER (Name, E-mail, Mail Address, City/State/Zip, Phone)
Miroslav N Velev
miroslav.velev@aries-da.com
6157 N Sheridan Road, 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 produce 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, the Mars Reconnaissance Orbiter, the Mars Rovers, and is planned to be used in the Crew Exploration Vehicle that will become operational in 2011. NASA will benefit from such a tool by being able to: 1) ensure that compiler optimizations have not introduced bugs in an executable; 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. After Phase 2, our technology will become applicable to any microprocessor architecture to be adapted by NASA in the future, as the tool that we will develop will allow to automatically generate a symbolic simulator for any instruction set architecture, given a formal definition of its semantics. As another 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)
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.

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
General Public Outreach
Guidance, Navigation, and Control
Highly-Reconfigurable
Human-Computer Interfaces
On-Board Computing and Data Management
Operations Concepts and Requirements
Pilot Support Systems
Radiation-Hard/Resistant Electronics
Simulation Modeling Environment
Software Development Environments
Spaceport Infrastructure and Safety
Testing Facilities
Testing Requirements and Architectures


Form Generated on 10-23-08 13:36