4. OUTLINE
? main() is not the really main
? OllyDBG:Baby First (Exam)
? Return-oriented Programming
? Overflow: Revo Wolf(Exam)
? Fuzzing
? Make a fuzzer in C++
? How to fuzzing with Z3
16. REALLY MAIN
? Label “_start” is really main.
? CRTStartUp is loaded in label “_start”.
(To init RTC/new/delete/arg…etc)
? Find programmer’s main (normal c plus compile)
? Find the address calling GetCommandLine
? Find the address calling exit() or cexit()
? Programmer’s main function is between them.
51. BUFFER OVERFLOW
? We just can see , cannot modify the application.
? For Exploit?
? Overflow local variables. (EBP+N are good friend to us)
? Do something for get control EIP/RIP.
81. “ Fuzz testing or fuzzing is a software testing technique,
often automated or semi-automated, that involves
providing invalid, unexpected, or random data to the
inputs of a computer program. The program is then
monitored for exceptions such as crashes, or failing
built-in code assertions or for finding potential memory
leaks. Fuzzing is commonly used to test for security
problems in software or computer systems. It is a form
of random testing which has been used for testing
hardware or software.
From Wikipedia
WHAT IS
FUZZING?
82. When we need to
fuzz?A. Prove that something is always true
B. Fuzzing for something unexpected
C.Fuckinnnnnnnnnnnnng Crypto
D.A lot of choice, find one is correct
108. Z3 BEGIN
?Get and Install Python2.7
? Z3.py script environment
? www.python.org
?You can use python basically
?Get Z3.py for Windows
? Prove tool
? github.com/Z3Prover/z3/wiki/Using-Z3Py-on-Windows
111. FUZZING(Z3)
BitVec(“Name” , BitCount)
For example:
1.char a => a = BitVec(“a”, 8)
2.short b => b = BitVec(“b”, 16)
3.int c => c = BitVec(“C”, 32) => Int(“c”)
4.bool e => e = BitVec(‘e’, 8)
112. FUZZING(Z3)
Solve(All rules ), Z3 will auto fuzz all variables,
and find a result(JUST ONE RESULT!).
Then, print all results of variables.
113. FUZZING(Z3)
If you have a looooot of rules,
you can use Solver().
Solver.add() can remember
all rules you requested.
114. FUZZING(Z3)
If you want to check current
whether rules can come true,
you just use: Solver.check()
117. FUZZING(Z3)
Finally, if you get “sat”,
you can use: Solver.model()
It will save a result in it.
Use model[Variable Name],
and get the answer by String