package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

0.10.1 (2025-06-30)

** Misc

  • Minor changes in the DBA printer (sync operator names with sse script)
  • Experimental support for extensible custom entries in formulas

** Bugs

  • Fix some issues with x86 and RISCV disassembly

0.10.0 (2025-02-16)

** Features

  • Add a new configuration option to tune the checkct instrumentation (-checkct-features control-flow,memory-access,multiplication,dividend,divisor)
  • Add the secret-erasure check command in checkct (check secret erasure over symbol)
  • Add an experimental hook function return command in SE

** Misc

  • Add support for AARCH64 core dump in SE
  • Improve debug with symbol offset annotation (-sse-debug-level 2)

** Bugs

  • Fix some ARM and x86 disassembly issues
  • Fix some rewriting rule issues
  • Fix compilation issues with latest OCaml compilers
  • Refactor parsers and suppress conflicts

0.9.1 (2024-05-21)

** Misc

  • Support native OCaml z3 binding (-smt-solver z3:builtin)

** Bugs

  • Fix SMTlib formula printer not always flushing the definitions before use

0.9.0 (2024-05-01)

** Features

  • Add a new SSE engine (-sse-engine multi-checks) that tries to reuse the previous SMT solver session (incremental mode)
  • Add a common sub-expression elimination pass in SSE (-sse-cse)

** Documentation

  • Add some comments in the SSE plugin interface

** Misc

  • Reworked SMT solver interface
  • Support for latest version of the bitwuzla solver
  • Add some formula rewriting rules

** Bugs

  • Fix solver queries taking several order times the given timeout
  • Fix some x86 and RISCV disassembly issues
  • Fix some script parser issues

0.8.2 (2024-03-08)

** Misc

  • Best effort handling of <symbol@plt> in SSE script (x86 for now)
  • Add an option to ignore or simply warn when trying to replace a symbol absent of the binary (-sse-missing-symbol)
  • Warn for different threats to completeness at the end of SSE analysis

** Bugs

  • Fix several issues in checkct analysis
  • Fix choice option not showing the alternatives
  • Fix several parsing issues
  • Fix some download links in examples
  • Fix several issues in architecture handling
  • Fix compilation issues with OCaml 5

0.8.1 (2023-10-31)

** Misc

  • Add basic opcode replacement and address hook in SSE script
  • Add a registration mechanism for symbolic state
  • Add an option to disable the monitor screen when curses is installed
  • Small code improvements
  • Upgrade ocamlformat to 0.26.1

** Bugs

  • Fix some uncatched exceptions
  • Fix a bug in checkct preprocessing

0.8.0 (2023-07-14)

** Features

  • Add symbolic execution monitoring mechanism

** Documentation

** Examples

0.7.4 (2023-05-12)

** Bugs

  • Fix infinite loop on arm64 basic bloc disassembly

0.7.3 (2023-05-05)

** Bugs

  • Fix operator precedence issues in DBA parser
  • Expected fix for a hard to reproduce overlapping text issue at the end of SSE exploration
  • Fix issues with SSE intermediate representation

0.7.2 (2023-04-22)

** Bugs

  • Backport fixes for SSE intermediate representation

0.7.1 (2023-02-14)

** Features

  • New architecture support : Z80
  • New quick merging strategy in SSE
  • Support for custom array in SSE stubs

** Documentation

** Examples

0.6.3 (2022-12-08)

** Misc

  • Restore SSE timeout option
  • Enable non ELF nor PE file loading as a single contiguous bytes section

** Bugs

  • Fix rare issues with SMT solvers

0.6.2 (2022-11-09)

** Misc

  • Improve SSE SMT-LIB printer

** Bugs

  • Fix SSE screen not properly releasing the terminal
  • Fix SSE screen forget some pending logs
  • Correct typo from #17

0.6.1 (2022-09-23)

** Bugs

  • Fix the model extraction for newer versions of Bitwuzla
  • Fix the timeout handler for ocaml-bitwuzla when 4.09 <= ocaml < 4.13
  • Fix SSE not properly resetting the screen when an exception occurs

0.6.0 (2022-09-22)

** Features

  • New architecture support : RISC V 64bit
  • Catch interrupt signal (CTRL-C) in SSE in order to print exploration summary gracefully
  • Switch between log and monitor screen in SSE by pressing space (require curses)

** Documentation

** Bugs

  • Fix bitvector canonical representation
  • Fix compatibility issues with unisim-archisec.0.0.3
  • Fix issues with new experimental SSE engine

0.5.0 (2022-04-18)

** Features

  • Alternative experimental SSE engine (enabled with -sse-alternative-engine)
  • Core dump support in SSE initialization
  • Self-modifying code support in SSE (enabled with -sse-self-written-enum N)

** Examples

0.4.1 (2021-12-20)

** Features

  • Reworked Backward Bounded Symbolic Execution (together with some documentation)

** Misc

** Bug

  • Fix an issue with 64-bit kernel virtual addresses

0.4.0 (2021-10-12)

** Features

  • New architecture support : ARMv7 Thumb mode (requires unisim_archisec)
  • New architecture support : AARCH64 (requires unisim_archisec)
  • New architecture support : AMD64 (requires unisim_archisec)
  • Backward Bounded Symbolic Execution (experimental)
  • Reworked Static Symbolic Execution (together with some documentation)

** Dropped features (until rework)

  • Static Abstract Interpretation
  • Dynamic Symbolic Execution

** Misc

  • Use Dune build system
  • Remove several system dependencies (PIQI, ZMQ)

0.3.0 (2020-01-21)

** Features

  • New architecture support : RISC-V 32 bits
  • Support for DWARF-4 debug instruction format
  • Support to import IDA control-flow graph
  • Add documented plugin creation example : mnemonic count [mcount]
  • New Makefile 'library' to ease plugin creation

** Fixes

  • Fix (vectorized instructions) x86 decoder

** Misc

  • Detach PINSEC to own repository (support to be deprecated in later version)

0.2.0 (2018-10-01)

  • New symbolic execution engine
  • New interpreter for binary code
  • Improved logical representation for formulas
  • New internal control-flow-graph representation
  • Directive language for symbolic execution control
  • Support for new PIN tool xtrasec

  • Improved x86 decoder

    • Fixed bugs reported by KAIST

  • Docker support

    • includes Unisim-vp ARM v7 decoder
    • includes new PIN tool xtrasec

0.1.0 (2017-03-01)

First release

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct