Program analysis and bindings in Haskell for binary ninja with support for the medium level SSA intermediate language.
Symlink binary ninja core shared objects to package root.
For example on MacOS:
ln -s /Applications/Binary\ Ninja.app/Contents/MacOS/libbinaryninjacore.dylib libbinaryninjacore.dylibln -s /Applications/Binary\ Ninja.app/Contents/MacOS/libbinaryninjacore.1.dylib libbinaryninjacore.1.dylib
Or pass stack the directory where libbinaryninjacore is located.
Then build and exec the demo (after changing the path to your license and binary/bndb of interest) with stack.
- stack init
- stack build --extra-lib-dirs "$(pwd)"
- stack run example --extra-lib-dirs "$(pwd)" -- +RTS -N14 -sstats -RTS
Haddock-generated documentation is hosted here.
Tested and implemented against an ultimate license install.
The main branch tracks the current work-in-progress.
This repo requires binary ninja version dev/5.4.9588 Ultimate. Other ultimate versions may work though assume it's not tested.
To upgrade binja version it's advised to compare the results of unit_test.sh between the known working version
and new version.
All haskell files are formatted with https://github.com/tweag/ormolu
The primary inspiration of Beluga is Frama-C's Eva plugin. I've found numerous bugs in C codebases with Eva and I want the same experience with binary ninja's MLIL SSA intermediate language.
Frama-c book: Guide to Software Verification with Frama-C
Sophia d'Antoine of Margin Research taught a course, Program Analysis for Vulnerability Research, which covered abstract interpretation implementation in Binary Ninja.