Awards

$600K

Efficient Techniques for Formal Verification of PowerPC 750 Executables

Phase 2 SBIR

Agency: National Aeronautics and Space Administration
Topic: 09-2
Budget: 01/01/09 - 12/31/09
PI: Dr. Miroslav N. Velev

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 ...

$100K

Insider Threat Detection and Response Using Formal Methods

Phase 1 SBIR

Agency: Department of Energy
Topic: 2009
Budget: 01/01/09 - 12/31/09
PI: Dr. Miroslav N. Velev

This project will extend the Capability Acquisition Graph (CAG) model to a form that can be easily analyzed with formal methods in order to develop countermeasures for cyber attacks arising from within an organization. The extension will be based on an efficient translation of the problem to Boolean Satisfiability (SAT), in order to exploit the ...

$100K

Efficient Techniques for Formal Verification of PowerPC 750 Executables

Phase 1 SBIR

Agency: National Aeronautics and Space Administration
Topic: 08-1
Budget: 01/01/08 - 12/31/08
PI: Dr. Miroslav N. Velev

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 ...

$100K

Formal-Verification-Based Tool for Deobfuscation of Tamper-Proofed Software

Phase 1 STTR

Institution: University of Arizona

Agency: Office of the Secretary of Defense
Topic: OSD06-NC5
Budget: 07/27/06 - 01/27/07
PI: Dr. Miroslav N. Velev

The rapid increase in the use of the Internet in many aspects of our lives has led to an explosive growth in the spread of malware such as computer worms, viruses, and trojans. Security tools typically examine software for the presence of malware either by looking for specific byte signatures, or (more recently) by analyzing the candidate binary...

$100K

SBIR Phase I: Techniques for Analysis of Counterexamples from Formal Verification of High-Level Microprocessor Designs

Phase 1 SBIR

Agency: National Science Foundation
Topic: 2006
Budget: 01/01/06 - 12/31/06
PI: Dr. Miroslav N. Velev

This Small Business Innovation Research (SBIR) Phase I research proposes to study the feasibility of automatic methods for analysis of counterexamples from formal verification of pipelined and superscalar microprocessors modeled at a high level of abstraction. Aries Design Automation has developed an automatic tool flow for formal verification o...