Skip to content

Latest commit

 

History

History
97 lines (78 loc) · 2.3 KB

README.md

File metadata and controls

97 lines (78 loc) · 2.3 KB
Raw

Symbolic Execution Engine Modoki

What is this?

  • this is Symbolic Engine built on z3py
  • and well(?) designed for education scene
  • but there're very tight limitations
    • for more information, see Limitations

How to run?

try running test script:

./test.py

Requirements

  • python2
  • z3py
  • (nasm/ndisasm)

Limitations

target machine

Currently, engine targets following machine spec:

  • based on Intel architecture
  • supports x86_64 ISA partially
  • NO data memory (Only Code on memory)
  • NO stack

instructions

Following few Intel x86_64 instructions are supported:

  • add
  • mov
  • inc
  • dec
  • cmp
  • jz (je)
  • jnz (jne)
  • jg
  • jl

There may be miss understanding semantics.

Instructions must be decoded like:

insts = [
    (0x0,   4, arch.OP_TYPE_RDST | arch.OP_TYPE_IVAL, "cmp", "rsi", 1),
    (0x4,   2, arch.OP_TYPE_IVAL, "jl", 8), # 0x6 + 8 = 0xe
    (0x6,   3, arch.OP_TYPE_RDST | arch.OP_TYPE_RSRC, "add", "rdx", "rdx"),
    (0x9,   3, arch.OP_TYPE_RDST, "dec", "rsi"),
    (0xc,   2, arch.OP_TYPE_IVAL, "jnz", -8), # 0xe - 8 = 0x6
    (0xe,   3, arch.OP_TYPE_RDST | arch.OP_TYPE_RSRC, "cmp", "rdx", "rax"),
    (0x11,  2, arch.OP_TYPE_IVAL, "je", 1), # 0x13 + 1 = 0x14
    (0x13,  1, arch.OP_TYPE_NOOP, "ret"),
    (0x14,  1, arch.OP_TYPE_NOOP, "nop"),
]

each fileds means:

    # decoded instruction format
    FIELD_INST_ADDR = 0      # instruction address
    FIELD_INST_SIZE = 1      # instruction byte size
    FIELD_INST_OP_TYPE = 2   # instruction operand types
    FIELD_INST_NAME = 3      # instruction name 
    FIELD_INST_OP_DST = 4    # instrunction destination X
    FIELD_INST_OP_SRC = 5    # instruction source X

    # operand type
    OP_TYPE_NOOP = 1 << 0       # no operands
    OP_TYPE_RDST = 1 << 1       # destination register. if memory, None
    OP_TYPE_RSRC = 1 << 2       # source register. if memory, None
    OP_TYPE_IVAL = 1 << 3       # immediate value
    OP_TYPE_MDST = 1 << 4       # future work (memory address or register name comes here for simplicity)
    OP_TYPE_MSRC = 1 << 5       # future work

registers

supports:

  • general registers: all
  • flag registers: ZF, SF

not supports:

  • flag registers: CF, OF, and so on

refactoring

This is alpha version. Hard effort to refactoring (including spell miss) is needed.