Skip to content
This repository was archived by the owner on Aug 23, 2022. It is now read-only.

Commit 8a9856a

Browse files
pgoodmanpgoodman
authored
Klee maze example (#369)
* In progress. Working on an example of using KLEE on a Maze, but with the maze program being compiled to x86, amd64, and aarch64. * Making lots of progress on getting lifting and runnning an aarch64 maze program on amd64, but using --explicit_args. The key thing I'm working through right now is a jump offset table, but where the offset is a block pc, rather than a table base. Also adding various bits of code here and there to making runnning with klee more directly doable, and working on a debugging facility to track down when the emulated program counter gets out of sync with the original program. * Fixed a subtle @page and @PAGEOFF-related reference bug on AArch64. Partially disabled the special jump offset table handling I had in table.py, as it doesn't (yet) handle the shifted table values. However, I still have the code there, so that it can recognize that a basic block address is used as a possible offset, so that I can remove the block address as a reference, which permits a new heuristic on the C++ side to work. On the C++ side, when there's a jump instruction that isn't associated with a cross-reference flow, I try to auto-augment it with addition switch cases, targeting blocks with no predecessors (as present in the CFG). This seems to work reasonably well. * Improved the scripts and updated the READMEs. * Minor rephrase * Minor rephrase
1 parent bc17c70 commit 8a9856a

25 files changed

+1074
-297
lines changed

‎.gdbinit

+83-191
Original file line numberDiff line numberDiff line change
@@ -6,128 +6,37 @@ define print-rip
66
dont-repeat
77
end
88

9-
define print-reg-state-64
10-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
11-
printf " emulated native\n"
12-
printf "rip 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2408)), $rip
13-
printf "rax 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2152)), $rax
14-
printf "rbx 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2168)), $rbx
15-
printf "rcx 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2184)), $rcx
16-
printf "rdx 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2200)), $rdx
17-
printf "rsi 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2216)), $rsi
18-
printf "rdi 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2232)), $rdi
19-
printf "rbp 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2264)), $rbp
20-
printf "rsp 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2248)), $rsp
21-
printf "r8 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2280)), $r8
22-
printf "r9 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2296)), $r9
23-
printf "r10 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2312)), $r10
24-
printf "r11 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2328)), $r11
25-
printf "r12 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2344)), $r12
26-
printf "r13 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2360)), $r13
27-
printf "r14 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2376)), $r14
28-
printf "r15 0x%016lx 0x%016lx\n", *((unsigned long long *)($rptr + 2392)), $r15
29-
dont-repeat
30-
end
31-
32-
define addr-of-xmm0-64
33-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
34-
printf "&(RegState::xmm0) = 0x%016lx\n", $rptr + 16
35-
dont-repeat
36-
end
37-
38-
define addr-of-xmm1-64
39-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
40-
printf "&(RegState::xmm1) = 0x%016lx\n", $rptr + 80
41-
dont-repeat
42-
end
43-
44-
define addr-of-xmm2-64
45-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
46-
printf "&(RegState::xmm2) = 0x%016lx\n", $rptr + 144
47-
dont-repeat
48-
end
49-
50-
define addr-of-xmm3-64
51-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
52-
printf "&(RegState::xmm3) = 0x%016lx\n", $rptr + 208
53-
dont-repeat
54-
end
55-
56-
define addr-of-xmm4-64
57-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
58-
printf "&(RegState::xmm4) = 0x%016lx\n", $rptr + 272
59-
dont-repeat
60-
end
61-
62-
define addr-of-xmm5-64
63-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
64-
printf "&(RegState::xmm5) = 0x%016lx\n", $rptr + 336
65-
dont-repeat
66-
end
67-
68-
define addr-of-xmm6-64
69-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
70-
printf "&(RegState::xmm6) = 0x%016lx\n", $rptr + 400
71-
dont-repeat
72-
end
73-
74-
define addr-of-xmm7-64
75-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
76-
printf "&(RegState::xmm7) = 0x%016lx\n", $rptr + 464
77-
dont-repeat
78-
end
79-
80-
define addr-of-xmm8-64
81-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
82-
printf "&(RegState::xmm8) = 0x%016lx\n", $rptr + 528
83-
dont-repeat
84-
end
85-
86-
define addr-of-xmm9-64
87-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
88-
printf "&(RegState::xmm9) = 0x%016lx\n", $rptr + 592
89-
dont-repeat
90-
end
91-
92-
define addr-of-xmm10-64
93-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
94-
printf "&(RegState::xmm10) = 0x%016lx\n", $rptr + 656
95-
dont-repeat
96-
end
97-
98-
define addr-of-xmm11-64
99-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
100-
printf "&(RegState::xmm11) = 0x%016lx\n", $rptr + 720
101-
dont-repeat
102-
end
103-
104-
define addr-of-xmm12-64
105-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
106-
printf "&(RegState::xmm12) = 0x%016lx\n", $rptr + 784
107-
dont-repeat
108-
end
109-
110-
define addr-of-xmm13-64
111-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
112-
printf "&(RegState::xmm13) = 0x%016lx\n", $rptr + 848
113-
dont-repeat
114-
end
115-
116-
define addr-of-xmm14-64
117-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
118-
printf "&(RegState::xmm14) = 0x%016lx\n", $rptr + 912
119-
dont-repeat
120-
end
9+
set $__rax_offset = 2216
10+
set $__flags_offset = 2064
11+
set $__xmm0_offset = 16
12112

122-
define addr-of-xmm15-64
13+
define print-reg-state-amd64
12314
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
124-
printf "&(RegState::xmm15) = 0x%016lx\n", $rptr + 976
125-
dont-repeat
126-
end
127-
128-
define print-flags-64
129-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
130-
set $flptr = (char *) ($rptr + 0x810)
15+
printf " emulated native\n"
16+
set $__rax_ptr = $rptr + $__rax_offset
17+
printf "rip 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 16 * 16)), $rip
18+
printf "rax 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 0 * 16)), $rax
19+
printf "rbx 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 1 * 16)), $rbx
20+
printf "rcx 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 2 * 16)), $rcx
21+
printf "rdx 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 3 * 16)), $rdx
22+
printf "rsi 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 4 * 16)), $rsi
23+
printf "rdi 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 5 * 16)), $rdi
24+
printf "rsp 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 6 * 16)), $rsp
25+
printf "rbp 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 7 * 16)), $rbp
26+
printf "r8 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 8 * 16)), $r8
27+
printf "r9 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 9 * 16)), $r9
28+
printf "r10 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 10 * 16)), $r10
29+
printf "r11 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 11 * 16)), $r11
30+
printf "r12 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 12 * 16)), $r12
31+
printf "r13 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 13 * 16)), $r13
32+
printf "r14 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 14 * 16)), $r14
33+
printf "r15 0x%016lx 0x%016lx\n", *((unsigned long long *)($__rax_ptr + 15 * 16)), $r15
34+
dont-repeat
35+
end
36+
37+
define print-flags-amd64
38+
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
39+
set $flptr = (char *) ($rptr + $__flags_offset)
13140
printf "eflags ["
13241
if $flptr[1]
13342
printf "CF "
@@ -154,122 +63,105 @@ define print-flags-64
15463
dont-repeat
15564
end
15665

157-
define print-reg-state-32
158-
set $rptr = ((unsigned (*)(void))__mcsema_debug_get_reg_state)()
159-
printf " emulated native\n"
160-
printf "eip 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2408)), $eip
161-
printf "eax 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2152)), $eax
162-
printf "ebx 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2168)), $ebx
163-
printf "ecx 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2184)), $ecx
164-
printf "edx 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2200)), $edx
165-
printf "esi 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2216)), $esi
166-
printf "edi 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2232)), $edi
167-
printf "ebp 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2264)), $ebp
168-
printf "esp 0x%08lx 0x%016lx\n", *((unsigned long long *)($rptr + 2248)), $esp
169-
dont-repeat
66+
define print-flags-x86
67+
print-flags-amd64
17068
end
17169

172-
173-
define addr-of-rip
70+
define print-reg-state-x86
17471
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
175-
printf "&rip = 0x%016lx\n", $rptr + 2408
176-
dont-repeat
177-
end
178-
179-
define addr-of-rax
180-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
181-
printf "&rax = 0x%016lx\n", $rptr + 2152
182-
dont-repeat
183-
end
184-
185-
define addr-of-rbx
186-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
187-
printf "&rbx = 0x%016lx\n", $rptr + 2168
188-
dont-repeat
189-
end
190-
191-
define addr-of-rcx
192-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
193-
printf "&rcx = 0x%016lx\n", $rptr + 2184
194-
dont-repeat
195-
end
196-
197-
define addr-of-rdx
198-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
199-
printf "&rdx = 0x%016lx\n", $rptr + 2200
72+
printf " emulated native\n"
73+
set $__rax_ptr = $rptr + $__rax_offset
74+
printf "eip 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 16 * 16)), (unsigned) $pc
75+
printf "eax 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 0 * 16)), $eax
76+
printf "ebx 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 1 * 16)), $ebx
77+
printf "ecx 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 2 * 16)), $ecx
78+
printf "edx 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 3 * 16)), $edx
79+
printf "esi 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 4 * 16)), $esi
80+
printf "edi 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 5 * 16)), $edi
81+
printf "esp 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 6 * 16)), $esp
82+
printf "ebp 0x%08x 0x%08x\n", *((unsigned *)($__rax_ptr + 7 * 16)), $ebp
20083
dont-repeat
20184
end
20285

203-
define addr-of-rsi
204-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
205-
printf "&rsi = 0x%016lx\n", $rptr + 2216
206-
dont-repeat
207-
end
86+
set $__x0_offset = 544
20887

209-
define addr-of-rdi
88+
define print-reg-state-aarch64
21089
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
211-
printf "&rdi = 0x%016lx\n", $rptr + 2232
90+
printf "\temulated\n"
91+
set $__x0_ptr = $rptr + $__x0_offset
92+
set $__i = 0
93+
while $__i < 31
94+
printf "x%d\t0x%016lx\t&x%d = 0x%lx\n", $__i, *((unsigned long long *)($__x0_ptr + $__i * 16)), $__i, $__x0_ptr + $__i * 16
95+
set $__i = $__i + 1
96+
end
97+
98+
printf "sp\t0x%016lx\n", *((unsigned long long *)($__x0_ptr + $__i * 16))
99+
set $__i = $__i + 1
100+
printf "pc\t0x%016lx\t&pc = 0x%lx\n", *((unsigned long long *)($__x0_ptr + $__i * 16)), $__x0_ptr + $__i * 16
212101
dont-repeat
213102
end
214103

215-
define addr-of-rbp
216-
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
217-
printf "&rbp = 0x%016lx\n", $rptr + 2264
218-
dont-repeat
219-
end
220104

221-
define addr-of-rsp
105+
define addr-of-rip
222106
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
223-
printf "&rsp = 0x%016lx\n", $rptr + 2248
107+
set $__rax_ptr = $rptr + $__rax_offset
108+
printf "&rip = 0x%016lx\n", $__rax_ptr + 16 * 16
224109
dont-repeat
225110
end
226111

227-
228-
define addr-of-r8
112+
define addr-of-rax
229113
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
230-
printf "&r8 = 0x%016lx\n", $rptr + 2280
114+
set $__rax_ptr = $rptr + $__rax_offset
115+
printf "&rax = 0x%016lx\n", $__rax_ptr + 0 * 16
231116
dont-repeat
232117
end
233118

234-
define addr-of-r9
119+
define addr-of-rbx
235120
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
236-
printf "&r9 = 0x%016lx\n", $rptr + 2296
121+
set $__rax_ptr = $rptr + $__rax_offset
122+
printf "&rbx = 0x%016lx\n", $__rax_ptr + 1 * 16
237123
dont-repeat
238124
end
239125

240-
define addr-of-r10
126+
define addr-of-rcx
241127
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
242-
printf "&r10 = 0x%016lx\n", $rptr + 2312
128+
set $__rax_ptr = $rptr + $__rax_offset
129+
printf "&rcx = 0x%016lx\n", $__rax_ptr + 2 * 16
243130
dont-repeat
244131
end
245132

246-
define addr-of-r11
133+
define addr-of-rdx
247134
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
248-
printf "&r11 = 0x%016lx\n", $rptr + 2328
135+
set $__rax_ptr = $rptr + $__rax_offset
136+
printf "&rdx = 0x%016lx\n", $__rax_ptr + 3 * 16
249137
dont-repeat
250138
end
251139

252-
define addr-of-r12
140+
define addr-of-rsi
253141
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
254-
printf "&r12 = 0x%016lx\n", $rptr + 2344
142+
set $__rax_ptr = $rptr + $__rax_offset
143+
printf "&rsi = 0x%016lx\n", $__rax_ptr + 4 * 16
255144
dont-repeat
256145
end
257146

258-
define addr-of-r13
147+
define addr-of-rdi
259148
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
260-
printf "&r13 = 0x%016lx\n", $rptr + 2360
149+
set $__rax_ptr = $rptr + $__rax_offset
150+
printf "&rdi = 0x%016lx\n", $__rax_ptr + 5 * 16
261151
dont-repeat
262152
end
263153

264-
define addr-of-r14
154+
define addr-of-rsp
265155
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
266-
printf "&r14 = 0x%016lx\n", $rptr + 2376
156+
set $__rax_ptr = $rptr + $__rax_offset
157+
printf "&rsp = 0x%016lx\n", $__rax_ptr + 6 * 16
267158
dont-repeat
268159
end
269160

270-
define addr-of-r15
161+
define addr-of-rbp
271162
set $rptr = ((unsigned long long (*)(void))__mcsema_debug_get_reg_state)()
272-
printf "&r15 = 0x%016lx\n", $rptr + 2392
163+
set $__rax_ptr = $rptr + $__rax_offset
164+
printf "&rbp = 0x%016lx\n", $__rax_ptr + 7 * 16
273165
dont-repeat
274166
end
275167

‎CMakeLists.txt

+3
Original file line numberDiff line numberDiff line change
@@ -105,3 +105,6 @@ install(
105105

106106
install(CODE
107107
"execute_process(COMMAND python ${PROJECT_SOURCE_DIR}/tools/setup.py install -f --prefix=${CMAKE_INSTALL_PREFIX})")
108+
109+
add_subdirectory(examples)
110+

‎README.md

+4-1
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ Why would anyone translate binaries *back* to bitcode?
3131

3232
* **Binary Patching And Modification**. Lifting to LLVM IR lets you cleanly modify the target program. You can run obfuscation or hardening passes, add features, remove features, rewrite features, or even fix that pesky typo, grammatical error, or insane logic. When done, your new creation can be recompiled to a new binary sporting all those changes. In the [Cyber Grand Challenge](https://blog.trailofbits.com/2015/07/15/how-we-fared-in-the-cyber-grand-challenge/), we were able to use McSema to translate challenge binaries to bitcode, insert memory safety checks, and then re-emit working binaries.
3333

34-
* **Symbolic Execution with KLEE**. [KLEE](https://klee.github.io/) operates on LLVM bitcode, usually generated by providing source to the LLVM toolchain. McSema can lift a binary to LLVM bitcode, [permitting KLEE to operate on previously unavailable targets](https://blog.trailofbits.com/2014/12/04/close-encounters-with-symbolic-execution-part-2/).
34+
* **Symbolic Execution with KLEE**. [KLEE](https://klee.github.io/) operates on LLVM bitcode, usually generated by providing source to the LLVM toolchain. McSema can lift a binary to LLVM bitcode, [permitting KLEE to operate on previously unavailable targets](https://blog.trailofbits.com/2014/12/04/close-encounters-with-symbolic-execution-part-2/). See our [walkthrough](examples/Maze/README.md) showing how to run KLEE on a symbolic maze.
3535

3636
* **Re-use existing LLVM-based tools**. KLEE is not the only tool that becomes available for use on bitcode. It is possible to run LLVM optimization passes and other LLVM-based tools like [libFuzzer](http://llvm.org/docs/LibFuzzer.html) on [lifted bitcode](docs/UsingLibFuzzer.md).
3737

@@ -71,8 +71,11 @@ sudo apt-get install \
7171
git \
7272
cmake \
7373
python2.7 python-pip \
74+
wget \
7475
build-essential \
7576
gcc-multilib g++-multilib \
77+
libtinfo-dev \
78+
lsb-release \
7679
realpath
7780

7881
sudo pip install --upgrade pip

‎examples/CMakeLists.txt

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
# Copyright (c) 2017 Trail of Bits, Inc.
2+
#
3+
# Licensed under the Apache License, Version 2.0 (the "License");
4+
# you may not use this file except in compliance with the License.
5+
# You may obtain a copy of the License at
6+
#
7+
# http://www.apache.org/licenses/LICENSE-2.0
8+
#
9+
# Unless required by applicable law or agreed to in writing, software
10+
# distributed under the License is distributed on an "AS IS" BASIS,
11+
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
# See the License for the specific language governing permissions and
13+
# limitations under the License.
14+
15+
project(examples)
16+
cmake_minimum_required (VERSION 3.2)
17+
18+
add_executable(maze Maze/Maze.c)

‎examples/Maze/.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
bc/*
2+
klee-*

0 commit comments

Comments
 (0)