Secure your code as it's written. Use Snyk Code to scan source code in minutes - no build needed - and fix issues immediately.
def test():
from manticore.native import Manticore
if __name__ == "__main__":
import sys
prog = sys.argv[1]
params = sys.argv[2:]
else:
prog = "test_exploit_generation_example/bof"
params = ["AAAAAAAAAAAAAAAAAAAAAAA"]
m = Manticore(prog, params)
m.verbosity(2)
# 'trace' will contain the executed instructions
m.context["trace"] = []
# None: The hook will be applied to all the instructions
@m.hook(None)
def record_trace(state):
pc = state.cpu.PC
ins = state.cpu.instruction
# Store the instruction
with m.locked_context() as c:
c["trace"] += [pc]
# We manipulate directly capstone instruction
c["last_ins"] = "%s %s" % (ins.mnemonic, ins.op_str)
# print(state.cpu)
r2 = r2pipe.open(file)
r2.cmd("aaa")
for x in range(0, 11):
dis = r2.cmd("pdf @ sym.check_char_{}".format(x))
dis = dis.decode()
entry = int(dis.split("\n")[4].split()[1], 16)
for line in dis.split("\n"):
# print(line)
if "exit" in line:
exit_call = int(line.split()[2], 16)
elif "je 0x" in line:
je_statement = int(line.split()[2], 16)
addrs.append((entry, je_statement, exit_call))
m = Manticore(file)
m.context["solved"] = False
buff_addr = None
@m.hook(0x4009A4)
def hook(state):
""" Jump over `puts` and `fgets` calls """
state.cpu.EIP = 0x4009C1
@m.hook(0x4009C8)
def hook(state):
""" Inject symbolic buffer instead of fgets """
buff_addr = state.cpu.RDI
with m.locked_context() as context:
context["buff_addr"] = state.cpu.RDI
print("Buf addr: {:x}".format(buff_addr))
buffer = state.new_symbolic_buffer(12)
def symbolic_run(prog, params, trace, pc_crash):
print("Starting symbolic execution")
trace_set = set(trace)
m = Manticore(prog, params)
# The hook will be applied only to the instruction @pc_crash
@m.hook(pc_crash)
def crash_analysis(state):
# Add the constraint on eax
state.constrain(state.cpu.EAX == 0x0804887C) # 0x0804887c = @call_me
# Retrieve the arguments corresponding to argv[1]
argv_1 = next((i for i in state.input_symbols if i.name == "ARGV1"), None)
if argv_1:
# Ask the value of argv_1 to the solver
val_argv_1 = state.solve_one(argv_1)
# Pretty print of the solution
print("The solution is:")
print("\\x" + "\\x".join("{:02x}".format(c) for c in val_argv_1))
state.abandon()
def concrete_run(prog, params):
print("Starting concrete execution")
m = Manticore(prog, params)
# 'trace' will contain the executed instructions
m.context["trace"] = []
# None: The hook will be applied to all the instructions
@m.hook(None)
def record_trace(state):
pc = state.cpu.PC
# Store the instruction
with m.locked_context() as c:
c["trace"] += [pc]
m.run()
# Print number of instructions recorded
def main():
args = DeepManticore.parse_args()
consts.procs = args.num_workers
consts.timeout = args.timeout
consts.mprocessing = consts.mprocessing.single
try:
m = manticore.native.Manticore(args.binary)
except Exception as e:
L.critical("Cannot create Manticore instance on binary {}: {}".format(
args.binary, e))
return 1
log.set_verbosity(args.verbosity)
if args.take_over:
return main_takeover(m, args, 'DeepState_TakeOver')
elif args.klee:
return main_takeover(m, args, 'main')
else:
return main_unit_test(m, args)
$ python win.py
Solves collision challenge from pwnable.kr,
using symbolic execution to determine edge cases that
can trigger a hash collision.
"""
from manticore.native import Manticore
from manticore.core.smtlib import operators
# initialize Manticore object with symbolic input in
# argv[1]. We can eventually solve for this through
# state.input_symbol
m = Manticore("./col", ["+" * 20])
m.context["solution"] = None
m.context["argv1"] = None
@m.init
def init(initial_state):
""" define constraints for symbolic ARGV before execution """
# determine argv[1] from state.input_symbols by label name
argv1 = next(sym for sym in initial_state.input_symbols if sym.name == "ARGV1")
if argv1 is None:
raise Exception("ARGV was not made symbolic")
# apply constraint for only ASCII characters
for i in range(20):
initial_state.constrain(operators.AND(ord(" ") <= argv1[i], argv1[i] <= ord("}")))
#!/usr/bin/env python
# -*- coding: utf-8 --
from manticore.native import Manticore
m = Manticore("ais3_crackme", ["a" * 30])
buffer_addr = 0
num_bytes = 24
@m.hook(0x4005CD)
def hook(state):
print("fake 2 args EDI=2")
state.cpu.EDI = 0x2
@m.hook(0x4005F3)
def hook(state):
print("retreive buffer from rax")
global buffer_addr
# print state.cpu.read_int(state.cpu.RAX), 'yoo'