Binary Ninja: native C++ plugin via MLIL SSA

[kyle-elliott-tob]

Summary

Build a native C++ Binary Ninja plugin that simplifies MBA expressions using CoBRA's core library. Operate at the Medium Level IL SSA (MLIL SSA) level, which provides explicit SSA variables and typed expression trees that map cleanly to CoBRA's Expr model.

Architecture

lib/binja/
  CobraBinja.cpp              — Plugin entry, command registration
  MLILDetector.cpp            — MBA detection via MLIL SSA expression walking
  MLILDetector.h
  MLILReconstructor.cpp       — Simplified Expr → MLIL or annotation output
  MLILReconstructor.h

Integration Point

• Register a PluginCommand or workflow action
• Can operate in two modes:
  • Whole-function scan: Walk all MLIL SSA instructions, detect and simplify MBA candidates
  • Selection-based: User selects an expression, plugin simplifies it
• Results applied as inline comments/annotations on the HLIL view, or via Binja's expression replacement API if available

MLIL SSA → Expr Bridge

Map Binary Ninja MLIL operations to CoBRA Expr kinds:

Binja MLIL op	CoBRA Expr
MLIL_ADD	Expr::Add
MLIL_SUB	Expr::Add + Expr::Negate
MLIL_MUL / MLIL_MULU_DP	Expr::Mul
MLIL_AND	Expr::BitwiseAnd
MLIL_OR	Expr::BitwiseOr
MLIL_XOR	Expr::BitwiseXor
MLIL_NOT	Expr::BitwiseNot
MLIL_NEG	Expr::Negate
MLIL_LSR	Expr::LogicalShr (constant shift)
MLIL_CONST / MLIL_CONST_PTR	Expr::Constant
MLIL_VAR_SSA	Expr::Variable

Evaluator

Build evaluator lambda from MLIL SSA expression trees — assign values to leaf SSA variables and evaluate the expression tree. MLIL SSA's explicit def-use chains make this straightforward.

Detection Heuristic

Walk MLIL SSA instructions looking for expression trees that mix arithmetic and bitwise operations. Same heuristic as the LLVM pass: count ops, require both categories, enforce minimum tree size and variable cap.

Output Strategy

Binary Ninja's IL layers are analysis results, not easily patched in-place. Options for presenting simplified results:

1. Inline comments: Add comments to HLIL showing simplified form (e.g., /* cobra: x + y */)
2. Tag annotations: Use Binja's tag system to mark simplified expressions
3. Expression replacement: Investigate Function.set_user_* APIs for direct expression patching
4. Log output: Print simplified forms to Binja's log console with address references

Recommend starting with inline comments (option 1) as it requires no IL mutation. Investigate expression replacement for v2.

Cross-Block Support

Leverage the same function-level detection architecture as the LLVM pass: post-order block traversal, reverse instruction walk, function-scope deduplication, phi-transparent tree building (Binja MLIL SSA has explicit phi functions via MLIL_VAR_PHI).

Build System

• COBRA_BUILD_BINJA_PLUGIN CMake option
• Requires Binary Ninja install path or API headers (BINJA_API_DIR)
• Binary Ninja ships C++ API headers and binaryninjaapi / binaryninjacore libraries
• Links against cobra-core (static)
• Produces cobra_binja.so / cobra_binja.dylib / cobra_binja.dll plugin

Task List

• CMake infrastructure for Binja plugin (API detection, plugin target)
• Plugin entry point: command registration, metadata
• MLIL SSA → Expr bridge (BuildExprFromMLIL)
• MLIL SSA evaluator (EvaluateMLIL)
• MBA detection heuristic for MLIL SSA
• Output: inline comments with simplified expressions
• Cost gate integration
• Variable remapping for aux var elimination
• Cross-block / phi support (MLIL_VAR_PHI)
• Investigate expression replacement APIs for direct IL patching
• Testing strategy

References

• Binary Ninja C++ API
• MLIL SSA has explicit MLIL_VAR_PHI nodes — maps to our phi-transparent detection
• Binja plugins are shared libraries exporting CorePluginInit