Miasm Symbolic Execution Skill
Status: ✅ Production Ready
Source: CEA-SEC Miasm Framework (3.8K stars)
Interop: blackhat-go adversarial bisimulation games
GF(3): ERGODIC (0) - transformation/mediation role
Conscious Hacker Integration Philosophy
The conscious hacker recognizes that offensive and defensive security are dual:
blackhat-go (attack chains) ←→ miasm-symbolic (program understanding)
↓ ↓
Order matters (Ungar) State equivalence (Bisim)
↓ ↓
MINUS (-1) ERGODIC (0)
Together with a defense verification skill (+1), this maintains GF(3) conservation.
Overview
Miasm provides:
- 16 Architectures: x86_16/32/64, ARM, MIPS, AArch64, PPC, SH4, MSP430, MEP
- IR Lifting: Assembly → Intermediate Representation
- Symbolic Execution: Constraint solving for path exploration
- Emulation: JIT-based binary emulation
- DSE: Dynamic Symbolic Execution
GF(3) Role Assignment
| Component | Trit | Role | |-----------|------|------| | Disassembly (r2/miasm) | -1 | MINUS - deconstruction | | IR Lifting (miasm) | 0 | ERGODIC - transformation | | Symbolic Exec (miasm) | +1 | PLUS - construction |
Conservation: (-1) + (0) + (+1) = 0 ✓
Adversarial Bisimulation Bridge to blackhat-go
Attack Chain Verification
When blackhat-go executes an Ungar game attack chain, miasm can verify semantics:
from miasm_r2_bridge import MiasmR2Bridge
# blackhat-go attack: shellcode injection
attack_chain = ["go-concurrency", "shellcode-inject", "process-hollow"]
# miasm verification: does shellcode do what attacker claims?
bridge = MiasmR2Bridge(shellcode_path, "x86_64")
# Lift to IR and symbolically execute
ir = bridge.lift_to_ir(entry_point, shellcode_bytes)
symbolic_state = bridge.symbolic_exec(ir)
# Check: does shellcode reach claimed goal state?
goal_reached = symbolic_state.check_constraint(goal_condition)
Bisimulation: Semantic Equivalence
Two binaries are bisimilar if miasm symbolic execution shows they produce equivalent observable states:
def check_binary_bisimilar(bin1: bytes, bin2: bytes) -> bool:
"""
Check if two binaries are behaviorally equivalent.
Used in blackhat-go bisimulation games for defense validation.
"""
bridge1 = MiasmR2Bridge(bin1, "x86_64")
bridge2 = MiasmR2Bridge(bin2, "x86_64")
sym1 = bridge1.symbolic_exec_full()
sym2 = bridge2.symbolic_exec_full()
# Compare final symbolic states
return sym1.is_equivalent(sym2)
Game Message Protocol
{
"type": "miasm/verify",
"game_id": "bisim-001",
"player": "arbiter",
"action": {
"operation": "symbolic_equivalence_check",
"binary1_hash": "abc123",
"binary2_hash": "def456"
},
"result": {
"bisimilar": true,
"constraints_matched": 42,
"paths_explored": 1337
},
"trit": 0
}
Supported Architectures
from miasm.analysis.machine import Machine
ARCHITECTURES = Machine.available_machine()
# ['arml', 'armb', 'armtl', 'armtb', 'sh4', 'x86_16', 'x86_32', 'x86_64',
# 'msp430', 'mips32b', 'mips32l', 'aarch64l', 'aarch64b', 'ppc32b',
# 'mepl', 'mepb']
Core Capabilities
1. Disassembly with Gay.jl Coloring
from miasm_r2_bridge import MiasmR2Bridge, GayColor
bridge = MiasmR2Bridge("/path/to/binary", "x86_64")
colors = GayColor(seed=1069)
instrs = bridge.disassemble_function(0x1000, code_bytes)
for instr in instrs:
print(f"{instr['addr']}: {instr['mnemonic']} | {instr['color']}")
2. IR Lifting
# Lift x86_64 instruction to miasm IR
ir = bridge.lift_to_ir(0x1000, shellcode)
# Result: {'addr': '0x1000', 'asm': 'MOV RAX, 0x42',
# 'ir': [{'dst': 'RAX', 'src': '0x42'}]}
3. Symbolic Execution
from miasm.ir.symbexec import SymbolicExecutionEngine
from miasm.expression.expression import ExprId, ExprInt
# Create symbolic state
symbols = {
ExprId("RAX", 64): ExprId("RAX_init", 64), # Symbolized
ExprId("RBX", 64): ExprInt(0, 64), # Concrete
}
# Execute symbolically
engine = SymbolicExecutionEngine(ir_arch, symbols)
final_state = engine.run_at(ir_cfg, entry_addr)
# Query: what value does RAX hold?
rax_expr = final_state.eval_expr(ExprId("RAX", 64))
4. Constraint Solving (with Z3)
from miasm.ir.translators.z3_ir import TranslatorZ3
translator = TranslatorZ3()
z3_expr = translator.from_expr(rax_expr)
# Solve for input that makes RAX == 0x1337
import z3
solver = z3.Solver()
solver.add(z3_expr == 0x1337)
if solver.check() == z3.sat:
model = solver.model()
print(f"Input to reach RAX=0x1337: {model}")
blackhat-go Interoperability
Ungar Game: Attack Verification
// blackhat-go side
game := NewUngarGame(kb)
game.AttackerMove("shellcode-inject")
// MCP message to miasm
msg := MCPMessage{
Type: "miasm/verify_attack",
Payload: AttackVerification{
Technique: "shellcode-inject",
Shellcode: shellcodeBytes,
ClaimedBehavior: "spawns /bin/sh",
},
}
// miasm verifies via symbolic execution
response := miasmService.Verify(msg)
if response.Verified {
game.ArbiterVerify() // GF(3) balance maintained
}
Bisimulation Game: Defense Equivalence
// blackhat-go: are two defenses equivalent?
bisim := NewBisimulationGame(kb, defense1, defense2)
// Use miasm to check binary-level equivalence
miasmCheck := miasm.CheckBisimilar(defense1.Binary, defense2.Binary)
if miasmCheck.Equivalent {
// Defender wins: defenses are observationally equivalent
bisim.DefenderWins()
}
Installation
# Requires pyparsing < 3 for miasm compatibility
uv venv --python 3.11 /tmp/miasm_venv
source /tmp/miasm_venv/bin/activate
uv pip install "pyparsing==2.4.7" miasm future
# Optional: Z3 for constraint solving
uv pip install z3-solver
Three Worlds Integration
| World | Seed | miasm Role | blackhat-go Role | |-------|------|------------|------------------| | 🔴 ZAHN | 1069 | Verify attack semantics | Execute attack chains | | 🟢 JULES | 69 | Check binary equivalence | Validate defenses | | 🔵 FABRIZ | 0 | Arbiter symbolic proofs | Arbiter game state |
MCP Tool Exposure
{
"tools": [
{
"name": "miasm_disassemble",
"description": "Disassemble bytes with miasm",
"parameters": {
"arch": "x86_64",
"bytes": "base64-encoded",
"addr": "0x1000"
}
},
{
"name": "miasm_lift_ir",
"description": "Lift assembly to miasm IR",
"parameters": {
"arch": "x86_64",
"bytes": "base64-encoded"
}
},
{
"name": "miasm_symbolic_exec",
"description": "Run symbolic execution",
"parameters": {
"ir": "ir-json",
"symbols": {"RAX": "symbolic"}
}
},
{
"name": "miasm_check_bisimilar",
"description": "Check if two binaries are bisimilar",
"parameters": {
"binary1": "base64",
"binary2": "base64",
"depth": 100
}
}
]
}
Conscious Hacker Principles
- Understand before attack: Use miasm to understand what code actually does
- Verify claims: Don't trust attacker claims without symbolic verification
- Defense through understanding: Bisimulation proves defense equivalence
- GF(3) balance: Every attack (-1) needs understanding (0) and defense (+1)
Related Skills
| Skill | Trit | Role | |-------|------|------| | blackhat-go | -1 | Attack chains, Ungar games | | miasm-symbolic | 0 | IR lifting, symbolic exec | | narya-proofs | +1 | Formal verification |
Conservation: (-1) + (0) + (+1) = 0 ✓
Contributors (CEA-SEC)
| Contributor | Role | Followers | |-------------|------|-----------| | serpilliere | Creator | 107 | | commial (Camille Mougey) | Core dev | 286 | | mrphrazer (Tim Blazytko) | Contributor | 521 | | mrexodia (Duncan Ogilvie) | x64dbg creator | 3,334 |
File Locations
~/.claude/skills/miasm-symbolic/SKILL.md # This skill
~/iii/src/miasm_r2_bridge.py # Bridge implementation
~/iii/r2con-integration/ # r2con integration
"The conscious hacker uses miasm not to attack, but to understand—and through understanding, to protect."
Autopoietic Marginalia
The interaction IS the skill improving itself.
Every use of this skill is an opportunity for worlding:
- MEMORY (-1): Record what was learned
- REMEMBERING (0): Connect patterns to other skills
- WORLDING (+1): Evolve the skill based on use
Add Interaction Exemplars here as the skill is used.