Static single assignment with Binary Ninja

This notebook demonstrates MLIL SSA queries against the Trivision webs binary, including possible-value ranges and def-use relationships for a memcpy size argument.

• Notebook: Static Single Assignment with Binary Ninja.ipynb
• Example output: mlil_ssa_output.csv
• Companion video

Requirements

• Binary Ninja Commercial with its Python API installed
• Python with JupyterLab

Get the sample

The sample comes from the EMUX Trivision firmware:

wget https://github.com/therealsaumil/emux/raw/refs/heads/master/files/emux/firmware/TRI227WF/rootfs.tar.bz2
bzip2 -d rootfs.tar.bz2
tar -xf rootfs.tar
cp rootfs/usr/bin/webs TRI227WF_webs

Open TRI227WF_webs in Binary Ninja, allow analysis to finish, and save a BNDB. The example focuses on the function at 0xb7e8 and the memcpy call at 0xb834; addresses depend on loading the same firmware build.

Run the notebook

python3 -m venv .venv
source .venv/bin/activate
python "/Applications/Binary Ninja.app/Contents/Resources/scripts/install_api.py"
python -m pip install jupyterlab pandas
jupyter lab "Static Single Assignment with Binary Ninja.ipynb"

Adjust the Binary Ninja application path on non-default or non-macOS installations. Possible-value results depend on Binary Ninja's analysis and are not a standalone vulnerability finding.

References

• Binary Ninja SSA basics
• Binary Ninja intermediate languages
• Vulnerability modeling with Binary Ninja
• EMUX