Triton学习笔记(三)

Triton我看重的就两点，一是可以让我不用写C/C++, 另一点就是本篇要开始讲的重点，符号执行，这篇先介绍符号执行

首先看官方给的例子:

# src/examples/python/ir.py
#!/usr/bin/env python2
## -*- coding: utf-8 -*-

import  sys
from    triton import *


code = [
    (0x400000, "\x48\x8b\x05\xb8\x13\x00\x00"), # mov        rax, QWORD PTR [rip+0x13b8]
    (0x400007, "\x48\x8d\x34\xc3"),             # lea        rsi, [rbx+rax*8]
    (0x40000b, "\x67\x48\x8D\x74\xC3\x0A"),     # lea        rsi, [ebx+eax*8+0xa]
    (0x400011, "\x66\x0F\xD7\xD1"),             # pmovmskb   edx, xmm1
    (0x400015, "\x89\xd0"),                     # mov        eax, edx
    (0x400017, "\x80\xf4\x99"),                 # xor        ah, 0x99
    (0x40001a, "\xC5\xFD\x6F\xCA"),             # vmovdqa    ymm1, ymm2
]



if __name__ == '__main__':

    #Set the arch
    setArchitecture(ARCH.X86_64)

    for (addr, opcodes) in code:
        # Build an instruction
        inst = Instruction()

        # Setup opcodes
        inst.setOpcodes(opcodes)

        # Setup Address
        inst.setAddress(addr)

        # optional - Update register state
        inst.updateContext(Register(REG.RAX,  12345));
        inst.updateContext(Register(REG.RBX,  67890));

        # optional - Add memory access <addr, size, content>
        inst.updateContext(MemoryAccess(0x66666666, 8, 0x31003200330034));

        # Process everything
        processing(inst)

        # Display instruction
        print inst

        # Display symbolic expressions
        for expr in inst.getSymbolicExpressions():
            print '\t', expr

        print

    sys.exit(0)

$ python src/examples/python/ir.py
0x400000: mov rax, qword ptr [rip + 0x13b8]
	ref!0 = ((_ zero_extend 0) (concat ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)))) ; MOV operation
	ref!1 = ((_ zero_extend 0) (_ bv4194311 64)) ; Program Counter
.......
0x400007: lea rsi, qword ptr [rbx + rax*8]
	ref!2 = ((_ zero_extend 0) (bvadd (_ bv0 64) (bvadd (_ bv67890 64) (bvmul ((_ extract 63 0) ref!0) (_ bv8 64))))) ; LEA operation
	ref!3 = ((_ zero_extend 0) (_ bv4194315 64)) ; Program Counter
.......

输出结果的第一行是汇编代码，下面的几行就是符号表达式了

符号表达式说简单点就是把一个变量的变化用表达式表示出来

其实只要理解了每个符号所代表的意义，还是很容易理解的，末尾也有注释

比如:

ref!1 = ((_ zero_extend 0) (_ bv4194311 64)) ; Program Counter

后面的注释很明显，程序指针，也就是eip, 其中(_ bv4194311 64)表示一个64bit的数，值的十进制表示为4194311，转成十六进制就是0x400007, (_ zero_extend 0)表示剩余为用0填充，4194311是不够64bit的，所以前面要用0到64bit

所以这个符号表达式翻译成简单的表达式就是eip = 0x400007, 很好理解的，执行完这句指令后，下句指令的地址就是0x400007

为啥要用这么复杂的一个符号表达式来表示这么简单的一句指令呢? 我认为应该是涉及到污点染色，会在之后的篇章中介绍

ref!0 = ((_ zero_extend 0) (concat ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)) ((_ extract 7 0) (_ bv0 8)))) ; MOV operation

看注释就知道，这句表达式是mov操作的表达式，处于学习阶段我们就耐心的慢慢读表达式，等都理解之后可以使用专门的模块进行处理.

((_ extract 7 0) (_ bv0 8))这句很简单，一个8bit的数0，取0-7bit的数，来举一个特例来解释下把，比如((_ extract 4 1) (_ bv93 8))的值是14

化简后就是: ((_ zero_extend 0) (concat 0 0 0 0 0 0 0 0)), concat的作用就是把后面8个8bit的0连接起来，因为赋值给rax, 用了qword指针，所以是64位

因为示例不是实际代码, [eip+0x13b8]指向的地址值未知，所以这里是0

我们继续往底下看，下一句指令是lea rsi, qword ptr [rbx + rax*8]

符号表达式是:

ref!2 = ((_ zero_extend 0) (bvadd (_ bv0 64) (bvadd (_ bv67890 64) (bvmul ((_ extract 63 0) ref!0) (_ bv8 64))))) ; LEA operation

其中ref!0从上面我们可以看出表示的是rax, 所以((_ extract 63 0) ref!0)表示的就是rax，如果改成((_ extract 31 0) ref!0)则表示的就是32为的rax也就是eax

我们对表达式进行化简: (bvadd 0 (bvadd 67890 (bvmul rax 8)))

(bvmul rax 8)也就是rax*8

bvadd表示加法

剩下看的就简单了: rax*8 + 67890 + 0

我们在python代码中初始化过rbx的值:

inst.updateContext(Register(REG.RBX, 67890));

所以67890表示的就是rbx

这句表达式就容易理解了，rsi = rax*8 + rbx

总结

介绍暂时就介绍这些，Triton的符号表达式引擎用的是SMT2-LIB, 所以要知道某句表达式的意思可以去参考官方文档

1. The SMT-LIBv2 Language and Tools: A Tutorial
2. The SMT-LIBv2 Theories Library