Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Unit Proofing Framework for Code-level Verification: A Research Agenda

Paschal C. Amusuo, Parth V. Patil, Owen Cochell, Taylor Le Lievre, James C. Davis

TL;DR

The paper addresses the challenge of scalable, reliable verification of code-level software implementations, where harness-based unit proofs are labor-intensive and error-prone. It presents an exploratory study of AWS-style unit proofs in FreeRTOS, showing that unit proofs can detect many memory-safety vulnerabilities but miss others due to incomplete properties, modeling gaps, or outdated proofs. It then proposes a principled Unit Proofing Framework with four tools—Software Decomposer, Proof Builder, Proof Repairer, and Proof Updater—to automate proof construction, repair, and maintenance within real development workflows. If realized, the framework could enable earlier discovery of code-level defects, reduce manual effort, and scale formal verification to real-world software used in safety-critical domains.

Abstract

Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose, engineers use code-level tools. However, such tools struggle to scale to large software. The process of "Unit Proofing" mitigates this by decomposing the software and verifying each unit independently. We examined AWS's use of unit proofing and observed that current approaches are manual and prone to faults that mask severe defects. We propose a research agenda for a unit proofing framework, both methods and tools, to support software engineers in applying unit proofing effectively and efficiently. This will enable engineers to discover code-level defects early.

A Unit Proofing Framework for Code-level Verification: A Research Agenda

TL;DR

The paper addresses the challenge of scalable, reliable verification of code-level software implementations, where harness-based unit proofs are labor-intensive and error-prone. It presents an exploratory study of AWS-style unit proofs in FreeRTOS, showing that unit proofs can detect many memory-safety vulnerabilities but miss others due to incomplete properties, modeling gaps, or outdated proofs. It then proposes a principled Unit Proofing Framework with four tools—Software Decomposer, Proof Builder, Proof Repairer, and Proof Updater—to automate proof construction, repair, and maintenance within real development workflows. If realized, the framework could enable earlier discovery of code-level defects, reduce manual effort, and scale formal verification to real-world software used in safety-critical domains.

Abstract

Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose, engineers use code-level tools. However, such tools struggle to scale to large software. The process of "Unit Proofing" mitigates this by decomposing the software and verifying each unit independently. We examined AWS's use of unit proofing and observed that current approaches are manual and prone to faults that mask severe defects. We propose a research agenda for a unit proofing framework, both methods and tools, to support software engineers in applying unit proofing effectively and efficiently. This will enable engineers to discover code-level defects early.

Paper Structure

This paper contains 21 sections, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Code-level Verification and Unit Proofing
  3. Formally Verifying Software Implementations
  4. Unit Proofing for Enabling Code-level Verification
  5. Exploratory Study of Unit Proofing
  6. Methodology
  7. Results
  8. Observations on Unit Proofing Failures
  9. Insufficient Verification Properties (CVE-2018-16523)
  10. Insufficient Input Modeling (e.g., CVE-2018-16527)
  11. Insufficient Function Modeling (CVE-2018-16524)
  12. Out-of-date Unit Proofs (CVE-2018-16525)
  13. Research Agenda: A Unit Proofing Framework
  14. Unit Proofing Challenges and Open Questions
  15. The Unit Proofing Framework Design
  16. ...and 6 more sections

Figures (2)

  • Figure 1: Overview of Unit Proofing. To verify function 2, an engineer models its input, shared resources, and other functions. A verifier can then check it in isolation.
  • Figure 2: An end-to-end agenda for unit proof engineering. Software engineers use a set of tools and intelligent agents to verify the memory safety of applications.