Инфраструктура Python. CTF

CTF: машинный код

todo Скриптование x64dbg? Immunity? IDAPython? Как бы прикрутить гейт между IPython и IDAPython, чтобы писать плагины и получать результаты их исполнения в нотебуке?

todo Frida? какой-нибудь аналог ProcMon?

todo pwn https://docs.pwntools.com/en/stable/about.html

Ассемблерирование — библиотека keystone.

качается инсталлер с сайта http://www.keystone-engine.org/

Пример вычисления факториала с https://godbolt.org/ clang 6.0.0

In [4]:
import keystone
import hexdump

code = '''
  push rbp
  mov rbp, rsp
  mov dword ptr [rbp - 4], edi
  mov dword ptr [rbp - 8], 1
  mov dword ptr [rbp - 12], 1
.LBB0_1: # =>This Inner Loop Header: Depth=1
  mov eax, dword ptr [rbp - 12]
  cmp eax, dword ptr [rbp - 4]
  jg .LBB0_4
  mov eax, dword ptr [rbp - 12]
  imul eax, dword ptr [rbp - 8]
  mov dword ptr [rbp - 8], eax
  mov eax, dword ptr [rbp - 12]
  add eax, 1
  mov dword ptr [rbp - 12], eax
  jmp .LBB0_1
.LBB0_4:
  mov eax, dword ptr [rbp - 8]
  pop rbp
  ret
.byte 0x6f,0x6d,0x67,0
'''

ks = keystone.Ks(keystone.KS_ARCH_X86, keystone.KS_MODE_64)
binary, count = ks.asm(code)
binary = ''.join(map(chr, binary))
hexdump.hexdump(binary)
00000000: 55 48 89 E5 89 7D FC C7  45 F8 01 00 00 00 C7 45  UH...}..E......E
00000010: F4 01 00 00 00 8B 45 F4  3B 45 FC 7F 15 8B 45 F4  ......E.;E....E.
00000020: 0F AF 45 F8 89 45 F8 8B  45 F4 83 C0 01 89 45 F4  ..E..E..E.....E.
00000030: EB E3 8B 45 F8 5D C3 6F  6D 67 00                 ...E.].omg.

И можно забыть о https://defuse.ca/online-x86-assembler.htm

Дизассемблерирование — библиотека capstone.

pip install capstone-windows
может потребоваться переместить capstone.dll
In [2]:
import capstone

# http://shell-storm.org/shellcode/files/shellcode-806.php
sploet = '\x31\xc0\x48\xbb\xd1\x9d\x96\x91\xd0\x8c\x97\xff\x48\xf7\xdb\x53\x54\x5f\x99\x52\x57\x54\x5e\xb0\x3b\x0f\x05'

pp = capstone.Cs(capstone.CS_ARCH_X86, capstone.CS_MODE_64)
for i in pp.disasm(sploet, 0):
    print '%02x:  %-21s %-6s %-25s' % (i.address, str(i.bytes).encode('hex'), i.mnemonic, i.op_str)
00:  31c0                  xor    eax, eax                 
02:  48bbd19d9691d08c97ff  movabs rbx, -0x68732f6e69622f   
0c:  48f7db                neg    rbx                      
0f:  53                    push   rbx                      
10:  54                    push   rsp                      
11:  5f                    pop    rdi                      
12:  99                    cdq                             
13:  52                    push   rdx                      
14:  57                    push   rdi                      
15:  54                    push   rsp                      
16:  5e                    pop    rsi                      
17:  b03b                  mov    al, 0x3b                 
19:  0f05                  syscall                          

Можно включить режим, в котором capstone сопровождает каждую инструкцию деталями ее разбора.

In [5]:
def detect_variable(instr):
    for op in instr.operands:
        if op.type == capstone.x86.X86_OP_MEM and op.mem.base == capstone.x86.X86_REG_RBP:
            return '; ' + {-4: 'n', -8: 'result', -12: 'i'}[op.mem.disp]
    return ''

pp = capstone.Cs(capstone.CS_ARCH_X86, capstone.CS_MODE_64)
pp.detail = True
for i in pp.disasm(binary, 0):
    print '%02x:  %-21s %-6s %-26s  %s' % (i.address, str(i.bytes).encode('hex'), i.mnemonic, i.op_str, detect_variable(i))
00:  55                    push   rbp                         
01:  4889e5                mov    rbp, rsp                    
04:  897dfc                mov    dword ptr [rbp - 4], edi    ; n
07:  c745f801000000        mov    dword ptr [rbp - 8], 1      ; result
0e:  c745f401000000        mov    dword ptr [rbp - 0xc], 1    ; i
15:  8b45f4                mov    eax, dword ptr [rbp - 0xc]  ; i
18:  3b45fc                cmp    eax, dword ptr [rbp - 4]    ; n
1b:  7f15                  jg     0x32                        
1d:  8b45f4                mov    eax, dword ptr [rbp - 0xc]  ; i
20:  0faf45f8              imul   eax, dword ptr [rbp - 8]    ; result
24:  8945f8                mov    dword ptr [rbp - 8], eax    ; result
27:  8b45f4                mov    eax, dword ptr [rbp - 0xc]  ; i
2a:  83c001                add    eax, 1                      
2d:  8945f4                mov    dword ptr [rbp - 0xc], eax  ; i
30:  ebe3                  jmp    0x15                        
32:  8b45f8                mov    eax, dword ptr [rbp - 8]    ; result
35:  5d                    pop    rbp                         
36:  c3                    ret                                
37:  6f                    outsd  dx, dword ptr [rsi]         
38:  6d                    insd   dword ptr [rdi], dx         

Эмуляция — unicorn

todo Установка

In [171]:
import unicorn
In [387]:
CODE = ''.join(map(chr, keystone.Ks(keystone.KS_ARCH_X86, keystone.KS_MODE_64).asm('add eax, eax')[0]))
print CODE.encode('hex')

mu = unicorn.Uc(unicorn.UC_ARCH_X86, unicorn.UC_MODE_64)
mu.mem_map(ADDRESS, 2 * 1024 * 1024, unicorn.UC_PROT_ALL)
mu.mem_write(ADDRESS, CODE)
mu.reg_write(unicorn.x86_const.UC_X86_REG_RAX, 21)
mu.emu_start(ADDRESS, ADDRESS + len(CODE))

print 'Calculations result =', mu.reg_read(unicorn.x86_const.UC_X86_REG_EAX)
01c0
Calculations result = 42
In [270]:
CODE = binary
function_argument_in_edi = 5


def show_regs(uc, regs):
    for reg in regs.split():
        value = uc.reg_read(unicorn.x86_const.__dict__['UC_X86_REG_' + reg.upper()])
        print '%s = %08X' % (reg, value),
    print

def hook_code(uc, address, size, user_data):
    print '-' * 40
    instr_bytes = str(uc.mem_read(address, size))
    print ';'.join(['%08x: %s %s %s' % (
        address,
        str(i.bytes).encode('hex').ljust(15),
        i.mnemonic,
        i.op_str) for i in pp.disasm(instr_bytes, 0)])
    show_regs(uc, 'eax rbp rsp')

def hook_mem_invalid(uc, access, address, size, value, user_data):
    if access == unicorn.UC_MEM_WRITE_UNMAPPED:
        print "INVALID WRITE at 0x%x %d byte(s) 0x%x" % (address, size, value)
    else:
        print 'INVALID READ  at 0x%x %d byte(s)' % (address, size)
    return False # do we want to continue emulation?
    
def hook_mem_access(uc, access, address, size, value, user_data):
    if access == unicorn.UC_MEM_WRITE:
        print 'WRITE at 0x%x %d byte(s) 0x%x' % (address, size, value)
    elif access == unicorn.UC_MEM_READ:
        print 'READ  at 0x%x %d byte(s)' % (address, size)
    stack = str(uc.mem_read(STACK - 32, 32))
    hexdump.hexdump(stack)


ADDRESS = 0x1000000
STACK = 0x1010000
OUTSIDE = 0x1010100

try:
    mu = unicorn.Uc(unicorn.UC_ARCH_X86, unicorn.UC_MODE_64)
    mu.mem_map(ADDRESS, 2 * 1024 * 1024, unicorn.UC_PROT_ALL)
    mu.mem_write(ADDRESS, CODE)       # code
    mu.mem_write(STACK, pack('I', OUTSIDE)) # return address
    mu.mem_write(OUTSIDE, '\xCC')           # return on int 3

    mu.reg_write(unicorn.x86_const.UC_X86_REG_EDI, function_argument_in_edi)
    mu.reg_write(unicorn.x86_const.UC_X86_REG_RSP, STACK)

    mu.hook_add(unicorn.UC_HOOK_CODE, hook_code)
    #mu.hook_add(unicorn.UC_HOOK_MEM_READ_UNMAPPED | unicorn.UC_HOOK_MEM_WRITE_UNMAPPED, hook_mem_invalid)
    #mu.hook_add(unicorn.UC_HOOK_MEM_WRITE | unicorn.UC_HOOK_MEM_READ, hook_mem_access)
    
    print 'Emulation start'
    mu.emu_start(ADDRESS, ADDRESS + len(CODE))
    print 'Emulation done'
except unicorn.UcError as e:
    print e
    print '=' * 40
    print 'Calculations result =', mu.reg_read(unicorn.x86_const.UC_X86_REG_EAX)
Emulation start
----------------------------------------
01000000: 55              push rbp
eax = 00000000 rbp = 00000000 rsp = 01010000
----------------------------------------
01000001: 4889e5          mov rbp, rsp
eax = 00000000 rbp = 00000000 rsp = 0100FFF8
----------------------------------------
01000004: 897dfc          mov dword ptr [rbp - 4], edi
eax = 00000000 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000007: c745f801000000  mov dword ptr [rbp - 8], 1
eax = 00000000 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100000e: c745f401000000  mov dword ptr [rbp - 0xc], 1
eax = 00000000 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000015: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000000 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000018: 3b45fc          cmp eax, dword ptr [rbp - 4]
eax = 00000001 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001b: 7f15            jg 0x17
eax = 00000001 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001d: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000001 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000020: 0faf45f8        imul eax, dword ptr [rbp - 8]
eax = 00000001 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000024: 8945f8          mov dword ptr [rbp - 8], eax
eax = 00000001 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000027: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000001 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002a: 83c001          add eax, 1
eax = 00000001 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002d: 8945f4          mov dword ptr [rbp - 0xc], eax
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000030: ebe3            jmp 0xffffffffffffffe5
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000015: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000018: 3b45fc          cmp eax, dword ptr [rbp - 4]
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001b: 7f15            jg 0x17
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001d: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000020: 0faf45f8        imul eax, dword ptr [rbp - 8]
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000024: 8945f8          mov dword ptr [rbp - 8], eax
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000027: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002a: 83c001          add eax, 1
eax = 00000002 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002d: 8945f4          mov dword ptr [rbp - 0xc], eax
eax = 00000003 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000030: ebe3            jmp 0xffffffffffffffe5
eax = 00000003 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000015: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000003 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000018: 3b45fc          cmp eax, dword ptr [rbp - 4]
eax = 00000003 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001b: 7f15            jg 0x17
eax = 00000003 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001d: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000003 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000020: 0faf45f8        imul eax, dword ptr [rbp - 8]
eax = 00000003 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000024: 8945f8          mov dword ptr [rbp - 8], eax
eax = 00000006 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000027: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000006 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002a: 83c001          add eax, 1
eax = 00000003 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002d: 8945f4          mov dword ptr [rbp - 0xc], eax
eax = 00000004 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000030: ebe3            jmp 0xffffffffffffffe5
eax = 00000004 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000015: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000004 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000018: 3b45fc          cmp eax, dword ptr [rbp - 4]
eax = 00000004 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001b: 7f15            jg 0x17
eax = 00000004 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001d: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000004 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000020: 0faf45f8        imul eax, dword ptr [rbp - 8]
eax = 00000004 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000024: 8945f8          mov dword ptr [rbp - 8], eax
eax = 00000018 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000027: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000018 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002a: 83c001          add eax, 1
eax = 00000004 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002d: 8945f4          mov dword ptr [rbp - 0xc], eax
eax = 00000005 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000030: ebe3            jmp 0xffffffffffffffe5
eax = 00000005 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000015: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000005 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000018: 3b45fc          cmp eax, dword ptr [rbp - 4]
eax = 00000005 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001b: 7f15            jg 0x17
eax = 00000005 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001d: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000005 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000020: 0faf45f8        imul eax, dword ptr [rbp - 8]
eax = 00000005 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000024: 8945f8          mov dword ptr [rbp - 8], eax
eax = 00000078 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000027: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000078 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002a: 83c001          add eax, 1
eax = 00000005 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100002d: 8945f4          mov dword ptr [rbp - 0xc], eax
eax = 00000006 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000030: ebe3            jmp 0xffffffffffffffe5
eax = 00000006 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000015: 8b45f4          mov eax, dword ptr [rbp - 0xc]
eax = 00000006 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000018: 3b45fc          cmp eax, dword ptr [rbp - 4]
eax = 00000006 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
0100001b: 7f15            jg 0x17
eax = 00000006 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000032: 8b45f8          mov eax, dword ptr [rbp - 8]
eax = 00000006 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000035: 5d              pop rbp
eax = 00000078 rbp = 0100FFF8 rsp = 0100FFF8
----------------------------------------
01000036: c3              ret 
eax = 00000078 rbp = 00000000 rsp = 01010000
----------------------------------------
01010100: cc              int3 
eax = 00000078 rbp = 00000000 rsp = 01010008
Unhandled CPU exception (UC_ERR_EXCEPTION)
========================================
Calculations result = 120

Помимо машинного кода реверсеры сталкиваются и с кодом виртуальных машин, например, виртуальной машины Python. Обычно он встречается в файлах формата *.pyc. Для просмотра кода ВМ функции можно использовать встроенную библиотеку dis, для преобразования *.pyc обратно (по возможности) в исходный код, библиотеки uncompyle* с разными суффиксами.

In [2]:
import dis
def fn(x):
    return x * 2
dis.dis(fn)
  3           0 LOAD_FAST                0 (x)
              3 LOAD_CONST               1 (2)
              6 BINARY_MULTIPLY     
              7 RETURN_VALUE        
In [282]:
import uncompyle6
with open('out.decompiled.txt', 'wb') as io:
    uncompyle6.decompile_file("C:\\Users\\User\\Anaconda2\\Lib\\site-packages\\moviepy\\audio\\fx\\volumex.pyc", io)
print file_get('out.decompiled.txt')
# uncompyle6 version 2.11.3
# Python bytecode 2.7 (62211)
# Decompiled from: Python 2.7.12 |Anaconda 2.5.0 (64-bit)| (default, Jun 29 2016, 11:07:13) [MSC v.1500 64 bit (AMD64)]
# Embedded file name: c:\users\user\appdata\local\temp\pip-install-cxbc6q\moviepy\moviepy\audio\fx\volumex.py
# Compiled at: 2018-04-18 17:57:33
from moviepy.decorators import audio_video_fx

@audio_video_fx
def volumex(clip, factor):
    """ Returns a clip with audio volume multiplied by the
    value `factor`. Can be applied to both audio and video clips.
    
    This effect is loaded as a clip method when you use moviepy.editor,
    so you can just write ``clip.volumex(2)``
    
    Examples
    ---------
    
    >>> newclip = volumex(clip, 2.0) # doubles audio volume
    >>> newclip = clip.fx( volumex, 0.5) # half audio, use with fx
    >>> newclip = clip.volumex(2) # only if you used "moviepy.editor"
    """
    return clip.fl(lambda gf, t: factor * gf(t), keep_duration=True)
In [272]:
import uncompyle2
io = BytesIO()
uncompyle2.uncompyle_file("C:\\Users\\User\\Anaconda2\\Lib\\site-packages\\moviepy\\audio\\fx\\volumex.pyc", io)
print io.getvalue()
<code object <module> at 000000002B1BC3B0, file "c:\users\user\appdata\local\temp\pip-install-cxbc6q\moviepy\moviepy\audio\fx\volumex.py", line 1>
100
100
108
109
90
101
100
132
131
90
100
<code object volumex at 000000002B1BC1B0, file "c:\users\user\appdata\local\temp\pip-install-cxbc6q\moviepy\moviepy\audio\fx\volumex.py", line 4>
124
106
135
135 [135, 136, 137] ('factor',) 0
102
100
134
100
116
131
<code object <lambda> at 000000002B1A3F30, file "c:\users\user\appdata\local\temp\pip-install-cxbc6q\moviepy\moviepy\audio\fx\volumex.py", line 19>
136
136 [135, 136, 137] ('factor',) 0
124
124
131
# Embedded file name: c:\users\user\appdata\local\temp\pip-install-cxbc6q\moviepy\moviepy\audio\fx\volumex.py
from moviepy.decorators import audio_video_fx

@audio_video_fx
def volumex(clip, factor):
    """ Returns a clip with audio volume multiplied by the
    value `factor`. Can be applied to both audio and video clips.
    
    This effect is loaded as a clip method when you use moviepy.editor,
    so you can just write ``clip.volumex(2)``
    
    Examples
    ---------
    
    >>> newclip = volumex(clip, 2.0) # doubles audio volume
    >>> newclip = clip.fx( volumex, 0.5) # half audio, use with fx
    >>> newclip = clip.volumex(2) # only if you used "moviepy.editor"
    """
    return clip.fl(lambda gf, t: factor * gf(t), keep_duration=True)

CTF: сеть

Библиотека dpkt умеет разбирать сетевой обмен и многие сетевые протоколы, по которому он проводится, например, самый распространенный Ethernet > IP > TCP.

pip install dpkt
In [6]:
import dpkt, itertools, socket, hexdump

mac_addr = lambda address: ':'.join('%02x' % ord(b) for b in address)
inet_to_str = lambda inet: socket.inet_ntoa(inet)

with open("picoctf2017_data__.pcap", 'rb') as fp:
    for ts, buf in itertools.islice(dpkt.pcap.Reader(fp), 29, 30):
        print '%.6f' % ts
        print
        hexdump.hexdump(buf)
        print
        eth = dpkt.ethernet.Ethernet(buf)
        print eth.__dict__
        print
        print '%s -> %s' % (mac_addr(eth.src), mac_addr(eth.dst))
        if type(eth.data) == dpkt.ip.IP:
            ip = eth.data
            if type(ip.data) == dpkt.tcp.TCP:
                tcp = ip.data
                print '%s:%d -> %s:%d' % (inet_to_str(ip.src), tcp.sport, inet_to_str(ip.dst), tcp.dport)
                print
                print tcp.data
                print
                print dpkt.http.Request(tcp.data).__dict__
1460061854.512104

00000000: 08 00 27 17 89 79 08 00  27 50 BB 09 08 00 45 00  ..'..y..'P....E.
00000010: 00 AD 1F E4 40 00 40 06  06 62 0A 00 00 05 0A 00  [email protected]@..b......
00000020: 00 01 E2 13 1F 90 FE FF  F7 F0 8D 23 17 15 80 18  ...........#....
00000030: 01 C9 86 F0 00 00 01 01  08 0A 00 0C E8 0E 00 0D  ................
00000040: 06 44 47 45 54 20 2F 72  6F 62 6F 74 73 2E 74 78  .DGET /robots.tx
00000050: 74 20 48 54 54 50 2F 31  2E 31 0D 0A 55 73 65 72  t HTTP/1.1..User
00000060: 2D 41 67 65 6E 74 3A 20  57 67 65 74 2F 31 2E 31  -Agent: Wget/1.1
00000070: 36 20 28 6C 69 6E 75 78  2D 67 6E 75 29 0D 0A 41  6 (linux-gnu)..A
00000080: 63 63 65 70 74 3A 20 2A  2F 2A 0D 0A 48 6F 73 74  ccept: */*..Host
00000090: 3A 20 31 30 2E 30 2E 30  2E 31 3A 38 30 38 30 0D  : 10.0.0.1:8080.
000000A0: 0A 43 6F 6E 6E 65 63 74  69 6F 6E 3A 20 4B 65 65  .Connection: Kee
000000B0: 70 2D 41 6C 69 76 65 0D  0A 0D 0A                 p-Alive....

{'ip': IP(len=173, id=8164, off=16384, p=6, sum=1634, src='\n\x00\x00\x05', dst='\n\x00\x00\x01', opts='', data=TCP(sport=57875, dport=8080, seq=4278188016L, ack=2367887125L, off=8, flags=24, win=457, sum=34544, opts='\x01\x01\x08\n\x00\x0c\xe8\x0e\x00\r\x06D', data='GET /robots.txt HTTP/1.1\r\nUser-Agent: Wget/1.16 (linux-gnu)\r\nAccept: */*\r\nHost: 10.0.0.1:8080\r\nConnection: Keep-Alive\r\n\r\n'))}

08:00:27:50:bb:09 -> 08:00:27:17:89:79
10.0.0.5:57875 -> 10.0.0.1:8080

GET /robots.txt HTTP/1.1
User-Agent: Wget/1.16 (linux-gnu)
Accept: */*
Host: 10.0.0.1:8080
Connection: Keep-Alive



{'body': '', 'uri': u'/robots.txt', 'headers': OrderedDict([(u'user-agent', u'Wget/1.16 (linux-gnu)'), (u'accept', u'*/*'), (u'host', u'10.0.0.1:8080'), (u'connection', u'Keep-Alive')]), 'version': u'1.1', 'data': '', 'method': u'GET'}

todo

scapy
    надо поставить pcapy и dnet
    https://github.com/CoreSecurity/pcapy/wiki/Compiling-Pcapy-on-Windows-Guide
    https://github.com/zlorb/scapy
    http://stackoverflow.com/questions/5447461/running-scapy-on-windows-with-python-2-7/27040800#27040800
dnet (1.12)
pcap (1.1)
pcapy (0.10.10)

socket
zio? pwn?

todo scapy хочет админские права, можно ли их дать из нотебука?

In [7]:
import scapy.all

def testTTL(pkt):
    if pkt.haslayer(IP):
        ip = pkt.getlayer(IP)
        print '[+] Pkt Received From: ' + ip.src + ' with TTL: ' + str(pkt.ttl)
scapy.all.sniff(prn=testTTL, store=0)
WARNING: No match between your pcap and dnet network interfaces found. You probably won't be able to send packets. Deactivating unneeded interfaces and restarting Scapy might help.
WARNING:scapy.loading:No match between your pcap and dnet network interfaces found. You probably won't be able to send packets. Deactivating unneeded interfaces and restarting Scapy might help.
WARNING: No route found for IPv6 destination :: (no default route?)
WARNING:scapy.runtime:No route found for IPv6 destination :: (no default route?)
---------------------------------------------------------------------------
TypeError                                 Traceback (most recent call last)
<ipython-input-7-ef358d5b6757> in <module>()
      5         ip = pkt.getlayer(IP)
      6         print '[+] Pkt Received From: ' + ip.src + ' with TTL: ' + str(pkt.ttl)
----> 7 scapy.all.sniff(prn=testTTL, store=0)

C:\Users\User\Anaconda2\lib\site-packages\scapy\arch\windows\__init__.pyc in sniff(count, store, offline, prn, lfilter, L2socket, timeout, *arg, **karg)
    494         if L2socket is None:
    495             L2socket = conf.L2listen
--> 496         s = L2socket(type=ETH_P_ALL, *arg, **karg)
    497     else:
    498         s = PcapReader(offline)

C:\Users\User\Anaconda2\lib\site-packages\scapy\arch\pcapdnet.pyc in __init__(self, iface, type, promisc, filter)
    103                     promisc = conf.sniff_promisc
    104                 self.promisc = promisc
--> 105                 self.ins = open_pcap(iface, 1600, self.promisc, 100)
    106                 try:
    107                     ioctl(self.ins.fileno(),BIOCIMMEDIATE,struct.pack("I",1))

C:\Users\User\Anaconda2\lib\site-packages\scapy\arch\windows\__init__.pyc in <lambda>(iface, *args, **kargs)
    232 
    233 _orig_open_pcap = pcapdnet.open_pcap
--> 234 pcapdnet.open_pcap = lambda iface,*args,**kargs: _orig_open_pcap(pcap_name(iface),*args,**kargs)
    235 
    236 def read_routes():

C:\Users\User\Anaconda2\lib\site-packages\scapy\arch\pcapdnet.pyc in <lambda>(*args, **kargs)
     51                 def __getattr__(self, attr):
     52                     return getattr(self.pcap, attr)
---> 53             open_pcap = lambda *args,**kargs: _PcapWrapper_pypcap(*args,**kargs)
     54         elif hasattr(pcap,"pcapObject"): # python-libpcap
     55             class _PcapWrapper_libpcap:

C:\Users\User\Anaconda2\lib\site-packages\scapy\arch\pcapdnet.pyc in __init__(self, device, snaplen, promisc, to_ms)
     48                     except TypeError:
     49                         # Older pypcap versions do not support the timeout_ms argument
---> 50                         self.pcap = pcap.pcap(device, snaplen, promisc, immediate=1)
     51                 def __getattr__(self, attr):
     52                     return getattr(self.pcap, attr)

pcap.pyx in pcap.pcap.__init__()

TypeError: exceptions must be strings, classes, or instances, not type

CTF: форматы

Простейшим способом доставать данные из бинарных форматов является встроенная библиотека struct. Форматной строкой описывается бинарный формат, функции pack и unpack преобразуют в/из него.

Шпаргалка по форматной строке (Little endian (Intel) — < перед символом, big endian (network) — >)

signedunsigned
`int8``b``B`
`int16``h``H`
`int32``i``I`
`int64``q``Q`
`float``f`
`double``d`
Строка длиной 42`42s`
In [9]:
import struct
bytes = struct.pack('Ih', 1, 1234)
print repr(bytes)
print struct.unpack('Ih', bytes)
'\x01\x00\x00\x00\xd2\x04'
(1, 1234)

Библиотека libmagic — стандартный метод опознавания типа файла в линуксах и python-magic Python-обертка её.

todo Установка на 64-битный питон

Скопировать

Скачать magic1.dll и K с https://github.com/pidydx/libmagicwin64

Если Python 32-битный:
скачать regex2.dll, zlib1.dll и magic1.dll с проекта gnuwin32
http://gnuwin32.sourceforge.net/packages/file.htm
http://gnuwin32.sourceforge.net/packages/regex.htm
http://gnuwin32.sourceforge.net/packages/zlib.htm

поместить их в PATH, например, переместив в C:\Users\User\Anaconda2\Lib\site-packages\
pip install python-magic
In [3]:
import os
dll_path = 'C:\\Users\\User\\Anaconda2\\Lib\\site-packages\\'
if dll_path not in os.environ['PATH'].split(';'):
    os.environ['PATH'] += ';' + dll_path;
In [4]:
import magic
m = magic.Magic(magic_file=os.path.join(dll_path, 'magic.mgc'))
In [5]:
print m.from_file("C:\\Users\\User\\Anaconda2\\Lib\\site-packages\\PySide\\QtCore4.dll")
PE32+ executable (DLL) (GUI) x86-64, for MS Windows
In [6]:
print m.from_file("files/feinman_audio.mp3")
Audio file with ID3 version 2.4.0, contains: MPEG ADTS, layer III, v1,  64 kbps, 44.1 kHz, Stereo
In [7]:
print m.from_file('files/wireshark.png')
PNG image data, 984 x 993, 8-bit/color RGB, non-interlaced

Утилита (и библиотека, но с API на отвали) binwalk анализирует файлы глубже, пытаясь отыскать знакомые сигнатуры (архивов, картинок итп) внутри.

Скачать https://github.com/ReFirmLabs/binwalk , распаковать
python setup.py install

Из командной строки (в папке %HOMEDIR%\Anaconda2\Scripts)
python binwalk filename -- искать сигнатуры
python binwalk -e filename -- извлечь все

Вывод аналогичный выводу binwalk filename можно получить кодом

In [4]:
import binwalk
for module in binwalk.scan('c:\\Temp\\jupyter_code\\201804\\asis ctf 2018\\plastic.binary', signature=True, quiet=True):
    print ("%s Results:" % module.name)
    for result in module.results:
        print "%s, offset 0x%08X  %s" % (result.file.name, result.offset, result.description)
Signature Results:
c:\Temp\jupyter_code\201804\asis ctf 2018\plastic.binary, offset 0x00000004  Zlib compressed data, best compression

todo Согласно документации, можно передавать вместо имени файла строку и string=True, но не работает.

Для описания и парсинга произвольных бинарных форматов существует инструмент kaitai и библиотека kaitaistruct. На YAML-подобном языке пишут *.ksy файл, описывающий структуру файла, затем его компилируют в исходник парсера в том числе на языке Python. В репозитории kaitai описано уже более 100 форматов. Можно создать свой в онлайн-IDE https://ide.kaitai.io/

http://kaitai.io/#download
pip install kaitaistruct
Для всех *.ksy файлов исполнить командную строку вида
"c:\Program Files (x86)\kaitai-struct-compiler\bin\kaitai-struct-compiler" --target python "c:\Program Files (x86)\kaitai-struct-compiler\formats\archive\rar.ksy"
Поместить сгенерированные *.py в доступное место
In [103]:
d = "c:\\Program Files (x86)\\kaitai-struct-compiler\\formats\\"
count = 0
for root, dirs, files in os.walk(d):
    ksy_files = [os.path.splitext(fn)[0] for fn in files if os.path.splitext(fn)[1] == '.ksy']
    if ksy_files:
        print '%23s' % root[len(d):], ':', ' '.join(ksy_files)
        count += len(ksy_files)
print
print count
                archive : cpio_old_le lzh rar zip
                    cad : monomakh_sapr_chg
                 common : bcd vlq_base128_be vlq_base128_le
               database : dbf tsm
             executable : dex dos_mz elf java_class mach_o microsoft_pe python_pyc_27 swf
             filesystem : apm_partition_table cramfs ext2 gpt_partition_table iso9660 luks lvm2 mbr_partition_table vdi vfat vmware_vmdk
               firmware : andes_firmware ines
                   font : ttf
                   game : doom_wad dune_2_pak fallout2_dat fallout_dat ftl_dat gran_turismo_vol heaps_pak heroes_of_might_and_magic_agg heroes_of_might_and_magic_bmp quake_mdl quake_pak renderware_binary_stream saints_row_2_vpp_pc warcraft_2_pud
             geospatial : shapefile_index shapefile_main
               hardware : edid
                  image : bmp dicom exif exif_be exif_le gif icc_4 ico jpeg pcx png psx_tim tga wmf xwd
                    log : glibc_utmp windows_evt_log
           machine_code : code_6502
                  media : avi blender_blend creative_voice_file genmidi_op2 id3v1_1 id3v2_3 id3v2_4 magicavoxel_vox ogg quicktime_mov standard_midi_file stl wav
  media\tracker_modules : s3m
                network : dns_packet ethernet_frame hccap hccapx icmp_packet ipv4_packet ipv6_packet microsoft_network_monitor_v2 packet_ppi pcap tcp_segment tls_client_hello udp_datagram
      scientific\nt_mdt : nt_mdt nt_mdt_pal
scientific\spectroscopy : avantes_roh60 specpr
          serialization : bson google_protobuf microsoft_cfb msgpack ruby_marshal
     serialization\asn1 : asn1_der
                windows : regf windows_lnk_file windows_minidump windows_resource_file windows_shell_items windows_systemtime

110
In [24]:
import kaitaistruct, imp

Rar = imp.load_source('rar', 'c:/Temp/jupyter_code/201804/kaitaiformats/rar.py').Rar
g = Rar.from_file("do_not_attach/FUNKAN.RAR")
g.__dict__
Out[24]:
{'_io': <kaitaistruct.KaitaiStream at 0x635ab38>,
 '_parent': None,
 '_root': <rar.Rar at 0x642d320>,
 'blocks': [<rar.Block at 0x627d048>,
  <rar.Block at 0x6436b00>,
  <rar.Block at 0x6436c18>,
  <rar.Block at 0x6436cf8>,
  <rar.Block at 0x6436dd8>],
 'magic': <rar.MagicSignature at 0x6436a58>}
In [25]:
for block in g.blocks:
    if block.block_type == Rar.BlockTypes.file_header:
        print block.body.low_unp_size, block.body.file_name
172544 funkan_faq.doc
449536 funkan_solutions1-20.doc
249856 funkan_solutions21-40.doc
161280 funkan_solutions41-55.doc

Другим популярным средством описания форматов являются темплейты платного hex-редактора 010 Editor. В них формат описывается си-подобным языком, в котором описания структур перемешаны с условиями и циклами (описание, например, здесь https://habrahabr.ru/post/213639/). В открытом для скачивания репозитории описано более 100 форматов. Для их парсинга и использования в Python может служить библиотека pfp.

pip install pfp
In [54]:
import requests, urllib
from lxml import etree
from ultra import file_get, file_put
In [51]:
baseurl = 'http://www.sweetscape.com/010editor/repository/templates/'
page = requests.get(baseurl).content
In [99]:
bt_files = []
for tr in etree.HTML(page).xpath('//table[@class="gradient2"]/tr/td'):
    categories = tr.xpath('i')
    links = tr.xpath('a')
    if categories:
        cat = 'Category: ' + categories[0].text
        print
        print cat
        print '-' * len(cat)
    if links:
        href = links[0].attrib['href']
        if href.startswith('../files/'):
            print links[0].text,
            url = urllib.basejoin(baseurl, href)
            bt_files.append(url)
Category: Archive
-----------------
CAB.bt ../files/CAB.bt
GZip.bt ../files/GZip.bt
LZ4.bt ../files/LZ4.bt
RAR.bt ../files/RAR.bt
SeqBox.bt ../files/SeqBox.bt
SquashFS.bt ../files/SquashFS.bt
ZIP.bt ../files/ZIP.bt
ZIPAdv.bt ../files/ZIPAdv.bt

Category: Audio
---------------
CDA.bt ../files/CDA.bt
MIDI.bt ../files/MIDI.bt
MP3.bt ../files/MP3.bt
OGG.bt ../files/OGG.bt
SF2.bt ../files/SF2.bt
WAV.bt ../files/WAV.bt
WAVAdv.bt ../files/WAVAdv.bt

Category: CAD
-------------
OrCAD_LIB.bt ../files/OrCAD_LIB.bt
OrCAD_SCH.bt ../files/OrCAD_SCH.bt
STL.bt ../files/STL.bt

Category: Database
------------------
DBF.bt ../files/DBF.bt
MongoDBWireProtocol.bt ../files/MongoDBWireProtocol.bt

Category: Document
------------------
MOBI.bt ../files/MOBI.bt
PDF.bt ../files/PDF.bt

Category: Drives
----------------
Drive.bt ../files/Drive.bt
ElTorito.bt ../files/ElTorito.bt
ISO.bt ../files/ISO.bt
LUKS.bt ../files/LUKS.bt
ROMFS.bt ../files/ROMFS.bt
SinclairMicrodrive.bt ../files/SinclairMicrodrive.bt
SytosPlus.bt ../files/SytosPlus.bt
VHD.bt ../files/VHD.bt

Category: Electronics
---------------------
EDID.bt ../files/EDID.bt
EVSB.bt ../files/EVSB.bt
EZTap_EZVIEW2.bt ../files/EZTap_EZVIEW2.bt
Goclever.bt ../files/Goclever.bt
Mifare1k.bt ../files/Mifare1k.bt
Mifare4k.bt ../files/Mifare4k.bt
MifareUltralight.bt ../files/MifareUltralight.bt
OscarItem.bt ../files/OscarItem.bt
Picolog_PLW.bt ../files/Picolog_PLW.bt
SRec.bt ../files/SRec.bt

Category: Executable
--------------------
ELF.bt ../files/ELF.bt
EXE.bt ../files/EXE.bt
MachO.bt ../files/MachO.bt

Category: Font
--------------
EOT.bt ../files/EOT.bt
FNT.bt ../files/FNT.bt
OpenType.bt ../files/OpenType.bt
TTF.bt ../files/TTF.bt

Category: Game
--------------
GGPK.bt ../files/GGPK.bt
NDS.bt ../files/NDS.bt
Quake3Arena_BSP.bt ../files/Quake3Arena_BSP.bt
Quake3Arena_MD3.bt ../files/Quake3Arena_MD3.bt

Category: GIS
-------------
SHP.bt ../files/SHP.bt
SHX.bt ../files/SHX.bt

Category: Image
---------------
BMP.bt ../files/BMP.bt
DDS.bt ../files/DDS.bt
EMF.bt ../files/EMF.bt
GIF.bt ../files/GIF.bt
ICO.bt ../files/ICO.bt
JPG.bt ../files/JPG.bt
PAL.bt ../files/PAL.bt
PCX.bt ../files/PCX.bt
PNG.bt ../files/PNG.bt
TGA.bt ../files/TGA.bt
TIF.bt ../files/TIF.bt
WMF.bt ../files/WMF.bt

Category: Inspector
-------------------
InspectorDates.bt ../files/InspectorDates.bt
InspectorWithMP4DateTime.bt ../files/InspectorWithMP4DateTime.bt

Category: Internet
------------------
SWF.bt ../files/SWF.bt
Torrent.bt ../files/Torrent.bt

Category: Misc
--------------
FTS.bt ../files/FTS.bt
KryoFlux.bt ../files/KryoFlux.bt
RDB.bt ../files/RDB.bt
RIFF.bt ../files/RIFF.bt
SCP.bt ../files/SCP.bt
Tacx.bt ../files/Tacx.bt

Category: Network
-----------------
NetflowVersion5.bt ../files/NetflowVersion5.bt
PCAP.bt ../files/PCAP.bt
PCAPNG.bt ../files/PCAPNG.bt
SSP.bt ../files/SSP.bt
TNEF.bt ../files/TNEF.bt

Category: Operating System
--------------------------
AndroidManifest.bt ../files/AndroidManifest.bt
AndroidResource.bt ../files/AndroidResource.bt
AndroidTrace.bt ../files/AndroidTrace.bt
BPlist.bt ../files/BPlist.bt
Cryptfs.bt ../files/Cryptfs.bt
DEX.bt ../files/DEX.bt
DMP.bt ../files/DMP.bt
HFSJournal.bt ../files/HFSJournal.bt
LNK.bt ../files/LNK.bt
PSF.bt ../files/PSF.bt
RegistryHive.bt ../files/RegistryHive.bt
RegistryPolicyFile.bt ../files/RegistryPolicyFile.bt
ThumbCache.bt ../files/ThumbCache.bt
UTMP.bt ../files/UTMP.bt

Category: Programming
---------------------
BSON.bt ../files/BSON.bt
CAP.bt ../files/CAP.bt
CLASS.bt ../files/CLASS.bt
CLASSAdv.bt ../files/CLASSAdv.bt
Luac.bt ../files/Luac.bt
LuaJIT.bt ../files/LuaJIT.bt
OPCache.bt ../files/OPCache.bt
PYC.bt ../files/PYC.bt
RES.bt ../files/RES.bt

Category: Software
------------------
010Theme.bt ../files/010Theme.bt
CRX.bt ../files/CRX.bt
HiewCMarkers.bt ../files/HiewCMarkers.bt
TOC.bt ../files/TOC.bt
WinhexPos.bt ../files/WinhexPos.bt

Category: Video
---------------
AVI.bt ../files/AVI.bt
BaseMedia.bt ../files/BaseMedia.bt
FLV.bt ../files/FLV.bt
MP4.bt ../files/MP4.bt
MXF.bt ../files/MXF.bt
RM.bt ../files/RM.bt
In [102]:
len(bt_files)
Out[102]:
114
In [108]:
d = 'c:\\Temp\\jupyter_code\\201804\\010formats\\'
for url in bt_files:
    f = requests.get(url).content
    file_put(os.path.join(d, url.split('/')[-1]), f)
In [126]:
import pfp
from pfp.fields import PYVAL

dom = pfp.parse(
    data_file="do_not_attach/FUNKAN.RAR",
    template_file='c:\\Temp\\jupyter_code\\201804\\010formats\\RAR.bt'
)
RAR signature found at 0x00000000.
It is a non-locked regular one-part RAR archive.
Version to unpack: 2.0
Files: 4, Dirs: 0, Comments: 0, SubBlocks: 0, Unpacked Size: 1033216
UNICODE Names: 0
Done. 6 blocks processed.
In [130]:
for block in dom.block:
    print PYVAL(block.file.UnpackedSize), block.file.FileName.raw_data
172544 funkan_faq.doc
449536 funkan_solutions1-20.doc
249856 funkan_solutions21-40.doc
161280 funkan_solutions41-55.doc
In [397]:
print dom._pfp__show(include_offset=True)[:5000]
0000 struct {
    0000 _skipped   = Char[0] ('')
    0000 Marker     = 0000 struct {
        0000 HEAD_CRC   = UShort(24914 [6152])
        0002 HeadType   = Enum<Char>(114 [72])(MARKER)
        0003 HEAD_FLAGS = 0003 struct {
            0003 _reserved  = UShort(6689 [1a21]):14
            0005 OLD_VERSION_IGNORE = UShort(0 [0000]):1
            0005 ADD_SIZE_PRESENT = UShort(0 [0000]):1
        }
        0005 HeaderSize = UShort(7 [0007])
    }
    0007 ArcHeader  = 0007 struct {
        0007 HEAD_CRC   = UShort(37071 [90cf])
        0009 HeadType   = Enum<Char>(115 [73])(ARCHIVE)
        000a HEAD_FLAGS = 000a struct {
            000a ARCHIVE_VOLUME = UChar(0 [00]):1
            000b ARCHIVE_COMMENT_PRESENT = UChar(0 [00]):1
            000b ARCHIVE_LOCKED = UChar(0 [00]):1
            000b ARCHIVE_SOLID = UChar(0 [00]):1
            000b NEW_VOLUME_NAMING = UChar(0 [00]):1
            000b AV_PRESENT = UChar(0 [00]):1
            000b RECOVERY_PRESENT = UChar(0 [00]):1
            000b BLOCK_HEADERS_ENCRYPTED = UChar(0 [00]):1
            000b IS_FIRST_VOLUME = UChar(0 [00]):1
            000c _reserved  = UChar(0 [00]):5
            000c OLD_VERSION_IGNORE = UChar(0 [00]):1
            000c ADD_SIZE_PRESENT = UChar(0 [00]):1
        }
        000c HeaderSize = UShort(13 [000d])
        000e _reserved1 = UShort(0 [0000])
        0010 _reserved2 = UInt(0 [00000000])
    }
    0014 block      = struct[4]
        0014 block[0] = 0014 struct {
                0014 HEAD_CRC   = UShort(26194 [6652])
                0016 HeadType   = Enum<Char>(116 [74])(FILE_OR_DIR)
                0017 HEAD_FLAGS = 0017 struct {
                    0017 from_PREV_VOLUME = UChar(0 [00]):1
                    0018 to_NEXT_VOLUME = UChar(0 [00]):1
                    0018 PASSWORD_ENCRYPTED = UChar(0 [00]):1
                    0018 FILE_COMMENT_PRESENT = UChar(0 [00]):1
                    0018 SOLID      = UChar(0 [00]):1
                    0018 DICTIONARY = Enum<Char>(4 [04]):3(_1024K)
                    0018 HIGH_SIZE  = UChar(0 [00]):1
                    0019 has_UNICODE_FILENAME = UChar(0 [00]):1
                    0019 ENCRYPTION_SALT = UChar(0 [00]):1
                    0019 IS_OLD_FILE_VERSION = UChar(0 [00]):1
                    0019 EXTENDED_TIME_INFO = UChar(0 [00]):1
                    0019 _reserved  = UChar(0 [00]):1
                    0019 OLD_VERSION_IGNORE = UChar(0 [00]):1
                    0019 ADD_SIZE_PRESENT = UChar(1 [01]):1
                }
                0019 HeaderSize = UShort(46 [002e])
                001b RawDataSize = UInt(40657 [00009ed1])
                001f file       = 001f struct {
                    001f UnpackedSize = UInt(172544 [0002a200])
                    0023 Host_OS    = Enum<UChar>(2 [02])(_Win32)
                    0024 FileCRC32  = UInt(3164328312L [bc9bd178])
                    0028 FileTime   = 0028 struct {
                        0028 second     = UShort(10 [000a]):5
                        002a minute     = UShort(18 [0012]):6
                        002a hour       = UShort(18 [0012]):5
                    }
                    002a FileDate   = 002a struct {
                        002a day        = UShort(27 [001b]):5
                        002c month      = UShort(12 [000c]):4
                        002c year       = UShort(18 [0012]):7
                    }
                    002c VersionToUnpack = UChar(20 [14])
                    002d Method     = Enum<Char>(51 [33])(Normal)
                    002e NameSize   = UShort(14 [000e])
                    0030 Attributes = 0030 struct {
                        0030 READONLY   = UInt(0 [00000000]):1
                        0034 HIDDEN     = UInt(0 [00000000]):1
                        0034 SYSTEM     = UInt(0 [00000000]):1
                        0034 VOLUME     = UInt(0 [00000000]):1
                        0034 DIRECTORY  = UInt(0 [00000000]):1
                        0034 ARCHIVE    = UInt(1 [00000001]):1
                        0034 DEVICE     = UInt(0 [00000000]):1
                        0034 NORMAL     = UInt(0 [00000000]):1
                        0034 TEMPORARY  = UInt(0 [00000000]):1
                        0034 SPARSE_FILE = UInt(0 [00000000]):1
                        0034 REPARSE_POINT = UInt(0 [00000000]):1
                        0034 COMPRESSED = UInt(0 [00000000]):1
                        0034 OFFLINE    = UInt(0 [00000000]):1
                        0034 NOT_CONTENT_INDEXED = UInt(0 [00000000]):1
                        0034 ENCRYPTED  = UInt(0 [00000000]):1
                        0034 _res2      = UInt(0 [00000000]):17
                    }
                    0034 FileName   = Char[14] ('funkan_faq.doc')
                }
                0042 _raw       = UChar[40657] ('\x1ebYQ\x0c\x8c\xcd\x9c\x16#\x01\xeb \xd4\x02&2\x11\xd1\x8c')
            }
        9f13 block[1] = 9f13 struct {
                9f13 HEAD_CRC   = UShort(16753 [4171])
                9f15 HeadType   = Enum<Char>(1

Если вас заинтересовала эта тема, посмотрите еще

https://github.com/construct/construct

http://www.ogf.org/dfdl

https://www.x-ways.net/winhex/templates/

https://www.synalysis.net/formats.xml

todo

radare2? nrbfdump?

pefile
pyelftools - Parsing and analyzing ELF files and DWARF debugging information.
elffile?
или https://github.com/sashs/filebytes pip install filebytes: ELF, PE, MachO, OAT (Android) -- нет ресурсов!

olefile (formerly OleFileIO_PL) is a Python package to parse, read and write Microsoft OLE2 files (also called Structured Storage, Compound File Binary Format or Compound Document File Format), such as Microsoft Office 97-2003 documents, vbaProject.bin in MS Office 2007+ files, Image Composer and FlashPix files, Outlook MSG files, StickyNotes, several Microscopy file formats, McAfee antivirus quarantine files, etc.
In [6]:
from filebytes.pe import *
In [39]:
pe_file = PE('do_not_attach/ab.exe')
print pe_file.imageDosHeader.header.e_magic
print pe_file.imageNtHeaders.header.Signature
print [item.name for item in pe_file.sections]
MZ
PE
[u'.text', u'.rdata', u'.data', u'.rsrc']
In [62]:
for imp in pe_file.dataDirectory[ImageDirectoryEntry.IMPORT]:
    print imp.dllName
    print ' '.join(sorted([rec.importByName.name if rec.importByName else '(by ordinal)' for rec in imp.importNameTable]))
    print
MSVCRT.dll
_XcptFilter __dllonexit __getmainargs __mb_cur_max __p___initenv __p__commode __p__environ __p__fmode __p__wenviron __set_app_type __setusermatherr _adjust_fdiv _close _controlfp _errno _except_handler3 _exit _ftol _getpid _initterm _iob _isctype _onexit _pctype _strdup _strnicmp atoi calloc exit fclose fflush fopen fprintf free malloc modf perror printf qsort realloc signal strchr strerror strncmp strncpy strrchr strspn strstr wcscpy wcslen wcsncmp

KERNEL32.dll
CancelIo CloseHandle CreateEventA CreateFileW DeleteCriticalSection DeviceIoControl EnterCriticalSection FileTimeToSystemTime FormatMessageA FreeEnvironmentStringsW GetCommandLineW GetEnvironmentStringsW GetExitCodeProcess GetFileInformationByHandle GetFileType GetLastError GetOverlappedResult GetProcAddress GetSystemTimeAsFileTime GetTimeZoneInformation GetVersionExA GlobalFree InitializeCriticalSection LeaveCriticalSection LoadLibraryA LocalFree PeekNamedPipe ReadFile ReleaseMutex SetEvent SetFilePointer SetHandleInformation SetLastError SetStdHandle Sleep SystemTimeToFileTime SystemTimeToTzSpecificLocalTime TerminateProcess TlsAlloc TlsFree WaitForSingleObject WriteFile

ADVAPI32.dll
AllocateAndInitializeSid FreeSid GetEffectiveRightsFromAclW GetNamedSecurityInfoA GetNamedSecurityInfoW GetSecurityInfo

WSOCK32.dll
(by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal) (by ordinal)

WS2_32.dll
WSARecv WSASend

SHELL32.dll
CommandLineToArgvW

CTF: криптография

Классические шифры реализованы в библиотеке pycipher. В их числе атбаш, Энигма, Playfair, Видженер.

pip install pycipher
In [392]:
import pycipher
enc = pycipher.Caesar().encipher('hello')
dec = pycipher.Caesar().decipher(enc)
print enc
print dec
URYYB
HELLO

Некоторые алгоритмы, полезные при решении задач CTF, включены в sympy, детально описываемый в разделе CAS.

In [131]:
import sympy.crypto.crypto
print sympy.crypto.crypto.AZ('Hello, world!')
print sympy.crypto.encode_morse('HELLO WORLD')
print sympy.crypto.decode_morse('....|.|.-..|.-..|---||.--|---|.-.|.-..|-..')
HELLOWORLD
....|.|.-..|.-..|---||.--|---|.-.|.-..|-..
HELLO WORLD

В Python встроены библиотеки hashlib, позволяющая вычислять некоторые популярные (устаревшие!) хэши, такие как MD5 или SHA1, и алгоритм в одноименной библиотеке hmac проверки целостности сообщения на основе общего секрета K и хэш-функции H (по умолчанию MD5).

ipad = the byte 0x36 repeated B times
opad = the byte 0x5C repeated B times.
HMAC(text) = H(K XOR opad, H(K XOR ipad, text))
In [4]:
import hashlib
def md5_file(filename):
    crc = hashlib.md5()
    with open(filename, 'rb') as fp:
        while True:
            buff = fp.read(4096)
            if len(buff) == 0:
                break
            crc.update(buff)
    return crc.hexdigest()

md5_file('files/wireshark.png')
Out[4]:
'7c82f8e0531df7aa13280f8f1d7f38d2'
In [55]:
hashlib.algorithms
Out[55]:
('md5', 'sha1', 'sha224', 'sha256', 'sha384', 'sha512')

Некриптографический, но популярный хэш CRC32 можно взять во встроенной библиотеке binascii.

In [422]:
import binascii
from numpy import uint32
In [423]:
'%08x' % uint32(binascii.crc32('a'))
Out[423]:
'e8b7be43'

todo HashCalc от SlavaSoft поддерживает: MD5, MD4, SHA1, SHA256, SHA386, SHA512, RIPEMD160, PANAMA, TIGER, MD2, ADLER32, CRC32, eDonkey/eMule

In [76]:
import hmac
K = 'shared secret'
M = 'message'
hmac.new(K, M).hexdigest()
Out[76]:
'570752326bf3279200928538957f3dcf'
In [79]:
from ultra import md5, xorstr
Ko = xorstr(K.ljust(64, '\0'), '\x5C')
Ki = xorstr(K.ljust(64, '\0'), '\x36')
md5(Ko + md5(Ki + M).decode('hex'))
Out[79]:
'570752326bf3279200928538957f3dcf'

Популярные более современные криптопримитивы, такие как AES и RSA, реализованы в библиотеке pycrypto.

pip install pycrypto
In [31]:
from Crypto.Cipher import DES
key = 'E0E0E0E0F1F1F1F1'.decode('hex')
text = 'Encrypt me twice'
print repr(DES.new(key).encrypt(text))
print DES.new(key).encrypt(DES.new(key).encrypt(text))
'\x08\[email protected][\xd8\nO\xed\x9f\x9e\xba\xaeD[\x0f'
Encrypt me twice

Не используйте слабые ключи (и вообще DES).

In [28]:
from Crypto.Cipher import AES
from Crypto.Random import get_random_bytes

BS = 16
pad = lambda s: s + (BS - len(s) % BS) * chr(BS - len(s) % BS)
unpad = lambda s: s[0:-ord(s[-1])]

iv = get_random_bytes(16)
key = get_random_bytes(16)
enc = AES.new(key, AES.MODE_CBC, iv).encrypt(pad('Hello, AES'))
print repr(enc)
dec = AES.new(key, AES.MODE_CBC, iv).decrypt(enc)
print unpad(dec)
']\x95q\xd5^Bj\x97\xa1\xa4N\xda\x93\xa3+v'
Hello, AES
In [146]:
from Crypto.PublicKey import RSA
from Crypto.Util.number import long_to_bytes, bytes_to_long

keyA = RSA.generate(2048)
pkA = keyA.publickey()

keyB = RSA.generate(2048)
pkB = keyB.publickey()

print pkA.exportKey()
print

# Алиса шифрует публичным ключом Боба, подписывает своим секретным
M = 'secret'
enc = pkB.encrypt(M, None)[0]
enc_sign = long_to_bytes(keyA.sign(M, None)[0])
print 'Encrypted:', repr(enc)
print
print 'Signature:', repr(enc_sign)
print

# Боб расшифровывает своим приватным ключем, проверяет подпись публичным ключом Алисы
dec = keyB.decrypt(enc)
print 'Decrypted:', dec
print 'Is signature correct?:', pkA.verify(dec, (bytes_to_long(enc_sign),))
 -----BEGIN PUBLIC KEY-----
MIIBIjANBgkqhkiG9w0BAQEFAAOCAQ8AMIIBCgKCAQEAuUkRgi+kEpxZnIuTEa/I
vIQU9f/X8sjIXPbsY3EnDVkm7/okKdgujCwiGq4hDfAhT/2+40g581AkZ0SbfvNC
bxqT8Zy7kvzuyFcDk/WuaVcAP7v1WwhTYE7MqXIP2ForlVR8EyC63o/RIx66cuyq
thcyW/v5u5uM4+J32szRvb639aOjQSGRyiu89Oan6Bkx/ZmBUKkz1S9lBO8nYZRg
OaxcdZNhZbbsAP7UHPIavKmuipNluezhwoSioU3mQJn2ITj+xVWREVVtiYtVPnJT
eXkOixfbzz1a7UPngb7lShW9KhT2WaZ2YObyF6CJ6sUjX/bqW8WlH9gzWhJ0YEsG
cwIDAQAB
-----END PUBLIC KEY-----

Encrypted: '\x8b\xf6\x8fW\xa2\x8dx\xe3\x1b\x16\xc5\xeeIG\x8e\x97\xa2C\x08\x87\xc1\xe0\xc2\x86b\x82N\x9eZie\xf8\x8e.\xb1T\xa6\xb9gp\xee\xdbN\xcf\x0b%\x0b\x8d\xa3\x12LI\xb0\x96\xcf\xfa:[\xdb\xb8\x10\xd8\xfc\xd7Q\x06\xf0lcBhr\x9a\x02\xafX\xad\xc9&*\x9c\xd8\xaa\xa9M\xac\[email protected]\xf5\xa7\xa2\xceo\xc3\xbf\x0e\xf8\xaaQ\x16\x91\n\xf8`\x1a\xeb\x17\x8b\xd6\x9cK\x0ea\x93\xee\xdat`\xd7\xdb!A\r\x04Z\xf0k\x95^\x8cy\x9f]9\x94s\xa1#\x91\xc0\xa1P\xe1wM\x9f\x9cN\xef\x10\x95\xb1\xaeLu\xa1\x81\x8e\xc1}L\x00\xcd\xbe\x18\x9c\xb7B\t\x96t\xb5\xa3\xfe\xa6\x00\x84\xdd\xc1F*\x88\xc0\xfc[\xcez\xe1\xa5ok\x8b\x9d\xd7\xc0\xb6\xcb\xeal\xfc`\x95\x9al\x1a\xba\xb4b\x99\x89\xd8\x96\x95\x98\xc0#\xe4\x7fo1\xa4\xa5\xc4\xafFN\xe3\xcd\xd1\x03\xc1~\xb1\xeaFS\xbd\xfbQ\x9c4\[email protected]\x8e>)7\xb7\x16ubyX\xa7\x85'

Signature: "\x99\xe5G\x98\x91\x91\x1c\xf0\x96\xe9\xe5\x9f\x14Q\x92\xf7~\xe9\x82\x07\xd8\xc9\x1c\x8b\x89t\x9e+\xe1/L#\x97\x1e[?Sz\xb73\xe5/\\\x9e\xa6\xa9v\x97\xc2\xf8m\xddjEd\xa9\nJ\\\xf0\x0fg\xc9\xe3\x05\xca)l\xf4)=j\xbd\xd3\x91\x8dW\xf5\x1e\x0b\xc6\x10\x8bO\x1f\xba\xa8>\xd9\xf9\x92\xb23K\x04u\x8d\x91\xd2\x9f\xae\x02G\xe0\x04 \x0f\\Z\x9cf\xcf\x07\x96\x81>\x07:\xf5?\xdf\xca\x9d\xea\x9c\x0eP\xd5\xa4i\xc4T\xbf\x08\xce\xec/\x95K\xe9\x0c\xb1$\x9f\xf6\xfc\x80N\x81\xf798\xc2\xa6+'E\xc7\xb1'\x0e\\\xa7\xa2\xa3\xa2\x93%\xb6\xc3\x13\x98,\xb6\xe4\xd0W\xc3\xf4\x0b\xf0\[email protected]\xb62\xba\[email protected]\xa1\xd8\xaf\xac,o\xe3gr\xe3\xef\xeb\xda\x16.\xe3g^\xa8\x1b\x9a\xc1`\x90\x0e\x85d\xaf\xee}@\xe0\x1d\x15o\xfe\x8ai\xc0\xb2\xcf\x88\x1f\x93\xcb!\xaf\xbaENq\x91\x8b}\x13e\x02*\x90\xc2\xe0\xfd\xd0\xf6\x80z\xda"

Decrypted: secret
Is signature correct?: True

Если криптография нужна в вашем приложении и вы не знаете точно, какие криптопримитивы использовать, возьмите библиотеку pynacl, обертку над libsodium, в которой выбор криптопримитивов сделан специалистами.

Подробнее http://latacora.singles/2018/04/03/cryptographic-right-answers.html (перевод https://habr.com/company/globalsign/blog/353576/).

pip install pynacl

Пример асимметричной криптографии. Алиса и Боб генерируют секретные ключи, обмениваются публичными, Боб шифрует сообщение своим приватным ключем и публичным Алисы. Сообщение может прочитать только Алиса и она может быть уверена, что его не мог сгенерить никто, кроме Боба.

In [2]:
import nacl.utils
from nacl.public import PrivateKey, Box

skbob = PrivateKey.generate()
pkbob = skbob.public_key

skalice = PrivateKey.generate()
pkalice = skalice.public_key

bob_box = Box(skbob, pkalice)
message = 'Kill all humans'
print len(message), message

# Encrypt our message, it will be exactly 40 bytes longer than the original message as it stores
# authentication information and the nonce alongside it.
# This is a nonce, it *MUST* only be used once, but it is not considered secret
# and can be transmitted or stored alongside the ciphertext. A good source of nonces are just sequences of 24 random bytes.
encrypted = bob_box.encrypt(message, nacl.utils.random(Box.NONCE_SIZE))
print len(encrypted), encrypted.encode('hex')

alice_box = Box(skalice, pkbob)
plaintext = alice_box.decrypt(encrypted)
print plaintext
15 Kill all humans
55 f8054c7a29c4bae69ce1e1c5a17caf0040bc5e4afb6499ec6fc5be7e858aead879a348f59f053de3fb878417b5d6e7f945ed1e3a8b1a0c
Kill all humans

todo Диффи-Хеллман, чтение HTTPS-дампа, зная ключ; скачать и проверить сертификат сайта; проверить подпись файла

CTF: SMT-сольверы

z3:
Visual Studio 2015 x64 Native Tools Command Prompt
python scripts/mk_make.py --x64
cd build
nmake
copy all /build/ to Lib/site-packages/z3/
__init__.py: from z3 import *

Существует ряд задач, в которых нужно найти какой-нибудь набор переменных, удовлетворяющий набору некоторых логических, математических или битовых условий. Для их решения созданы специальные программы, SMT-сольверы, один из которых z3 от Microsoft наиболее популярен и имеет одноименный Python-враппер.

Использование z3 заключается в объявлении переменных с указанием их типа, добавлении условий на эти переменные в сольвер (используется смесь операторов Python и собственных функций z3), вызове solver.check(), который вернет z3.sat, если z3 сумел найти решение. Переменные решения можно получить, используя вызов solver.model().

In [13]:
from z3 import *
import numpy

Пример: Найти uint32 a такой, что (0xDEADDEAD >> 2) ^ a == 0xBEEFBEEF

In [9]:
a = BitVec('a', 32)
b = BitVecVal(0xDEADDEAD, 32)
c = BitVecVal(0xBEEFBEEF, 32)
s = Solver()
s.add(LShR(b, 2) ^ a == c)
if s.check() == sat:
    print "0x%8X" % s.model()[a].as_long()
else:
    print "Equation unsatisfiable"
0x8944C944
In [17]:
a = numpy.uint32(0x8944C944)
(0xDEADDEAD >> 2) ^ a == 0xBEEFBEEF
Out[17]:
True

Пример: Найти вещественные x, y такие, что $x^2/4 + y^2 < 1$, $x + y > 2.1$

In [20]:
x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 2.1, x ** 2 / 4 + y ** 2 < 1)
print s.check()
print s.model()
sat
[x = 7/4, y = 3/8]
In [22]:
7./4 + 3./8, (7./4) ** 2 / 4 + (3./8) ** 2
Out[22]:
(2.125, 0.90625)

todo пример со строкой xor и crc32. С какими 4 байтами нужно сксорить строку, чтобы получить такой CRC32?

In [1]:
import binascii, zlib
from array import array

poly = 0xEDB88320

table = array('L')
for byte in range(256):
    crc = 0
    for bit in range(8):
        if (byte ^ crc) & 1:
            crc = (crc >> 1) ^ poly
        else:
            crc >>= 1
        byte >>= 1
    table.append(crc)

def crc32(string):
    value = 0xffffffffL
    for ch in string:
        value = table[(ord(ch) ^ value) & 0xff] ^ (value >> 8)

    return -1 - value

# test

data = (
    '',
    'test',
    'hello world',
    '1234',
    'A long string to test CRC32 functions',
)

for s in data:
    print repr(s)
    a = binascii.crc32(s)
    print '%08x' % (a & 0xffffffffL)
    aa = zlib.crc32(s)
    print '%08x' % (aa & 0xffffffffL)
    b = crc32(s)
    print '%08x' % (b & 0xffffffffL)
    print
''
00000000
00000000
00000000

'test'
d87f7e0c
d87f7e0c
d87f7e0c

'hello world'
0d4a1185
0d4a1185
0d4a1185

'1234'
9be3e0a3
9be3e0a3
9be3e0a3

'A long string to test CRC32 functions'
d2d10e28
d2d10e28
d2d10e28

Пример: задача с VolgaCTF, reverse. От кодов символов флага вычисляется и проверяется ряд полиномов. Иногда задавать условия для SMT-сольвера удобнее, генерируя строки условий, а затем исполняя их в глобальном контексте.

In [30]:
formulas = '''\
13 * s[29] + s[36] * 132 * s[0] + 13 * s[19] + 3 * s[1] - s[30] * 14 * s[30] + s[34] * 60 * s[3] + (-14) * s[26] + (-8) * s[28] - s[28] + 3 * s[19] + 10 * s[7] - s[4] + s[30] + 8 * s[42] == 1311351
(-11) * s[43] + s[20] * 20 * s[44] + s[35] * 60 * s[5] - s[40] * s[3] * 1008 * s[1] + 8 * s[44] + (-10) * s[28] + (-7) * s[35] - 2 * s[27] + (-4) * s[17] - s[17] - 8 * s[26] - s[18] - 8 * s[9] == (-1324642844)
11 * s[6] + s[25] + 7 * (s[32] + s[26]) + s[36] * 180 * s[33] + s[35] * 99 * s[9] + (-12) * s[42] - s[22] * 32 * s[27] + 10 * s[15] + 15 * s[8] + 8 * s[4] + (-10) * s[33] + 14 * s[8] == 910067
15 * s[0] + 13 * s[13] + (-13) * s[3] + 3 * s[15] + 3 * s[34] + 6 * s[39] - s[32] * 60 * s[38] + 15 * s[33] + s[6] * 60 * s[32] + (-4) * s[30] - s[30] + (-8) * s[36] - s[36] - s[11] + 8 * s[35] + 7 * s[0] == (-119712)
9 * s[5] + s[8] + s[0] + 10 * s[3] - s[13] * 84 * s[2] + s[27] * 16 * s[28] + 12 * s[28] + 2 * s[11] + (-14) * s[40] + (-12) * s[32] + 15 * s[10] + (-4) * s[23] - s[23] + (-3) * s[11] + (-5) * s[5] == (-914171)
11 * s[31] + 13 * s[18] + s[18] * 84 * s[26] + (-12) * s[7] + 14 * s[42] + 6 * s[23] - s[20] * s[33] * 1260 * s[24] - s[44] * 98 * s[17] + s[41] * 270 * s[43] * s[33] + 10 * s[8] == (-701812476)
(-11) * s[23] + 9 * s[36] + (-7) * s[36] + s[38] * 78 * s[0] + (-8) * s[40] - s[40] - s[42] * 10 * s[34] + (-7) * s[36] + s[36] + s[13] * s[14] * 560 * s[34] - s[32] + 11 * s[32] + 15 * s[35] == 805471623
s[44] * 55 * s[15] + s[17] * 48 * s[36] + 2 * (s[19] + 6 * s[2]) - s[14] * 14 * s[38] + 11 * s[2] - 12 * s[6] * s[14] + 8 * s[11] - s[11] + s[23] * 13 * s[18] + (-10) * s[4] + 3 * s[21] == 986086
13 * s[20] + 7 * s[2] + (-14) * s[42] - 4 * s[24] + 8 * s[37] + s[19] * 78 * s[36] - 63 * s[24] * s[42] - s[18] - 2 * s[20] - 4 * s[31] + 4 * s[15] + 10 * s[38] + 7 * s[20] - 4 * s[26] == (-471203)
s[43] + s[27] + 3 * s[29] + (-9) * s[20] + 4 * s[15] - s[25] - s[41] + 15 * s[12] + (-6) * s[13] + 4 * s[9] - s[4] * 24 * s[28] + 130 * s[4] * s[41] + 14 * s[3] + 8 * s[0] - s[0] == 584152
11 * s[18] - 8 * s[22] + 4 * s[17] + (-9) * s[29] + 8 * s[14] - 8 * s[1] + (-12) * s[38] + 2 * s[26] + (-11) * s[14] + 6 * s[3] + s[39] * 3 * s[35] + (-10) * s[16] + 22 * s[21] * s[29] + 14 * s[42] == 302239
15 * s[35] + (-13) * s[14] + (-7) * s[41] + (-7) * s[38] + 9 * s[3] + s[39] * s[9] * 360 * s[16] + 6 * s[24] - s[30] + 135 * s[2] * s[16] + (-9) * s[9] + 4 * s[30] - s[23] * 112 * s[10] == 118806054
13 * s[1] + (-3) * s[25] + s[28] * 150 * s[27] + (-13) * s[43] + s[38] * 12 * s[0] - 4 * s[29] - s[10] - 2 * s[42] + 4 * s[26] - 8 * s[33] + (-10) * s[12] + s[39] * 18 * s[24] + 13 * s[20] == 1675940
s[18] + 5 * s[37] + 15 * s[43] + s[16] + 11 * s[13] + s[6] * 15 * s[23] + (-6) * s[20] - s[8] * 10 * s[23] + 135 * s[20] * s[6] + 10 * s[19] + (-6) * s[18] + 14 * s[2] + (-12) * s[33] == 1333282
9 * s[0] + 9 * s[1] + s[6] * 156 * s[24] + (-4) * s[32] - s[32] + 2 * s[39] + 15 * s[9] + 10 * s[24] - 4 * s[19] + 8 * s[20] + 4 * s[20] + (-8) * s[23] - s[23] + 13 * s[40] + (-7) * s[29] + (-3) * s[36] + (-12) * s[0] == 1457854
13 * s[5] + 13 * s[36] + 7 * s[9] + (-15) * s[30] + (-12) * s[43] + 11 * s[40] + (-12) * s[18] + 12 * s[12] + (-11) * s[18] - s[4] * 104 * s[0] - s[20] * 132 * s[1] - 8 * s[6] + 8 * s[19] - s[19] + 5 * s[14] == (-2582478)
9 * s[40] + 11 * s[18] + 3 * s[21] + (-13) * s[1] + s[31] + s[30] - 4 * s[29] + 8 * s[4] - s[4] - s[36] * 210 * s[29] + (-14) * s[37] - 6 * s[44] * s[21] - 2 * s[39] + 8 * s[29] + 4 * s[35] == (-1562727)
3 * s[31] + 6 * s[19] - s[7] * 130 * s[36] + 12 * s[40] - s[12] * 42 * s[31] + 4 * s[2] + 10 * s[0] + s[10] * 99 * s[28] - s[34] * 40 * s[24] - 8 * s[5] + s[12] + 7 * s[0] == (-1038889)
s[23] + 5 * s[41] + 9 * s[3] + s[1] * 15 * s[41] + 5 * s[22] + (-15) * s[25] - s[31] * 24 * s[22] - 4 * s[12] - s[16] * 36 * s[44] + (-10) * s[4] + 9 * s[8] - 45 * s[34] * s[1] == (-923909)
15 * s[5] + s[33] * 130 * s[40] + s[4] + 2 * s[10] - s[35] * 132 * s[16] + s[14] * 75 * s[23] - 2 * s[24] + (-6) * s[32] - 2 * s[26] + 4 * s[40] + (-11) * s[15] + 4 * s[19] - 8 * s[5] == 856586
5 * s[31] + (-15) * s[39] + s[19] * 90 * s[18] + s[27] * 16 * s[16] - s[44] * s[41] * 70 * s[28] + 2 * s[8] + s[42] * 35 * s[38] + 10 * s[7] + 2 * s[12] + 8 * s[29] + 4 * s[20] == (-53357640)
5 * s[23] + s[1] + 4 * (2 * s[29] - s[18] - s[21]) + s[28] * 39 * s[12] - s[36] * s[22] * 30 * s[21] + 8 * s[26] - s[26] + s[18] + 12 * s[0] + (-10) * s[17] - 12 * s[27] * s[17] == (-20510795)
3 * s[41] + 5 * s[6] + 8 * s[10] + 10 * s[8] - s[41] * 28 * s[9] + (-10) * s[30] + 10 * s[21] + 10 * s[19] - s[24] + 5 * s[8] + (-10) * s[22] + (-3) * s[23] + 4 * s[32] + 9 * s[30] + 11 * s[28] == (-117294)
9 * s[43] + 15 * s[29] + s[1] * 120 * s[44] + 12 * s[13] + 12 * s[15] + 14 * s[32] + 10 * s[25] + 13 * s[37] + (-4) * s[22] - s[22] + 8 * s[26] - s[26] + (-4) * s[36] - s[36] - s[13] + 7 * s[13] - s[40] * 36 * s[38] == 1256993
9 * s[25] + 5 * s[8] + s[37] * 28 * s[23] + 6 * s[13] + (-6) * s[17] + (-3) * s[26] - 2 * s[36] + (-6) * s[4] + (-10) * s[29] - 8 * s[3] + s[24] * 99 * s[9] + 4 * s[19] + s[11] * 84 * s[12] == 1373634
(-3) * s[17] + 9 * s[24] + 4 * s[37] + 9 * s[34] - 4 * s[34] + 8 * s[15] + s[7] * 40 * s[42] + 10 * s[15] - s[11] * s[27] * 360 * s[16] + 12 * s[5] - 15 * s[10] * s[16] + 13 * s[1] == (-62537013)
(-5) * s[23] + 15 * s[26] + 8 * s[25] + 15 * s[23] - s[1] * 90 * s[6] + (-6) * s[32] - 4 * s[8] + (-13) * s[32] + s[26] - s[14] * 70 * s[23] - 4 * s[9] - 8 * s[19] - s[12] * 78 * s[33] == (-1952483)
9 * s[22] + (-7) * s[27] + 8 * s[1] + 4 * (3 * s[9] + (-3) * s[31]) + (-6) * s[10] + 2 * s[38] + 8 * s[41] - s[41] + (-4) * s[13] - s[13] - 2 * s[8] - s[10] * 60 * s[16] + s[1] * 60 * s[38] - s[28] * 7 * s[1] == 447630
13 * s[7] + (-7) * s[13] + 9 * s[27] + (-2) * s[35] + 12 * s[34] + (-3) * s[14] + 63 * s[44] * s[27] + (-7) * s[20] + s[37] * 70 * s[42] - s[32] * 156 * s[19] - 2 * s[12] + (-12) * s[10] == 656269
11 * s[9] + s[1] * 56 * s[2] + (-4) * s[6] - s[6] - s[20] * 77 * s[14] + (-12) * s[34] + (-11) * s[38] - 8 * s[5] + (-15) * s[26] + s[11] * s[41] * 72 * s[29] - s[18] * s[35] * 528 * s[32] == (-716423735)
(-3) * s[13] + (-13) * s[38] + 15 * s[26] + 11 * s[13] + s[23] * 110 * s[8] + 2 * ((-3) * s[25] + 5 * s[27]) + s[37] * s[9] * 550 * s[34] + (-4) * s[7] - s[7] - s[31] * 135 * s[37] + 12 * s[11] + (-9) * s[8] == 498719083
(-7) * s[20] + (-3) * s[43] + s[29] + (-7) * s[35] + 11 * s[34] - s[39] * s[26] * 18 * s[37] - 4 * s[0] + 2 * s[8] - 8 * s[27] + 8 * s[15] - s[15] - s[26] * 8 * s[33] + (-13) * s[26] == (-19729480)
s[10] * s[0] * 182 * s[24] + s[32] * 2 * s[30] + (-4) * s[39] - s[39] + 10 * s[32] + 8 * s[17] - 8 * s[30] + 4 * s[34] + (-12) * s[29] - s[12] * 55 * s[41] + s[8] * s[4] * 1144 * s[17] == 1381453791
9 * s[3] + (-5) * s[34] + 6 * s[44] + (-11) * s[21] + (-14) * s[4] - 8 * s[5] + s[39] * 1344 * s[4] * s[21] + 5 * s[40] + 15 * s[1] - s[27] * 15 * s[26] + (-10) * s[13] + 11 * s[16] + 8 * s[17] - s[17] == 1411741755
13 * s[33] + s[20] + 4 * (s[6] - s[20]) + 8 * s[44] - s[44] - s[13] * 90 * s[36] + 6 * s[20] + (-4) * s[37] - s[37] + s[11] * s[32] * 20 * s[7] + (-4) * s[9] - s[9] + 2 * s[29] + (-10) * s[0] + s[23] * 156 * s[11] == 5981100
(-7) * s[19] + 7 * s[14] + 13 * s[6] + s[42] + s[23] * 4 * s[17] - 2 * s[40] + (-13) * s[17] + 9 * s[14] + 14 * s[1] - s[5] * 39 * s[13] + 6 * s[32] + 4 * s[29] - s[37] + 14 * s[24] == (-262868)
s[10] + s[9] * 10 * s[14] + 8 * s[44] + (-3) * s[13] - s[7] * 90 * s[26] + (-6) * s[27] + 11 * s[1] + 6 * s[27] + 2 * s[24] + s[27] - s[29] + (-8) * s[33] - s[33] + 6 * s[1] + (-13) * s[11] == (-563008)
(-7) * s[24] + (-11) * s[27] + (-11) * s[9] + s[12] + s[38] * 70 * s[30] + (-10) * s[29] - 2 * s[40] + (-6) * s[28] - s[43] * 8 * s[6] + 10 * s[25] - 2 * s[12] - s[3] * s[43] * ((s[40] * 256) - 32 * s[40]) == (-267345737)
(-11) * s[6] + 13 * s[29] + 13 * s[28] + s[29] + (-7) * s[20] + 5 * s[16] + 15 * s[10] + 4 * s[41] + 2 * s[17] + (-15) * s[18] + (-10) * s[30] + (-6) * s[24] + 13 * s[0] - 48 * s[43] * s[18] - 2 * s[7] == (-586617)
2 * s[12] + s[3] * 225 * s[0] + (-12) * s[36] + (-7) * s[3] - s[43] * 12 * s[7] + (-12) * s[43] - s[0] - s[4] * 18 * s[29] - s[11] * s[21] * 75 * s[2] + 12 * s[12] + 15 * s[25] == (-31526095)
'''.splitlines()
In [33]:
import re
In [39]:
%%time
solver = z3.Solver()
s = z3.Ints(' '.join('s%d' % i for i in range(45)))

for i in range(45):
    constr = 'solver.add(s[%d] > 32, s[%d] < 127)' % (i,i)
    eval(constr)

for f in formulas:
    constr = 'solver.add(' + f + ')'
    eval(constr)
    
#flag = 'VolgaCTF{' + '?' * 35 + '}'
#for i, ch in enumerate(flag):
#    if ch != '?':
#        solver.add(s[i] == ord(ch))

if solver.check() == z3.sat:
    print ''.join(map(chr, [solver.model().eval(s[i]).as_long() for i in range(45)]))
VolgaCTF{[email protected][email protected]}
Wall time: 1min 37s

Пример: задача Эйнштейна

Норвежец живёт в первом доме.
Англичанин живёт в красном доме.
Зелёный дом находится слева от белого, рядом с ним.
Датчанин пьёт чай.
Тот, кто курит Marlboro, живёт рядом с тем, кто выращивает кошек.
Тот, кто живёт в жёлтом доме, курит Dunhill.
Немец курит Rothmans.
Тот, кто живёт в центре, пьёт молоко.
Сосед того, кто курит Marlboro, пьёт воду.
Тот, кто курит Pall Mall, выращивает птиц.
Швед выращивает собак.
Норвежец живёт рядом с синим домом.
Тот, кто выращивает лошадей, живёт в синем доме.
Тот, кто курит Winfield, пьет пиво.
В зелёном доме пьют кофе.
In [5]:
from collections import OrderedDict
In [6]:
def solve_einstein_problem(props, conditions_fn):
    ks = props.keys()

    # Переменные
    variables = {}
    for i in range(len(ks)):
        for j in range(i + 1, len(ks)):
            for vi in props[ks[i]]:
                for vj in props[ks[j]]:
                    varname = vi + '_' + vj
                    variables[varname] = Bool(varname)
    
    conds = []
    # Существование и единственность
    for i in range(len(ks)):
        for j in range(i + 1, len(ks)):
            for vi in props[ks[i]]:
                # vi_vj1 || vi_vj2 || ...
                conds.append(Or(*[variables['%s_%s' % (vi, vj)] for vj in props[ks[j]]]))
                # vi1_vj1 => !vi1_vj2 && !vi1_vj3 && ... и !vi2_vj1 && !vi3_vj1 && ...
                for vj in props[ks[j]]:
                    conds.append(Implies(variables['%s_%s' % (vi, vj)], And(*[
                        Not(variables['%s_%s' % (vi, vjj)]) for vjj in props[ks[j]] if vjj != vj
                    ])))
                    conds.append(Implies(variables['%s_%s' % (vi, vj)], And(*[
                        Not(variables['%s_%s' % (vii, vj)]) for vii in props[ks[i]] if vii != vi
                    ])))
                                 
    # Транзитивность
    for i in range(len(ks)):
        for j in range(i + 1, len(ks)):
            for k in range(j + 1, len(ks)):
                for vi in props[ks[i]]:
                    for vj in props[ks[j]]:
                        for vk in props[ks[k]]:
                            # vi_vj && vj_vk => vi_vk
                            conds.append(Implies(And(variables['%s_%s' % (vi, vj)], variables['%s_%s' % (vj, vk)]), variables['%s_%s' % (vi, vk)]))
                            # vi_vj && vi_vk => vj_vk
                            conds.append(Implies(And(variables['%s_%s' % (vi, vj)], variables['%s_%s' % (vi, vk)]), variables['%s_%s' % (vj, vk)]))
                            # vi_vk && vj_vk => vi_vj
                            conds.append(Implies(And(variables['%s_%s' % (vi, vk)], variables['%s_%s' % (vj, vk)]), variables['%s_%s' % (vi, vj)]))
                              
    for k, v in variables.iteritems():
        conditions_fn.__globals__[k] = v
    task_predicates = conditions_fn()
    
    s = Solver()
    s.add(*(conds + task_predicates))
    if s.check() == sat:
        m = s.model()
        for vi in props[ks[0]]:
            print vi,
            for j in range(1, len(ks)):
                for vj in props[ks[j]]:
                    if m.evaluate(variables['%s_%s' % (vi, vj)]):
                        print vj,
            print
In [7]:
%%time
einstein_props = OrderedDict([
    ('number', ['n1', 'n2', 'n3', 'n4', 'n5']),
    ('nation', ['no', 'en', 'dk', 'de', 'sw']),
    ('color', ['green', 'white', 'yellow', 'blue', 'red']),
    ('drink', ['tea', 'milk', 'water', 'beer', 'coffee']),
    ('smoke', ['marlboro', 'dunhill', 'rothmans', 'pallmall', 'winfield']),
    ('pet', ['cat', 'bird', 'dog', 'horse', 'fish']),
])

def FromLeftNear(variables, prop1, prop2):
    nums = einstein_props['number']
    return And(*[
        Implies(variables['%s_%s' % (pos1, prop1)], variables['%s_%s' % (pos2, prop2)])
        for pos1, pos2 in zip(nums, nums[1:])
    ])

def Near(variables, prop1, prop2):
    nums = einstein_props['number']
    return And(*[
        Implies(variables['%s_%s' % (pos2, prop1)], Or(variables['%s_%s' % (pos1, prop2)], variables['%s_%s' % (pos3, prop2)]))
        for pos1, pos2, pos3 in zip([nums[1]] + nums, nums, nums[1:] + [nums[-2]])
    ])

result = solve_einstein_problem(einstein_props, lambda:[
    n1_no,
    en_red,
    FromLeftNear(globals(), 'green', 'white'),
    dk_tea, 
    Near(globals(), 'marlboro', 'cat'),
    yellow_dunhill,
    de_rothmans,
    n3_milk,
    Near(globals(), 'marlboro', 'water'),
    pallmall_bird,
    sw_dog,
    Near(globals(), 'no', 'blue'),
    blue_horse,
    beer_winfield,
    green_coffee
])
n1 no yellow water dunhill cat
n2 dk blue tea marlboro horse
n3 en red milk pallmall bird
n4 de green coffee rothmans fish
n5 sw white beer winfield dog
Wall time: 1.68 s