Simplifier — Linux Port

A Linux port of Simplifier by Mazeworks Security — a high-performance framework for deobfuscating Mixed Boolean-Arithmetic (MBA) expressions.

---

Motivations behind this Linux port

There are two reasons behind this Linux port :

1. I use this amazing project in a pipeline and I need to containerize it for maintainability purpose.
2. This project also served as an experiment to evaluate LLM-assisted multi-language porting on a technically complex codebase. This project was a good way to benchmark it as it uses different languages and mixed boolean arithmetic expressions is a complex subject which I thought current models would not understand.

I was helped by Claude Sonnet 4.6 via Claude Code for this project.

What is MBA?

Mixed Boolean-Arithmetic expressions combine arithmetic operations (addition, multiplication) with bitwise operations (AND, OR, XOR, NOT) in ways that are semantically equivalent to much simpler expressions. They are commonly used to obfuscate code.

Example :

x + y = (x & y) + (x | y)

A very good blog post has been made by Justus Polzin on MBA : https://plzin.github.io/posts/mba

For MBA deobfuscation you have this blog post from Matteo Favaro and Tim Blazytko : https://secret.club/2022/08/08/eqsat-oracle-synthesis.html

---

Requirements

Dependency	Minimum version
.NET SDK	8
CMake	3.16
GCC or Clang	GCC 11+ / Clang 13+ (C++20)
Rust toolchain	stable

---

Building

Docker

$ git clone https://github.com/arueco/SimplifierLinux.git
$ cd SimplifierLinux
$ docker build -t simplifier-mba .

From source

$ git clone https://github.com/arueco/SimplifierLinux.git
$ cd SimplifierLinux
$ ./build-linux.sh

The build script runs three steps in order:

1. C++ — CMake → native/libMba.FFI.so, native/libEspresso.so
2. Rust — cargo build --release → EqSat/target/release/libeq_sat.so (links against libMba.FFI.so)
3. .NET — dotnet publish → publish/Simplifier

All output lands in publish/.

---

Usage

Docker

$ docker run -it simplifier-mba Simplifier "<expression>" [options]

If compiled from source (in publish/)

$ ./Simplifier "<expression>" [options]

Options

Flag	Description
-b <N>	Bit width of variables (default: 64)
-z	Verify equivalence of input and result using Z3 (up to 10s timeout)
-e	Enable equality saturation alongside the standard pipeline (64-bit only)
-l	Run only the linear simplifier
-c, --clean	Strip type annotations (e.g. :i64) from the output
-h	Print help

Examples

Basic simplification:

$ ./Simplifier "(x & y) + (x | y)"


Expression: ((x:i64&y:i64)+(x:i64|y:i64))



Simplified to: (y:i64+x:i64)

with cost: 3

32-bit expression with Z3 verification:

$ ./Simplifier "(x & y) + (x | y)" -b 32 -z


Expression: ((x:i32&y:i32)+(x:i32|y:i32))



Simplified to: (y:i32+x:i32)

with cost: 3
Proving equivalence...

Expressions are equivalent.

Clean output (no type annotations):

./Simplifier "x^(x&y)" -c

Expression: (x:i64^(x:i64&y:i64))



Simplified to: (x&(~y))

with cost: 4

---

Architecture

The project has three components compiled as shared libraries and linked by the .NET host:

publish/
├── Simplifier          ← .NET host binary
├── libeq_sat.so        ← Rust: equality saturation engine (egg-based e-graphs)
├── libMba.FFI.so       ← C++: LLVM Groebner basis, polynomial utilities
└── libEspresso.so      ← C++: Boolean minimization (Espresso algorithm)

---

Linux Port Notes

This port adapts the Windows-only original to Linux x86-64. Key changes:

Area	Change
JIT (Rust + C#)	Windows x64 ABI (first arg in RCX) → System V AMD64 (RDI); a mov rcx, rdi stub is emitted on Linux
Memory management	VirtualAlloc/VirtualProtect/VirtualFree → mmap/mprotect/munmap
Export visibility	__declspec(dllexport) → __attribute__((visibility("default")))
LLVM config headers	Target triple and feature flags updated for x86_64-pc-linux-gnu
Native build system	Visual Studio .vcxproj replaced with CMakeLists.txt
Runtime library paths	libeq_sat.so built with -rpath,$ORIGIN so both .so files resolve from the same directory
Truth table DB paths	Resolved relative to the executable directory (not CWD) using std::env::current_exe()
-c / --clean flag	Added to strip :i<N> type annotations from output

---

Maintenance & Upstream Policy

This Linux port is independent from the original project.

It will not track upstream Windows changes and may diverge permanently.

No guarantees are made regarding future updates, compatibility, or support.

Credits

This project is licensed under the GNU General Public License v3.0 (GPL-3.0), in accordance with the original Simplifier project.

Original project and research by Mazeworks Security.