PV5 ⊧ HolBAlibrary for semi-automatic analysis of binary code

Framework/set of tools for binary analysis in HOL.

Application domain/field

• Binary analysis
• Binary code
• Machine checkable proofs
• Binary Intermediate Representation (BIR)

Type of tool

Binary analysis framework

Expected input

Depends on the subtool that is used.

Internals

Tool for binary analysis in HOL4. It has the following tools:

• backlifter: gets ISA-level contracts from BIR contracts
• cfg: Control Flow Graph utilities
• comp: Composition of contracts
• exec: Concrete execution
• lifter: Transpiler from binary to BIR
• pass: Passification utility
• scamv: Abstract side channel model validation framework
• wp: Weakest precondition propagation