Skip to content

Commit c999cda

Browse files
shoucshouc
committedJan 16, 2022
add qsym diff
1 parent 5228a51 commit c999cda

File tree

6 files changed

+542
-0
lines changed

6 files changed

+542
-0
lines changed
 

‎did_digfuzz_contribute.py

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
import os
2+
import config
3+
import qemu_instr
4+
5+
_executor = qemu_instr.STDINExecutorQEMU(config.QEMU_BIN, config.LOCAL_UNINSTRUMENTED_EXEC_PATH)
6+
qemu = qemu_instr.QEMUInstr(_executor, config.DUMPER_PATH, shm_key=config.SHM_KEY)
7+
tests = list(filter(lambda x: "digfuzz" not in x and not x.startswith("."), os.listdir("out/m/queue")))
8+
qemu.build_execution_tree(["out/m/queue/" + x for x in tests])
9+
10+
tests = list(filter(lambda x: "digfuzz" in x and not x.startswith("."), os.listdir("out/m/queue")))
11+
12+
for filename in ["out/m/queue/" + x for x in tests]:
13+
with open(filename, "rb") as fp:
14+
corpus_content = fp.read()
15+
qemu.executor.execute_test_case(corpus_content)
16+
try:
17+
trace = qemu.executor.dump_trace()
18+
except EOFError as e:
19+
print(f"[Crash] Found crash {filename} with error {e}, skipping")
20+
qemu.executor.restart_bin()
21+
continue
22+
for i in trace:
23+
if i not in qemu.execution_tree:
24+
print(i, filename)

‎preachfuzz.py

+68
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
#!/usr/bin/env python
2+
# coding: utf-8
3+
import angr
4+
import claripy
5+
import time
6+
import os
7+
8+
import config
9+
from llvm_instr import GDBExecutor
10+
branch_instrs = ["ja","jae","jb","jbe","jc","je","jecxz","jg","jge","jl","jle","jna","jnae","jnb","jnbe","jnc","jne","jng",
11+
"jnge","jnl","jnle","jno","jnp","jns","jnz","jo","jp","jpe","jpo","js","jz"]
12+
cmp_instrs = ["cmp", "test","FUCOM","FUCOMP","FUCOMPP","FUCOMI","FUCOMIP","FTST","FXAM","FCOM","FCOMP","FCOMPP","FICOM","FICOMP","FCOMI","FCOMIP"]
13+
14+
floc = f"/tmp/objdump-log-{time.time()}"
15+
os.system(f"objdump -d {config.LOCAL_UNINSTRUMENTED_EXEC_PATH} > {floc}")
16+
17+
mapping = {}
18+
19+
gdb = GDBExecutor(config.LOCAL_UNINSTRUMENTED_EXEC_PATH)
20+
hardest_path = [f"test.c:{x}:-1".encode("ascii") for x in [13, 19, 23, 26, 27, 30, 31, 34, 35, 38, 39, 42, 43, 46, 47]]
21+
22+
solve_for_addr = []
23+
24+
for i in hardest_path:
25+
addrs = gdb.get_addr(i)
26+
solve_for_addr.append(addrs[0])
27+
solve_for_addr.append(addrs[1])
28+
29+
print(solve_for_addr)
30+
# for line in open(floc).read().split("\n"):
31+
# line_arr = line.split("\t")
32+
# if len(line_arr) > 2 and ("nop" in line_arr[-1]):
33+
# continue
34+
# if record_next or driver_part:
35+
# if len(line_arr) > 1:
36+
# pc = int("0x" + line_arr[0].split(":")[0].replace(" ", ""), 16)
37+
# self.__non_comp_bb.add(pc)
38+
# record_next = False
39+
#
40+
# # todo: parse instead of direct match
41+
# if len(line_arr) > 2 and ("call" in line_arr[-1] or "jmp" in line_arr[-1]):
42+
# record_next = True
43+
# if len(line_arr) == 1:
44+
# record_next = True
45+
# driver_part = False
46+
# if len(line_arr) == 1 and ("<main>" in line_arr[-1] or "<__libc_csu" in line_arr[-1]):
47+
# driver_part = True
48+
49+
50+
p = angr.Project('harness')
51+
52+
53+
state = p.factory.full_init_state(
54+
args=['./harness', 'v'],
55+
56+
add_options=angr.options.unicorn,
57+
stdin=angr.SimFile,
58+
)
59+
state.options.add(angr.options.LAZY_SOLVES)
60+
61+
while True:
62+
succ = state.step()
63+
if len(succ.successors) == 2:
64+
break
65+
state = succ.successors[0]
66+
67+
68+
print(state)

‎qsym.diff

+390
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,390 @@
1+
diff --git a/Dockerfile b/Dockerfile
2+
index 3c99259..c9425af 100644
3+
--- a/Dockerfile
4+
+++ b/Dockerfile
5+
@@ -10,3 +10,6 @@ COPY . /workdir/qsym
6+
7+
RUN ./setup.sh
8+
RUN pip install .
9+
+RUN cd /workdir/qsym/qsym/pintool && make -j${nproc}
10+
+RUN mkdir /tmp/in
11+
+RUN mkdir /tmp/out
12+
\ No newline at end of file
13+
diff --git a/qsym/pintool/solver.cpp b/qsym/pintool/solver.cpp
14+
index 147334f..b50c5a1 100644
15+
--- a/qsym/pintool/solver.cpp
16+
+++ b/qsym/pintool/solver.cpp
17+
@@ -127,9 +127,9 @@ void Solver::add(z3::expr expr) {
18+
z3::check_result Solver::check() {
19+
uint64_t before = getTimeStamp();
20+
z3::check_result res;
21+
- LOG_STAT(
22+
- "SMT: { \"solving_time\": " + decstr(solving_time_) + ", "
23+
- + "\"total_time\": " + decstr(before - start_time_) + " }\n");
24+
+ // LOG_STAT(
25+
+ // "SMT: { \"solving_time\": " + decstr(solving_time_) + ", "
26+
+ // + "\"total_time\": " + decstr(before - start_time_) + " }\n");
27+
// LOG_DEBUG("Constraints: " + solver_.to_smt2() + "\n");
28+
try {
29+
res = solver_.check();
30+
@@ -146,15 +146,14 @@ z3::check_result Solver::check() {
31+
return res;
32+
}
33+
34+
+void Solver::fake_check(){
35+
+ // printf("BB\n%lu%sBBEND\n", last_pc_, solver_.to_smt2().c_str());
36+
+}
37+
+
38+
+
39+
bool Solver::checkAndSave(const std::string& postfix) {
40+
- if (check() == z3::sat) {
41+
- saveValues(postfix);
42+
- return true;
43+
- }
44+
- else {
45+
- LOG_DEBUG("unsat\n");
46+
- return false;
47+
- }
48+
+ fake_check();
49+
+ return true;
50+
}
51+
52+
void Solver::addJcc(ExprRef e, bool taken, ADDRINT pc) {
53+
@@ -174,49 +173,41 @@ void Solver::addJcc(ExprRef e, bool taken, ADDRINT pc) {
54+
55+
// check duplication before really solving something,
56+
// some can be handled by range based constraint solving
57+
- bool is_interesting;
58+
- if (pc == 0) {
59+
- // If addJcc() is called by special case, then rely on last_interested_
60+
- is_interesting = last_interested_;
61+
- }
62+
- else
63+
- is_interesting = isInterestingJcc(e, taken, pc);
64+
65+
- if (is_interesting)
66+
- negatePath(e, taken);
67+
- addConstraint(e, taken, is_interesting);
68+
+ negatePath(e, taken);
69+
+ addConstraint(e, taken, false);
70+
}
71+
72+
void Solver::addAddr(ExprRef e, ADDRINT addr) {
73+
- llvm::APInt v(e->bits(), addr);
74+
- addAddr(e, v);
75+
+// llvm::APInt v(e->bits(), addr);
76+
+// addAddr(e, v);
77+
}
78+
79+
void Solver::addAddr(ExprRef e, llvm::APInt addr) {
80+
- if (e->isConcrete())
81+
- return;
82+
-
83+
- if (last_interested_) {
84+
- reset();
85+
- // TODO: add optimize in z3
86+
- syncConstraints(e);
87+
- if (check() != z3::sat)
88+
- return;
89+
- z3::expr &z3_expr = e->toZ3Expr();
90+
-
91+
- // TODO: add unbound case
92+
- z3::expr min_expr = getMinValue(z3_expr);
93+
- z3::expr max_expr = getMaxValue(z3_expr);
94+
- solveOne(z3_expr == min_expr);
95+
- solveOne(z3_expr == max_expr);
96+
- }
97+
-
98+
- addValue(e, addr);
99+
+// if (e->isConcrete())
100+
+// return;
101+
+//
102+
+// if (last_interested_) {
103+
+// reset();
104+
+// // TODO: add optimize in z3
105+
+// syncConstraints(e);
106+
+// if (check() != z3::sat)
107+
+// return;
108+
+// z3::expr &z3_expr = e->toZ3Expr();
109+
+//
110+
+// // TODO: add unbound case
111+
+// z3::expr min_expr = getMinValue(z3_expr);
112+
+// z3::expr max_expr = getMaxValue(z3_expr);
113+
+// solveOne(z3_expr == min_expr);
114+
+// solveOne(z3_expr == max_expr);
115+
+// }
116+
+//
117+
+// addValue(e, addr);
118+
}
119+
120+
void Solver::addValue(ExprRef e, ADDRINT val) {
121+
- llvm::APInt v(e->bits(), val);
122+
- addValue(e, v);
123+
+// llvm::APInt v(e->bits(), val);
124+
+// addValue(e, v);
125+
}
126+
127+
void Solver::addValue(ExprRef e, llvm::APInt val) {
128+
@@ -234,31 +225,31 @@ void Solver::addValue(ExprRef e, llvm::APInt val) {
129+
}
130+
131+
void Solver::solveAll(ExprRef e, llvm::APInt val) {
132+
- if (last_interested_) {
133+
- std::string postfix = "";
134+
- ExprRef expr_val = g_expr_builder->createConstant(val, e->bits());
135+
- ExprRef expr_concrete = g_expr_builder->createBinaryExpr(Equal, e, expr_val);
136+
-
137+
- reset();
138+
- syncConstraints(e);
139+
- addToSolver(expr_concrete, false);
140+
-
141+
- if (check() != z3::sat) {
142+
- // Optimistic solving
143+
- reset();
144+
- addToSolver(expr_concrete, false);
145+
- postfix = "optimistic";
146+
- }
147+
-
148+
- z3::expr z3_expr = e->toZ3Expr();
149+
- while(true) {
150+
- if (!checkAndSave(postfix))
151+
- break;
152+
- z3::expr value = getPossibleValue(z3_expr);
153+
- add(value != z3_expr);
154+
- }
155+
- }
156+
- addValue(e, val);
157+
+// if (last_interested_) {
158+
+// std::string postfix = "";
159+
+// ExprRef expr_val = g_expr_builder->createConstant(val, e->bits());
160+
+// ExprRef expr_concrete = g_expr_builder->createBinaryExpr(Equal, e, expr_val);
161+
+//
162+
+// reset();
163+
+// syncConstraints(e);
164+
+// addToSolver(expr_concrete, false);
165+
+//
166+
+// if (check() != z3::sat) {
167+
+// // Optimistic solving
168+
+// reset();
169+
+// addToSolver(expr_concrete, false);
170+
+// postfix = "optimistic";
171+
+// }
172+
+//
173+
+// z3::expr z3_expr = e->toZ3Expr();
174+
+// while(true) {
175+
+// if (!checkAndSave(postfix))
176+
+// break;
177+
+// z3::expr value = getPossibleValue(z3_expr);
178+
+// add(value != z3_expr);
179+
+// }
180+
+// }
181+
+// addValue(e, val);
182+
}
183+
184+
UINT8 Solver::getInput(ADDRINT index) {
185+
@@ -293,58 +284,41 @@ void Solver::readInput() {
186+
inputs_.push_back((UINT8)ch);
187+
}
188+
189+
-std::vector<UINT8> Solver::getConcreteValues() {
190+
- // TODO: change from real input
191+
- z3::model m = solver_.get_model();
192+
- unsigned num_constants = m.num_consts();
193+
- std::vector<UINT8> values = inputs_;
194+
- for (unsigned i = 0; i < num_constants; i++) {
195+
- z3::func_decl decl = m.get_const_decl(i);
196+
- z3::expr e = m.get_const_interp(decl);
197+
- z3::symbol name = decl.name();
198+
-
199+
- if (name.kind() == Z3_INT_SYMBOL) {
200+
- int value = e.get_numeral_int();
201+
- values[name.to_int()] = (UINT8)value;
202+
- }
203+
- }
204+
- return values;
205+
-}
206+
207+
void Solver::saveValues(const std::string& postfix) {
208+
- std::vector<UINT8> values = getConcreteValues();
209+
-
210+
- // If no output directory is specified, then just print it out
211+
- if (out_dir_.empty()) {
212+
- printValues(values);
213+
- return;
214+
- }
215+
-
216+
- std::string fname = out_dir_+ "/" + toString6digit(num_generated_);
217+
- // Add postfix to record where it is genereated
218+
- if (!postfix.empty())
219+
- fname = fname + "-" + postfix;
220+
- ofstream of(fname, std::ofstream::out | std::ofstream::binary);
221+
- LOG_INFO("New testcase: " + fname + "\n");
222+
- if (of.fail())
223+
- LOG_FATAL("Unable to open a file to write results\n");
224+
-
225+
- // TODO: batch write
226+
- for (unsigned i = 0; i < values.size(); i++) {
227+
- char val = values[i];
228+
- of.write(&val, sizeof(val));
229+
- }
230+
-
231+
- of.close();
232+
- num_generated_++;
233+
+// std::vector<UINT8> values = getConcreteValues();
234+
+//
235+
+// // If no output directory is specified, then just print it out
236+
+// if (out_dir_.empty()) {
237+
+// printValues(values);
238+
+// return;
239+
+// }
240+
+//
241+
+// std::string fname = out_dir_+ "/" + toString6digit(num_generated_);
242+
+// // Add postfix to record where it is genereated
243+
+// if (!postfix.empty())
244+
+// fname = fname + "-" + postfix;
245+
+// ofstream of(fname, std::ofstream::out | std::ofstream::binary);
246+
+// LOG_INFO("New testcase: " + fname + "\n");
247+
+// if (of.fail())
248+
+// LOG_FATAL("Unable to open a file to write results\n");
249+
+//
250+
+// // TODO: batch write
251+
+// for (unsigned i = 0; i < values.size(); i++) {
252+
+// char val = values[i];
253+
+// of.write(&val, sizeof(val));
254+
+// }
255+
+//
256+
+// of.close();
257+
+// num_generated_++;
258+
}
259+
260+
void Solver::printValues(const std::vector<UINT8>& values) {
261+
- fprintf(stderr, "[INFO] Values: ");
262+
- for (unsigned i = 0; i < values.size(); i++) {
263+
- fprintf(stderr, "\\x%02X", values[i]);
264+
- }
265+
- fprintf(stderr, "\n");
266+
+// fprintf(stderr, "[INFO] Values: ");
267+
+// for (unsigned i = 0; i < values.size(); i++) {
268+
+// fprintf(stderr, "\\x%02X", values[i]);
269+
+// }
270+
+// fprintf(stderr, "\n");
271+
}
272+
273+
z3::expr Solver::getPossibleValue(z3::expr& z3_expr) {
274+
@@ -352,40 +326,19 @@ z3::expr Solver::getPossibleValue(z3::expr& z3_expr) {
275+
return m.eval(z3_expr);
276+
}
277+
278+
-z3::expr Solver::getMinValue(z3::expr& z3_expr) {
279+
- push();
280+
- z3::expr value(context_);
281+
- while (true) {
282+
- if (checkAndSave()) {
283+
- value = getPossibleValue(z3_expr);
284+
- solver_.add(z3::ult(z3_expr, value));
285+
- }
286+
- else
287+
- break;
288+
- }
289+
- pop();
290+
- return value;
291+
-}
292+
293+
-z3::expr Solver::getMaxValue(z3::expr& z3_expr) {
294+
- push();
295+
- z3::expr value(context_);
296+
- while (true) {
297+
- if (checkAndSave()) {
298+
- value = getPossibleValue(z3_expr);
299+
- solver_.add(z3::ugt(z3_expr, value));
300+
- }
301+
- else
302+
- break;
303+
- }
304+
- pop();
305+
- return value;
306+
+void Solver::addToSolver(ExprRef e, bool taken) {
307+
+ if (!taken)
308+
+ e = g_expr_builder->createLNot(e);
309+
+ add(e->toZ3Expr());
310+
}
311+
312+
-void Solver::addToSolver(ExprRef e, bool taken) {
313+
- e->simplify();
314+
+void Solver::addToSolverDump(ExprRef e, bool taken) {
315+
if (!taken)
316+
e = g_expr_builder->createLNot(e);
317+
+ z3::solver s(context_);
318+
+ s.add(e->toZ3Expr());
319+
+ std::cout << "FLIPME" << last_pc_ << "\n" << s.to_smt2() << "FLIPMEEND\n";
320+
add(e->toZ3Expr());
321+
}
322+
323+
@@ -518,21 +471,25 @@ bool Solver::isInterestingJcc(ExprRef rel_expr, bool taken, ADDRINT pc) {
324+
void Solver::negatePath(ExprRef e, bool taken) {
325+
reset();
326+
syncConstraints(e);
327+
- addToSolver(e, !taken);
328+
- bool sat = checkAndSave();
329+
- if (!sat) {
330+
- reset();
331+
- // optimistic solving
332+
- addToSolver(e, !taken);
333+
- checkAndSave("optimistic");
334+
- }
335+
+ addToSolverDump(e, taken);
336+
+
337+
+
338+
+
339+
+
340+
+ fake_check();
341+
+// if (!sat) {
342+
+// reset();
343+
+// // optimistic solving
344+
+// addToSolver(e, !taken);
345+
+// checkAndSave("optimistic");
346+
+// }
347+
}
348+
349+
void Solver::solveOne(z3::expr z3_expr) {
350+
- push();
351+
- add(z3_expr);
352+
- checkAndSave();
353+
- pop();
354+
+// push();
355+
+// add(z3_expr);
356+
+// checkAndSave();
357+
+// pop();
358+
}
359+
360+
void Solver::checkFeasible() {
361+
diff --git a/qsym/pintool/solver.h b/qsym/pintool/solver.h
362+
index e37f091..a7dbcbf 100644
363+
--- a/qsym/pintool/solver.h
364+
+++ b/qsym/pintool/solver.h
365+
@@ -65,15 +65,13 @@ protected:
366+
void checkOutDir();
367+
void readInput();
368+
369+
- std::vector<UINT8> getConcreteValues();
370+
void saveValues(const std::string& postfix);
371+
void printValues(const std::vector<UINT8>& values);
372+
373+
z3::expr getPossibleValue(z3::expr& z3_expr);
374+
- z3::expr getMinValue(z3::expr& z3_expr);
375+
- z3::expr getMaxValue(z3::expr& z3_expr);
376+
377+
void addToSolver(ExprRef e, bool taken);
378+
+ void addToSolverDump(ExprRef e, bool taken);
379+
void syncConstraints(ExprRef e);
380+
381+
void addConstraint(ExprRef e, bool taken, bool is_interesting);
382+
@@ -88,6 +86,8 @@ protected:
383+
void solveOne(z3::expr);
384+
385+
void checkFeasible();
386+
+
387+
+ void fake_check();
388+
};
389+
390+
extern Solver* g_solver;

‎targets/bzip2/build.sh

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
git clone https://github.com/libigl/libigl.git target
2+
pushd target
3+
mkdir build
4+
pushd build
5+
cmake -DLIBIGL_WITH_OPENGL=OFF \
6+
-DLIBIGL_WITH_OPENGL_GLFW=OFF \
7+
-DLIBIGL_WITH_OPENGL_GLFW_IMGUI=OFF \
8+
-DLIBIGL_WITH_COMISO=OFF \
9+
-DLIBIGL_WITH_EMBREE=OFF \
10+
-DLIBIGL_WITH_PNG=OFF \
11+
-DLIBIGL_WITH_TETGEN=OFF \
12+
-DLIBIGL_WITH_TRIANGLE=OFF \
13+
-DLIBIGL_WITH_PREDICATES=OFF \
14+
-DLIBIGL_WITH_XML=OFF \
15+
-DLIBIGL_BUILD_TESTS=OFF \
16+
..
17+
CXXFLAGS=-no-pie make -j$(nproc)
18+
popd
19+
20+
g++ -no-pie make -DIGL_STATIC_LIBRARY \
21+
-I./include \
22+
-isystem ./include \
23+
-isystem ./external/eigen \
24+
-c ../fuzz.cc -o fuzzer.o
25+
26+
g++ -no-pie fuzzer.o ./build/libigl.a ../../../driver.o -o harness

‎targets/bzip2/fuzz.c

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include "bzlib.h"
2+
#include <stdint.h>
3+
#include <stdlib.h>
4+
#include <assert.h>
5+
#include <string.h>
6+
7+
extern int BZ2_bzBuffToBuffDecompress(char* dest,
8+
unsigned int* destLen,
9+
char* source,
10+
unsigned int sourceLen,
11+
int small,
12+
int verbosity);
13+
14+
int
15+
LLVMFuzzerTestOneInput(const uint8_t *data, size_t size)
16+
{
17+
int r, small;
18+
unsigned int nZ, nOut;
19+
20+
// See: https://github.com/google/bzip2-rpc/blob/master/unzcrash.c#L39
21+
nOut = size*2;
22+
char *outbuf = malloc(nOut);
23+
small = size % 2;
24+
r = BZ2_bzBuffToBuffDecompress(outbuf, &nOut, (char *)data, size,
25+
small, /*verbosity=*/0);
26+
27+
if (r != BZ_OK) {
28+
#ifdef __DEBUG__
29+
fprintf(stdout, "Decompression error: %d\n", r);
30+
#endif
31+
}
32+
free(outbuf);
33+
return 0;
34+
}

‎targets/wasm3/build.sh

Whitespace-only changes.

0 commit comments

Comments
 (0)
Please sign in to comment.