A Comparative Binary Analysis Tool (CBAT)
Abstract
This report describes the research and software development carried out by the CBAT team in the context of ONR's Total Platform Cyber Protection (TPCP) program. The CBAT tool enables automated verification of late-stage software customizations and is sufficiently mature to handle realistic software. CBAT is now a useful and complete tool, and has been released publicly as open-source software. It has extensive documentation and an indepth tutorial that walks users through much of its functionality. We also include a guide to the underlying framework BAP that CBAT is built on top of, in order to better serve the power user who wants to contribute to CBAT, and to further adoption. CBAT is already in use by other projects at Draper, and can be directly utilized in other areas such as automated program repair or translation verification. Overall, the CBAT project advances verification research and demonstrates that formal verification can enable late-stage software customization with evidence for recertification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 14, 2022
- Accession Number
- AD1186235
Entities
People
- J. T. Paasch
Organizations
- Charles Stark Draper Laboratory