Description

Software correctness is vital for creating robust and trustworthy systems, especially in safety-critical and security-sensitive domains. Precisely understanding and proving properties about a program ensures that it behaves as intended under all circumstances, minimizing errors and vulnerabilities. Techniques like program verification rigorously prove that a program meets its specifications, while relational analysis identifies how changes or differences between versions impact behavior. Translation validation ensures that transformations, such as compiling or lifting code, preserve correctness, providing confidence in the integrity of generated outputs. Formal methods, grounded in mathematical rigor, enable comprehensive reasoning about program logic, ensuring correctness even in complex systems. Together, these approaches establish a foundation of trust, reduce debugging and testing costs, and provide the assurance necessary for high-stakes software applications, where errors can have far-reaching consequences.

Solutions

  • CodeHawk: Analysis and Patching Platform

Projects

Dark Corners

Identify and mitigate the sources of static analysis imprecision in large, real-world programs.

PI: Jeff Perkins

Technical Areas: Static Analysis, Software Correctness, Vulnerability Discovery

Funding: DARPA (APAC)

Arya (TA3)

High-Assurance, Decentralized, Autonomous Agents for Neutralizing Botnets

PI: Michael Gordon

Technical Areas: Runtime Protection, Software Correctness, AI / ML, Vulnerability Remediation

Funding: DARPA (HACCS)

MRAM

Low-cost and high-assurance binary patching for the masses

PI: Michael Gordon

Technical Areas: Static Analysis, Binary Patching, Software Correctness, Vulnerability Remediation

Funding: DARPA (AMP)

Papers