package binsec
 sectionYPositions = computeSectionYPositions($el), 10)"
  x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
  >
  
  
On This Page
  
  
  Semantic analysis of binary executables
Install
    
    dune-project
 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.4.tbz
    
    
        
    
  
  
  
    
  
  
    
  
        sha256=ee45b9a6d54aebfb2b860c8fa7548ad85afbf1da3fe65cee10529c8a0934b8d6
    
    
  sha512=493658d337a96bf6ac7b54b162717aeb31c527348a50552bad8f9b0f3f08791295e89c09b02b3f1c8cfa3913d57625c791e4e80322477e2a5f974ca7d85d57ae
    
    
  doc/CHANGES.html
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 prechallchallenge from FCSC 2022
- Add SSE soukchallenge from FCSC 2022
- Add SSE licornechallenge 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-bitwuzlawhen4.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 guguschallenge from crackmes.one
- Add SSE hidden_passwordchallenge from crackmes.one with dedicated write-up
- Add SSE license_checker_3challenge from crackmes.one
- Add SSE trycrackmechallenge 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