binsec/binsec

Stars
301
Rank 133,584 (Top 3 %)
Language
OCaml
License
GNU Lesser Genera...
Created about 6 years ago
Updated 2 months ago

binsec/binsec

binsec

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

BINSEC binary-level open-source platform

BINSEC

BINSEC is an open-source toolset to help improve software security at the binary level. It relies on cutting-edge research in binary code analysis, at the intersection of formal methods, program analysis, security and software engineering. It is powered up by state-of-the-art techniques such as binary-level formal methods, symbolic execution, abstract interpretation, SMT solving and fuzzing.

Website

More information about BINSEC is available at: https://binsec.github.io/

Getting started

See install instructions.
Then, have a look at user documentation for command examples.

Contributing

Found a bug or want to make a suggestion, check how to contribute improving BINSEC.

xyntia

Xyntia, the black-box deobfuscator

Rel

Binsec/Rel is an extension of Binsec that implements relational symbolic execution for constant-time verification and secret-erasure at binary-level.

klee21-tina-artifact

TInA is an automated, generic, verification-friendly and trustworthy lifting technique turning GNU-style inline assembly into semantically equivalent C code amenable to verification, in order to take advantage of existing C analyzers.

haunted

Binsec/Haunted is an extension of Binsec to verify speculative constant-time and detect Spectre attacks.

icse2021-artifact992

preca

Constraint acquisition based precondition learner

rtas2021_artifact

haunted_bench

Benchmarks for Binsec/Rel tool.

binsec.github.io

www presence for the BINSEC binary-level analysis open-source platform

rel_bench

Benchmark (mostly cryptographic programs) for Binsec/Rel.

hade

tfml

cav2021-artifacts

esop2023_artefact

xtrasec

A (simple) PIN-based tracer for BINSEC

unisim_archisec

OCaml binding for the external UNISIM DBA decoder