Triton学习笔记(三)

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

首先看官方给的例子:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
# 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)
1
2
3
4
5
6
7
8
9
$ 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 = ((_ zeroextend 0) ( bv4194311 64)) ; Program Counter

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

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

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

ref!0 = ((_ zeroextend 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 = ((_ zeroextend 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
文章目录
  1. 1. 总结