package binsec
Semantic analysis of binary executables
Install
Dune Dependency
Authors
-
AAdel Djoudi
-
BBenjamin Farinier
-
CChakib Foulani
-
DDorian Lesbre
-
FFrédéric Recoules
-
GGuillaume Girol
-
JJosselin Feist
-
LLesly-Ann Daniel
-
MManh-Dung Nguyen
-
MMathéo Vergnolle
-
MMathilde Ollivier
-
MMatthieu Lemerre
-
OOlivier Nicole
-
RRichard Bonichon
-
RRobin David
-
SSébastien Bardin
-
SSoline Ducousso
-
TTa Thanh Dinh
-
YYaëlle Vinçont
Maintainers
Sources
binsec-0.7.3.tbz
sha256=05c507b9b2d96387499eb5c8be676db6be1604a9941e367fc19b8da90ea903be
sha512=e18c5d5e65e53a912b54948a8c66723023acdc84ff26edb627d6f88272447d277f379d51b567523a242b17036c5a44fc94861587d8bd3b08e077782073de4bee
doc/CHANGES.html
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
- 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
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
when4.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
(requirecurses
)
** 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
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
- 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
0.4.1 (2021-12-20)
** 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
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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page