package binsec

  1. Overview
  2. Docs
Semantic analysis of binary executables

Install 

dune-project
 Dependency

binsec.github.io Readme Changelog LGPL-2.1-or-later License Edit opam file Versions (18)

Authors

  1. A
    Adel Djoudi
  2. B
    Benjamin Farinier
  3. C
    Chakib Foulani
  4. D
    Dorian Lesbre
  5. F
    Frédéric Recoules
  6. G
    Guillaume Girol
  7. J
    Josselin Feist
  8. L
    Lesly-Ann Daniel
  9. M
    Manh-Dung Nguyen
  10. M
    Mathéo Vergnolle
  11. M
    Mathilde Ollivier
  12. M
    Matthieu Lemerre
  13. O
    Olivier Nicole
  14. R
    Richard Bonichon
  15. R
    Robin David
  16. S
    Sébastien Bardin
  17. S
    Soline Ducousso
  18. T
    Ta Thanh Dinh
  19. Y
    Yaëlle Vinçont

Maintainers

  1. B
    BINSEC <binsec@saxifrage.saclay.cea.fr>

Sources

binsec-0.7.2.tbz
sha256=5e1d0f26a567df4abcbeb964b454cf8b2c8484194ff2d9639bdeb94d63edcb3b
sha512=a638c665407fde9aadbd57a7b9f84260db8f03c0cbf65722732d43dfc93122d801e31977e0ba7cd249b340262caf216bca746a3520d0e01d487a5baf6a6c77e6

doc/binsec/Binsec/index.html

Module BinsecSource

module Array_utils : sig ... end

Extra functions over arrays

module Ast_builder : sig ... end
module Base_logger : sig ... end
module Basic_types : sig ... end

Definitions of non-DBA types

module Binpatcher : sig ... end

Definitions for binary patcher

module Binpatcher_options : sig ... end

Options for binary patching

module Binstream : sig ... end

Representation of binary streams

module Bitset : sig ... end

Bitsets

module Bitvector : sig ... end
module Cfg : sig ... end

Control Flow Graphs

module Cfgraph : sig ... end
module Cli : sig ... end

Functors for command-line parameters declarations

module Colors : sig ... end

General color definitions for outputs

module Concrete : sig ... end
module Dba : sig ... end

Definition of DBA type

module Dba_printer : sig ... end

Pretty-printing modules & functions for DBA

module Dba_to_formula : sig ... end

Convert some DBA structure to Smtlib

module Dba_types : sig ... end

Modules & types related to DBA types

module Dba_utils : sig ... end

Shelter for functions over DBA

module Dba_visitor : sig ... end
module Dbacsl_parser : sig ... end
module Dbacsl_token : sig ... end
module Decode_utils : sig ... end
module Dhunk : sig ... end

DBA hunks, aka dhunk

module Directive : sig ... end

Directives are general located goals that one would like to achieve during an * analysis

module Disasm : sig ... end

Disassemblers & utilities

module Disasm_cfg : sig ... end
module Disasm_core : sig ... end
module Disasm_options : sig ... end
module Dwarf : sig ... end
module Dwarf_cunit : sig ... end
module Dwarf_expr : sig ... end
module Dwarf_frame : sig ... end
module Dwarf_lines : sig ... end
module Dwarf_options : sig ... end

Options for debug information printing

module Elf_options : sig ... end
module Errors : sig ... end
module File_utils : sig ... end

Extra functions over files

module Formula : sig ... end

Definition of abstract representation for logical formulas (based on SMTLIB's syntax and semantics)

module Formula_main : sig ... end

Main entry point for formula handling

module Formula_options : sig ... end
module Formula_pp : sig ... end

Formula printer

module Formula_to_smtlib : sig ... end

Translation functions from BINSEC inner representation to SMT-LIB terms

module Formula_transformation : sig ... end
module Formula_utils : sig ... end

Utility functions for formula creation

module Ghidra_cfg : sig ... end
module Ghidra_options : sig ... end
module Hash : sig ... end
module Hashamt : sig ... end

Implementation of Hash-Array Mapped Tries

module Htx_main : sig ... end
module Htx_options : sig ... end
module Ida : sig ... end
module Ida_cfg : sig ... end
module Ida_cg : sig ... end
module Ida_options : sig ... end
module Ida_utils : sig ... end
module Imap : sig ... end
module Infos : sig ... end

Abstract representation of configuration data for static analyses

module Instr_cfg : sig ... end
module Instruction : sig ... end

Canonical representation of an instruction

module Interval : sig ... end
module Isa_helper : sig ... end
module Kernel_core : sig ... end

Core kernel functions

module Kernel_functions : sig ... end

Basic kernel functions

module Kernel_options : sig ... end
module Lexer : sig ... end
module Lexer_ghidra : sig ... end
module List_utils : sig ... end

Extra functions over lists

module Lmap : sig ... end
module Loader : sig ... end
module Loader_buf : sig ... end

Generic representation of loader buffers

module Loader_elf : sig ... end
module Loader_pe : sig ... end
module Loader_raw : sig ... end
module Loader_sigs : sig ... end
module Loader_ti83 : sig ... end
module Loader_types : sig ... end
module Loader_utils : sig ... end

Loader utility functions

module Location : sig ... end
module Logger : sig ... end

Logging/output facilities

module Lreader : sig ... end

Basic stream reader

module Machine : sig ... end

Abstract description of machines

module Mcount_main : sig ... end
module Mcount_options : sig ... end
module Mnemonic : sig ... end
module Natural : sig ... end
module Parse_helpers : sig ... end
module Parse_utils : sig ... end

General BINSEC related utilities

module Parser : sig ... end
module Parser_ghidra : sig ... end
module Predba : sig ... end

First IL before producing DBA

module Prettytbl : sig ... end
module Print_utils : sig ... end

Extra pretty-printing functions

module Prover : sig ... end
module Riscv_arch : sig ... end
module Riscv_options : sig ... end
module Riscv_to_dba : sig ... end
Sourcemodule Runtime : sig ... end
module Sequence : sig ... end
module Sigs : sig ... end

Generic signatures used throughout BINSEC

module Simplification_dba : sig ... end
module Simplification_dba_block : sig ... end

Intra-block simplifications

module Simplification_dba_prog : sig ... end
module Simplification_dba_utils : sig ... end

Generic utility functions for DBA simplification

module Simplification_options : sig ... end
module Simulation : sig ... end
module Size : sig ... end
module Smt_model : sig ... end

Internal model representation

module Smtlib : sig ... end
module Smtlib_lexer : sig ... end
module Smtlib_options : sig ... end
module Smtlib_parser : sig ... end
module Smtlib_pp : sig ... end
module Smtlib_to_formula : sig ... end
module Smtlib_utils : sig ... end
module Solver : sig ... end

Interface with SMT solvers

module String_utils : sig ... end

Extra functions over strings

module Subprocess : sig ... end
module Term : sig ... end
module Utils : sig ... end

Generic utilities

module Virtual_address : sig ... end
module Worklist : sig ... end

Worklist / Work queue implementation

module X86Instruction : sig ... end

Interface for X86 instructions

module X86Types : sig ... end
module X86Util : sig ... end

X86 utility functions

module X86_options : sig ... end
module X86decoder : sig ... end

Decode a function from a reader

module X86pp : sig ... end

Pretty-printers for X86

module X86toDba : sig ... end

Lifter from X86 to DBA

module Z80_arch : sig ... end
module Z80_options : sig ... end
module Z80_to_dba : sig ... end