https://github.com/binsec/binsec - 0.10.1

CHANGES:

** 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

- OCaml
Published by recoules 8 months ago

https://github.com/binsec/binsec - 0.10.0

CHANGES:

** 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

- OCaml
Published by recoules about 1 year ago

https://github.com/binsec/binsec - 0.9.1

CHANGES:

** Misc

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

** Bugs

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

- OCaml
Published by recoules almost 2 years ago

https://github.com/binsec/binsec - 0.9.0

CHANGES:

** 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

- OCaml
Published by recoules almost 2 years ago

https://github.com/binsec/binsec - 0.8.2

CHANGES:

** 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

- OCaml
Published by recoules almost 2 years ago

https://github.com/binsec/binsec - 0.8.1

CHANGES:

** 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

- OCaml
Published by recoules over 2 years ago

https://github.com/binsec/binsec - 0.8.0

CHANGES:

** Features

• Add symbolic execution monitoring mechanism

** Documentation

• Add the tutorial "Checking constant-time security property"
• Add the tutorial "Monitoring the symbolic execution with a custom plugin"

** Examples

• Add a shadow stack SSE plugin
• Add a re-implementation of the relational symbolic engine

- OCaml
Published by recoules over 2 years ago

https://github.com/binsec/binsec - 0.7.4

CHANGES:

** Bugs

• Fix infinite loop on arm64 basic bloc disassembly

- OCaml
Published by recoules almost 3 years ago

https://github.com/binsec/binsec - 0.7.3

CHANGES:

** 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

- OCaml
Published by recoules almost 3 years ago

https://github.com/binsec/binsec - 0.7.2

CHANGES:

** Bugs

• Backport fixes for SSE intermediate representation

- OCaml
Published by recoules almost 3 years ago

https://github.com/binsec/binsec - 0.7.1

CHANGES:

** Features - New architecture support : Z80 - New quick merging strategy in SSE - Support for custom array in SSE stubs

** Documentation

• Add the write-up "FCSC 2022: Licorne"

** Examples

• Add SSE prechall challenge from FCSC 2022
• Add SSE souk challenge from FCSC 2022
• Add SSE licorne challenge from FCSC 2022

- OCaml
Published by recoules about 3 years ago

https://github.com/binsec/binsec - 0.6.3

CHANGES:

** 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

- OCaml
Published by recoules about 3 years ago

https://github.com/binsec/binsec - 0.6.2

CHANGES:

** 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

- OCaml
Published by recoules over 3 years ago

https://github.com/binsec/binsec - 0.7.0-alpha

CHANGES:

** Features - New architecture support : Z80 - New quick merging strategy in SSE - Support for custom array in SSE stubs

** Documentation

• Add the write-up "FCSC 2022: Licorne"

** Examples

• Add SSE prechall challenge from FCSC 2022
• Add SSE souk challenge from FCSC 2022
• Add SSE licorne challenge from FCSC 2022

- OCaml
Published by recoules over 3 years ago

https://github.com/binsec/binsec - 0.6.1

CHANGES:

** 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

- OCaml
Published by recoules over 3 years ago

https://github.com/binsec/binsec - 0.6.0

CHANGES:

** 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

• Broaden the SSE manual reference
• Add the write-up "How to read the SSE exploration board"

** Bugs

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

- OCaml
Published by recoules over 3 years ago

https://github.com/binsec/binsec - 0.5.0

CHANGES:

** 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

• Add SSE FlareOn 2021 challenge 2
• Add SSE gugus challenge from crackmes.one
• Add SSE hidden_password challenge from crackmes.one with dedicated write-up
• Add SSE license_checker_3 challenge from crackmes.one
• Add SSE trycrackme challenge from crackmes.one with dedicated write-up

- OCaml
Published by recoules almost 4 years ago

https://github.com/binsec/binsec - 0.4.1

CHANGES:

** Features

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

** Misc

• Support native OCaml bitwuzla binding

** Bug

• Fix an issue with 64-bit kernel virtual addresses

- OCaml
Published by recoules about 4 years ago

https://github.com/binsec/binsec - 0.4.0

CHANGES:

** 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)

- OCaml
Published by recoules over 4 years ago

https://github.com/binsec/binsec - binsec 0.2 beta

This is the beta version of the forthcoming 0.2 release of BINSEC.

- OCaml
Published by rbonichon over 7 years ago