PV5 ⊧ HolBAlibrary for semi-automatic analysis of binary codeFramework/set of tools for binary analysis in HOL.
- Binary analysis
- Binary code
- Machine checkable proofs
- Binary Intermediate Representation (BIR)
Type of toolBinary analysis framework
Expected inputDepends on the subtool that is used.
InternalsTool 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