package binsec
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
sha256=b8e7b9c756245656c481e992549fb7b1864ee6eeb492e16488e7a9d962d39cdb
sha512=07a5e4105e5275751fcc6832743f5f9eedc72bd061273ec54c4466135032852120df3784ba571656c788e5f3cd971aad8a53f030336a364e77e940e26dff38d7
CHANGES.md.html
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
analysisFix 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 installedSmall code improvements
Upgrade
ocamlformat
to0.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
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
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
Add the write-up "FCSC 2022: Licorne"
** Examples
Add SSE
prechall
challenge from FCSC 2022Add SSE
souk
challenge from FCSC 2022Add 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 gracefullySwitch 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.oneAdd SSE
hidden_password
challenge from crackmes.one with dedicated write-upAdd SSE
license_checker_3
challenge from crackmes.oneAdd 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