---
# System prepended metadata

title: Script RE
tags: [hàng độc quyền]

---

Các script để sẵn nhằm mục đích giải quyết nhanh các dạng Flag Checker kinh điển

# Automate debug with gdb 1  
automate debug và bruteforce flag bằng cách kiểm tra giá trị thanh ghi r12  
Để tránh mất thời gian viết lại pseudocode hoặc reverse pseudocode thì có thể vừa bruteforce vừa debug  
  
```python3=
#!/usr/bin/env python3

import pwn

pwn.context.log_level = "CRITICAL"  


def get_updated_value(flag_input,i) :
    PROMPT = b"(gdb)"
    io: pwn.tube
    with pwn.process(["gdb", "-q", "--nx", "./checker"]) as io:
        io.sendlineafter(PROMPT, b"b *0x0000555555555A3A")
        io.sendlineafter(PROMPT, b"run")
        io.sendline(flag_input.encode())
        for j in range(i):
            io.sendlineafter(PROMPT, b"continue")
        io.sendlineafter(PROMPT, b"info registers r12") #x/_ ___
        n=(io.recvline())

    return n[-2:-1]
        

flag = ""
for i in range(49):
    for s in range(33,127):
        print(chr(s),end='')
        u = get_updated_value(flag+chr(s),i)
        if u==b'1':
            flag=flag+chr(s)
            print((flag))
            break
print(flag)

```
Đã cố gắng thử viết automate debug nhiều bài bằng IDA python nhưng có vẻ không hiệu quả  
# Link Start TSCCTF 2025  
Áp dụng nguyên lý trên để giải quyết 1 bài toán khó reverse mà không cần reverse  
Lấy mảng:  
```python=
#!/usr/bin/env python3
import pwn

pwn.context.log_level = "CRITICAL"  


def get_updated_value(flag_input) :
    PROMPT = b"(gdb)"
    io: pwn.tube
    with pwn.process(["gdb", "-q", "--nx", "./chalj"]) as io:
        io.sendlineafter(PROMPT, b"b *0x0000555555555755")
        io.sendlineafter(PROMPT, b"run")
        io.sendline(flag_input.encode())

        io.sendlineafter(PROMPT, b"x/44b 0x7fffffffdd90")
        n=(io.recvline())
    
    #print(n[25:-1])
    #exit(0)
    return n[25:-1]
        
F=b';sDs\x1f\x10IE\x1fr$Uq\x7fq|$k~\x03ulOy!\x7fd}\x12tcU!`O[\rlO|=^nN\x00'
flag = ""
sym='''!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~'''
z=[]
for s in sym:
    u = get_updated_value(s+"a"*43)
    y= list(map(int, u.split(b'\t')))[:4]
    z.append(y[2])
    #print(y)
print(z)
z=[]
for s in sym:
    u = get_updated_value('a'+s+"a"*42)
    y= list(map(int, u.split(b'\t')))[:4]
    z.append(y[1])
    #print(y)
print(z)
z=[]
for s in sym:
    u = get_updated_value('a'+'a'+s+"a"*41)
    y= list(map(int, u.split(b'\t')))[:4]
    z.append(y[3])
    #print(y)
print(z)
z=[]
for s in sym:
    u = get_updated_value('a'+'a'+'a'+s+"a"*40)
    y= list(map(int, u.split(b'\t')))[:4]
    z.append(y[0])
    #print(y)
print(z)

```
Ánh xạ với enc:  

```python=
s2=[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94]
s3=[49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110]
s4=[17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78]
s1=[97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62]
enc=b';sDs\x1f\x10IE\x1fr$Uq\x7fq|$k~\x03ulOy!\x7fd}\x12tcU!`O[\rlO|=^nN\x00'
sym=b'''!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~'''
flag=''
for i in range(0,44,4):

    for k in range(len(s3)):
        if s3[k]==enc[i+2]:
            flag=flag+chr(sym[k])
    for k in range(len(s2)):
        if s2[k]==enc[i+1]:
            flag=flag+chr(sym[k])
    for k in range(len(s4)):
        if s4[k]==enc[i+3]:
            flag=flag+chr(sym[k])
    for k in range(len(s1)):
        if s1[k]==enc[i]:
            flag=flag+chr(sym[k])
    print(flag)
            
#TSC{Y0u_4Re_a_L1nK3d_LI5t_MasTeR_@ka_LLM~~~}
```
# Giải pháp thay thế pwntools + gdb  
có vẻ gdb không phải lúc nào cũng hữu ích:  
![image](https://hackmd.io/_uploads/Sk8UWafYyg.png)  

tìm giải pháp thay thế có vẻ hơi khó khăn nhưng khả năng vẫn có thể làm được :\(\(  
vấn đề khó khăn nhất là nhập vào từ bàn phím để truyền vào scanf hoặc các dạng tương tự và không rõ hiệu năng khi autodebug bằng script trên IDAPython sẽ thế nào :\(\(  


# ASIS Final 2024  
chuyển hex từ hex editor sang bytes python  
Source:  
```C=
__int64 __fastcall sub_5555555556EB(_BYTE *a1)
{
  int i; // [rsp+14h] [rbp-24h]
  int k; // [rsp+14h] [rbp-24h]
  int j; // [rsp+18h] [rbp-20h]
  int m; // [rsp+18h] [rbp-20h]
  int v6; // [rsp+1Ch] [rbp-1Ch]
  int v7; // [rsp+1Ch] [rbp-1Ch]
  _BYTE *v8; // [rsp+20h] [rbp-18h]
  _BYTE *v9; // [rsp+28h] [rbp-10h]
  _BYTE *v10; // [rsp+28h] [rbp-10h]
  _BYTE *v11; // [rsp+30h] [rbp-8h]
  _BYTE *v12; // [rsp+30h] [rbp-8h]

  v11 = a1;
  v8 = byte_555555558AE0;
  for ( i = 0; i <= 7; ++i )
  {
    v6 = 8 * (unsigned __int8)(*v11++ ^ *v8++);
    v9 = a1;
    for ( j = 0; j <= 7; ++j )
    {
      if ( i != j )
        *v9 ^= byte_5555555580E0[v6 + j];
      ++v9;
    }
  }
  v12 = a1;
  for ( k = 0; k <= 7; ++k )
  {
    v7 = 8 * (unsigned __int8)(*v12++ ^ *v8++);
    v10 = a1;
    for ( m = 0; m <= 7; ++m )
    {
      if ( k != m )
        *v10 ^= byte_5555555580E0[v7 + m];
      ++v10;
    }
  }
  return 0LL;
}
```
Chuyển hex sang bytes:  
```python=
hex_string = 'DD DB 18 E4 AB 3B F6 2B  7E FD D2 1F FF C0 4A 7A '
hex_string = hex_string.replace(" ", "").replace("\n", "")
byte_array = bytes.fromhex(hex_string)
print(byte_array)
```

script solve:  
```python=
byte_5555555580E0=b''#dài
byte_555555558AE0=b''#dài
def reverse_sub_5555555556EB(a1: bytearray):
    global byte_555555558AE0, byte_5555555580E0
    v8 = byte_555555558AE0
    for k in reversed(range(8)):
        v7 = 8 * (a1[k] ^ v8[k + 8])
        for m in reversed(range(8)):
            if k != m:
                a1[m] ^= byte_5555555580E0[v7 + m]
    for i in reversed(range(8)):
        v6 = 8 * (a1[i] ^ v8[i])
        for j in reversed(range(8)):
           if i != j:
                a1[j] ^= byte_5555555580E0[v6 + j]

    return a1
encrypted_data = bytearray(b'')
for i in range(0,len(encrypted_data),8):
    original_data = reverse_sub_5555555556EB(encrypted_data[i:i+8])
    with open('asis1.png', 'ab') as f:
        f.write(original_data)
```
Flag: ~~ASIS\{R3d0c3\_@\_siMpl3\_X0R\_3nCryPt!0n\}~~
# Angr symbolic mem  
một vài script angr để thay thế z3 khi giải mấy bài flag checker không thể reverse  
Pseudo code(rất khó để reverse):  
```C=
__int64 __fastcall main(int a1, char **a2, char **a3)
{
  __int64 v3; // rdx
  __int64 v4; // rdi
  __int64 v5; // r11
  __int64 *v6; // r10
  int v7; // esi
  __int64 v8; // rcx
  __int64 *v9; // rax
  __int64 v10; // rdx
  __int64 v11; // rdx
  unsigned __int64 v12; // r9
  int v13; // eax
  char *v14; // rbx
  void **v15; // rbp
  unsigned __int8 v16; // di
  __int64 v18[4]; // [rsp+0h] [rbp-78h] BYREF
  char v19[26]; // [rsp+20h] [rbp-58h] BYREF
  char v20[26]; // [rsp+3Ah] [rbp-3Eh] BYREF
  char v21; // [rsp+54h] [rbp-24h] BYREF
  unsigned __int64 v22; // [rsp+58h] [rbp-20h]

  v22 = __readfsqword(0x28u);
  __printf_chk(1LL, "I'm practicing my math skills. Give me nine integers: ", a3);
  __isoc99_scanf(
    "%d %d %d %d %d %d %d %d %d",
    &dword_5555555580A0 - 8,
    &dword_5555555580A0 - 7,
    &dword_5555555580A0 - 6,
    &dword_5555555580A0 - 5,
    &dword_5555555580A0 - 4,
    &dword_5555555580A0 - 3,
    &dword_5555555580A0 - 2,
    &dword_5555555580A0 - 1,
    &dword_5555555580A0);
  __printf_chk(1LL, "Hmm, let me think", v3);
  fflush(stdout);
  usleep(0x493E0u);
  putchar(46);
  fflush(stdout);
  usleep(0x493E0u);
  putchar(46);
  fflush(stdout);
  usleep(0x493E0u);
  puts(".");
  usleep(0x7A120u);
  v4 = -60LL;
  v5 = 0x400C0210000001LL;
  do
  {
    v6 = &qword_555555558080;
    v7 = 0;
    v8 = 1LL;
    v9 = &qword_555555558080;
    do
    {
      v10 = *(int *)v9;
      v9 = (__int64 *)((char *)v9 + 4);
      v11 = v8 * v10;
      v8 *= v4;
      v7 += v11;
    }
    while ( &unk_5555555580A4 != (_UNKNOWN *)v9 );
    if ( (_DWORD)v4 == 44
      || (_DWORD)v4 == 58
      || (v12 = (unsigned int)(v4 + 37), (unsigned int)v12 <= 0x36) && _bittest64(&v5, v12) )
    {
      if ( v7 )
      {
LABEL_16:
        puts("Those aren't the right numbers. Try again!");
        return 1LL;
      }
    }
    else if ( !v7 )
    {
      goto LABEL_16;
    }
    ++v4;
  }
  while ( v4 != 60 );
  if ( dword_5555555580A0 != 1 )
  {
    do
    {
      v13 = *(_DWORD *)v6;
      v6 = (__int64 *)((char *)v6 + 4);
      v11 = (unsigned int)(v13 >> 31);
      LODWORD(v11) = v13 % dword_5555555580A0;
      *((_DWORD *)v6 - 1) = v13 / dword_5555555580A0;
    }
    while ( v6 != (__int64 *)&unk_5555555580A4 );
  }
  __printf_chk(1LL, "Correct! Here's the flag: ", v11);
  v14 = v19;
  v18[0] = qword_555555558080;
  v15 = &off_555555558020;
  v18[1] = qword_555555558088;
  LOWORD(v18[2]) = dword_555555558090;
  WORD1(v18[2]) = dword_555555558094;
  WORD2(v18[2]) = dword_555555558098;
  HIWORD(v18[2]) = dword_55555555809C;
  LOWORD(v18[3]) = dword_5555555580A0;
  qmemcpy(v19, v18, sizeof(v19));
  qmemcpy(v20, v18, sizeof(v20));
  do
  {
    v16 = *(_BYTE *)v15 ^ *v14++;
    v15 = (void **)((char *)v15 + 1);
    *(v14 - 1) = v16;
    putchar(v16);
  }
  while ( &v21 != v14 );
  putchar(10);
  return 0LL;
}

```
  
Script angr:  
đã tùy biến linh hoạt để có thể áp dụng giải các bài toán tương tự  
```python=
import angr
import sys

def success(state):
    return b'Correct!' in state.posix.dumps(sys.stdout.fileno())#path muốn đến

def fail(state):
    return b'Try again!' in state.posix.dumps(sys.stdout.fileno())#path bỏ qua

def main():
    proj = angr.Project('polyomino')#file elf

    # define start addr
    start_addr = 0x401209
    init_state = proj.factory.blank_state(addr=start_addr, add_options={angr.options.LAZY_SOLVES})#doi khi phai tuy bien lai
    howmanyinput = 9 #so input nhap vao
    size = 4 #size input 
    inputt=[0]*howmanyinput
    
    for i in range(howmanyinput):
        inputt[i]= init_state.solver.BVS('input'+str(i), size*8,explicit_name=True)
   
    addresstostore = 0x404080 #dia chi luu 
    for i in range(howmanyinput):
        init_state.memory.store(addresstostore+i*size,inputt[i],endness='Iend_LE')#doi khi se phai tuy bien lai
    # prepare simulation
    simulation = proj.factory.simgr(init_state)

    simulation.explore(find=success, avoid=fail)
    simulation.explore(find=success, avoid=fail)
    ketqua = [0]*howmanyinput
    if simulation.found:
        solution_state = simulation.found[0]
        for i in range(howmanyinput):
            ketqua[i] = solution_state.solver.eval(inputt[i],cast_to=int)#cast_to=int do dau vao la integer
            print(ketqua[i], end=' ')
    else:
        raise Exception('Counld not find input')

if __name__ == '__main__':
    main()

```
# angr1  
1 bài toán khác  
```python=
import angr
import claripy

def good(state):
    return b'Flag' in state.posix.dumps(1)

def bad(state):
    return b'Try' in state.posix.dumps(1)

path = "U"

proj = angr.Project(path)
# argv1 = claripy.BVS('arg1', 52*8)
m_args = [proj.filename, claripy.BVS('arg1', 9*8)]#thay 9 bằng strlen(input)
state = proj.factory.entry_state(args=m_args)
simulation = proj.factory.simgr(state)
simulation.explore(find=good, avoid=bad)
if simulation.found:
    solution_state = simulation.found[0]
    print(simulation.found[0].posix.dumps(1))
    # stdout
    print(simulation.found[0].posix.dumps(0))
    # stdin such as input by scanf
    print(solution_state.solver.eval(m_args[1], cast_to=bytes))
    # commandline input, flag
else:
    print("NO")

```
# angr2  
Giới hạn mỗi bytes trong input xuống chỉ từ 33->127 thay vì 0->255
```python=
import angr
# load the binary into an angr project
p = angr.Project("./warmup")
state = p.factory.blank_state(addr=0x4009D8)
flag_len = 0x6CCD7C-0x6CCD60
input=state.se.BVS('input', flag_len * 8)
for i in xrange(flag_len):
    state.add_constraints(input.get_byte(i) >= 0x20)
    state.add_constraints(input.get_byte(i) <= 0x7D)

state.memory.store(0x6CCD60, input)
path = p.factory.path(state=state)
ex = p.surveyors.Explorer( start=path, find=(0x400C6C), )
ex.run()
found_state = ex.found[0].state
print found_state.se.any_str(input) # EKO{1s_th1s_ju5t_4_w4rm_up?}
```
# IDA python  
## Lấy giá trị thanh ghi eax tại breakpoint  
```python=
import ida_dbg
import ida_idaapi

# Khởi động trình debug
ida_dbg.load_debugger("win32", False)

# Đường dẫn đến file thực thi
executable_path = "D:/ADMIN/rev-bin/atdb.exe"
working_directory = "D:/ADMIN/rev-bin"

# Khởi chạy quá trình debug
ida_dbg.start_process(executable_path, "", working_directory)

# Đặt breakpoint tại địa chỉ cụ thể
bpt_addr = 0x401567
ida_dbg.add_bpt(bpt_addr)

# Chạy chương trình đến breakpoint
ida_dbg.request_continue_process()

c = ida_dbg.get_reg_val("EAX")
print(f"Value in RAX: {hex(c)}")

```
# libc.so.6  
ăn cắp code từ bài giải packeta akasec của [neziRzz](https://github.com/neziRzz/CTF_Writeups/blob/main/Akasec%20CTF%202024/Packeta/wu.md) để lấy ví dụ về sử dụng các hàm độc quyền trong C ngay trong python  
lưu ý random trong python khác với C và cũng khác nhau giữa windows và linux  
```python=
from Crypto.Cipher import ARC4
from ctypes import CDLL
from capstone import *

md = Cs(CS_ARCH_X86, CS_MODE_64)

libc = CDLL("libc.so.6")
ct = [0x4d, 0x75, 0xac, 0xea, 0x75, 0xab, 0x78, 0x7, 0x90, 0x58, 0x8e, 0x25, 0x7, 0x84, 0x3f, 0x73, 0x2b, 0xa2, 0x70, 0x40, 0x78, 0x62, 0x4b, 0xfd, 0x65, 0xf0, 0x9b, 0x7, 0x58, 0x44, 0x9d, 0xca, 0x5a, 0x37]
v4 = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"

for i in range(500):
	libc.srand(4919 + i) #tuyệt đối không thể thay thế srand() bằng random.seed() trong python
	key = ""
	for j in range(16):
		key += v4[libc.rand() % 62] 
	cipher = ARC4.new(key.encode())
	asm = cipher.decrypt(bytes(ct))
	for j in md.disasm(asm, 0x401000):
		print(i, j)
        
```
# Z3-1  
Bài này khá dài, để đây chủ yếu là để ví dụ về cách gọi biến nhanh  
```python=
from z3 import *
solver = Solver()

C = {f'C{hex(i)[2:].zfill(3).upper()}': Int(f'C{hex(i)[2:].zfill(3).upper()}') for i in range(0x40, 0x100)}
solver.add(C['C0D0'] + C['C04C'] + C['C095'] + C['C0A3'] + C['C07D'] + C['C056'] + C['C061'] + C['C07A'] + C['C094'] + C['C0CA'] == 808) 
solver.add( C['C048'] + C['C04C'] + C['C084'] + C['C056'] + C['C08A'] + C['C0B9'] + C['C09B'] + C['C096'] + C['C0B0'] + C['C051'] + C['C07C'] == 846 ) 
solver.add( C['C0B6'] + C['C0CC'] == 110 ) 
solver.add( C['C0BD'] + C['C06E'] + C['C064'] + C['C071'] + C['C09D'] + C['C099'] + C['C0BD'] + C['C09E'] + C['C0BB'] + C['C055'] + C['C040'] + C['C05C'] == 838 ) 
solver.add( C['C070'] + C['C0B0'] + C['C0B1'] + C['C05E'] + C['C096'] + C['C080'] + C['C071'] + C['C04A'] + C['C06F'] + C['C05B'] + C['C068'] + C['C062'] + C['C085'] + C['C044'] + C['C081'] + C['C04A'] == 1314 ) 
solver.add( C['C043'] + C['C0B6'] + C['C046'] + C['C0A6'] + C['C0B7'] + C['C05C'] + C['C0AF'] + C['C04D'] + C['C08A'] + C['C0C6'] + C['C0A0'] + C['C0C6'] == 906 ) 
solver.add( C['C0C8'] + C['C07D'] + C['C06F'] + C['C08A'] + C['C09F'] + C['C043'] + C['C05C'] + C['C096'] + C['C0BD'] + C['C072'] + C['C049'] + C['C0B5'] + C['C0BF'] + C['C049'] + C['C085'] + C['C0C9'] + C['C08F'] + C['C055'] + C['C0CA'] + C['C09E'] == 1385 ) 
solver.add( C['C0B3'] + C['C06A'] + C['C099'] + C['C0C1'] + C['C04E'] + C['C074'] + C['C0AF'] + C['C095'] + C['C065'] + C['C047'] + C['C04E'] + C['C0AD'] == 802 ) 
solver.add( C['C05A'] + C['C076'] + C['C08D'] + C['C06B'] + C['C0CE'] + C['C086'] + C['C0C8'] + C['C097'] + C['C082'] + C['C0C7'] + C['C0C4'] + C['C097'] + C['C073'] == 976 ) 
solver.add( C['C097'] + C['C08F'] + C['C08B'] + C['C0A7'] + C['C07B'] + C['C061'] + C['C085'] == 563 ) 
solver.add( C['C050'] + C['C066'] + C['C042'] + C['C0D0'] + C['C069'] + C['C096'] + C['C063'] == 611 ) 
solver.add( C['C06C'] + C['C08E'] + C['C063'] + C['C06E'] + C['C08B'] + C['C08C'] + C['C0A8'] + C['C044'] + C['C061'] + C['C0A0'] + C['C0C5'] + C['C0AB'] + C['C09D'] + C['C064'] + C['C0C1'] + C['C075'] + C['C09E'] + C['C081'] + C['C07E'] == 1407 ) 
solver.add( C['C0A1'] + C['C064'] + C['C055'] + C['C073'] + C['C04A'] + C['C09C'] + C['C0BD'] + C['C08E'] + C['C0BD'] + C['C0C2'] == 753 ) 
solver.add( C['C080'] + C['C068'] + C['C0CC'] + C['C0AC'] + C['C04B'] + C['C0A2'] + C['C0B7'] + C['C060'] + C['C089'] + C['C056'] + C['C09F'] + C['C06B'] + C['C098'] + C['C082'] + C['C076'] + C['C0BD'] == 1109 ) 
solver.add( C['C073'] + C['C06D'] + C['C0C3'] + C['C088'] + C['C054'] + C['C0CE'] + C['C0A8'] + C['C0C2'] + C['C05D'] + C['C055'] + C['C0A3'] + C['C0A1'] + C['C076'] == 1004 ) 
solver.add( C['C05A'] + C['C0D0'] + C['C062'] + C['C099'] + C['C0C9'] + C['C0C4'] + C['C0C3'] + C['C08C'] + C['C04E'] + C['C0BF'] + C['C067'] + C['C0C0'] + C['C05B'] + C['C0C9'] + C['C09E'] + C['C07B'] == 1209 ) 
solver.add( C['C065'] + C['C07F'] + C['C09A'] + C['C04C'] + C['C076'] + C['C05F'] + C['C09B'] + C['C0B0'] + C['C0A8'] + C['C0A8'] + C['C061'] + C['C075'] + C['C05C'] + C['C075'] + C['C0A2'] + C['C0B0'] + C['C08C'] + C['C058'] + C['C067'] == 1371 ) 
solver.add( C['C08A'] + C['C0A7'] + C['C08E'] + C['C0A4'] == 241 ) 
solver.add( C['C099'] + C['C06F'] + C['C0C9'] + C['C0CB'] + C['C0A6'] + C['C055'] + C['C0B3'] + C['C088'] + C['C053'] == 647 ) 
solver.add( C['C0BD'] + C['C083'] + C['C05E'] == 233 ) 
solver.add( C['C086'] + C['C048'] + C['C05B'] + C['C054'] + C['C086'] + C['C04B'] == 484 ) 
solver.add( C['C0A6'] + C['C078'] + C['C05C'] + C['C0AF'] + C['C07F'] + C['C042'] + C['C074'] + C['C095'] == 655 ) 
solver.add( C['C089'] + C['C0AD'] + C['C081'] + C['C0CD'] + C['C0CD'] + C['C08C'] + C['C092'] + C['C0B9'] + C['C0CD'] + C['C093'] + C['C07B'] + C['C046'] + C['C0A7'] + C['C0A0'] + C['C04C'] == 1186 ) 
solver.add( C['C0A4'] + C['C072'] + C['C061'] + C['C0C1'] + C['C04B'] + C['C093'] + C['C0A2'] + C['C089'] + C['C0A9'] + C['C051'] + C['C0B5'] + C['C052'] + C['C0A1'] + C['C09F'] + C['C061'] + C['C0C4'] + C['C088'] + C['C09E'] == 1264 ) 
solver.add( C['C094'] + C['C047'] + C['C0A5'] + C['C0C3'] + C['C09A'] + C['C095'] + C['C08B'] + C['C049'] + C['C0BE'] + C['C0CA'] + C['C0AC'] + C['C075'] + C['C093'] + C['C04E'] + C['C070'] + C['C071'] == 1179 ) 
solver.add( C['C048'] + C['C0B9'] + C['C0BA'] + C['C097'] + C['C07E'] + C['C079'] + C['C0AB'] + C['C0A5'] == 721 ) 
solver.add( C['C07F'] + C['C06C'] + C['C0CC'] + C['C09E'] + C['C0A6'] + C['C0B5'] + C['C063'] + C['C095'] + C['C0B1'] + C['C0BA'] + C['C058'] == 803 ) 
solver.add( C['C09A'] + C['C052'] == 134 ) 
solver.add( C['C074'] + C['C0B1'] + C['C05E'] == 278 ) 
solver.add( C['C071'] + C['C05A'] + C['C061'] + C['C0C1'] + C['C078'] == 369 ) 
solver.add( C['C0C7'] + C['C09F'] + C['C07D'] + C['C083'] + C['C081'] + C['C09A'] == 429 ) 
solver.add( C['C0A3'] + C['C06D'] + C['C0B2'] + C['C0BB'] + C['C050'] + C['C052'] + C['C09C'] + C['C0A0'] + C['C053'] + C['C060'] + C['C095'] + C['C04C'] + C['C07A'] + C['C072'] == 1016 ) 
solver.add( C['C0C8'] + C['C0A8'] + C['C08F'] + C['C050'] + C['C082'] + C['C04C'] + C['C06B'] + C['C046'] + C['C0C9'] + C['C096'] + C['C06E'] + C['C050'] + C['C0BA'] + C['C090'] + C['C06E'] + C['C0A4'] + C['C093'] + C['C0BE'] == 1240 ) 
solver.add( C['C046'] + C['C04B'] + C['C09E'] + C['C0C1'] + C['C05E'] + C['C088'] + C['C08C'] + C['C06F'] == 610 ) 
solver.add( C['C05A'] + C['C0C8'] + C['C0B4'] + C['C0BE'] + C['C087'] + C['C076'] + C['C073'] + C['C05B'] + C['C07A'] + C['C06D'] + C['C0B0'] + C['C072'] + C['C08D'] == 1010 ) 
solver.add( C['C065'] + C['C060'] + C['C0C7'] + C['C08E'] + C['C04F'] + C['C07A'] + C['C0C9'] + C['C068'] + C['C0AF'] + C['C084'] + C['C09F'] + C['C08B'] + C['C089'] + C['C0A8'] + C['C091'] == 1051 ) 
solver.add( C['C04B'] + C['C08C'] + C['C064'] + C['C0B4'] + C['C0A9'] + C['C0CE'] + C['C0C2'] + C['C08F'] == 633 ) 
solver.add( C['C050'] + C['C08B'] + C['C07A'] + C['C063'] + C['C080'] + C['C05D'] + C['C06E'] + C['C041'] + C['C0B0'] + C['C0B2'] + C['C045'] + C['C08D'] + C['C0C9'] + C['C0A5'] + C['C059'] + C['C07F'] + C['C07B'] + C['C059'] == 1352 ) 
solver.add( C['C07F'] + C['C0C9'] + C['C048'] + C['C092'] + C['C095'] + C['C051'] == 443 ) 
solver.add( C['C04F'] + C['C062'] == 177 ) 
solver.add( C['C06B'] + C['C05C'] + C['C090'] + C['C080'] + C['C060'] + C['C041'] + C['C05B'] == 575 ) 
solver.add( C['C04E'] + C['C0C6'] + C['C0B7'] + C['C04E'] + C['C0D0'] + C['C0AC'] + C['C049'] + C['C060'] + C['C07C'] == 710 ) 
solver.add( C['C0C0'] + C['C079'] + C['C080'] + C['C0C0'] + C['C0CD'] + C['C0A7'] + C['C098'] + C['C09D'] + C['C0B5'] == 678 ) 
solver.add( C['C06E'] + C['C09B'] + C['C072'] + C['C067'] + C['C079'] + C['C047'] + C['C05D'] + C['C051'] + C['C082'] + C['C078'] + C['C0C9'] == 831 ) 
solver.add( C['C058'] + C['C0CE'] + C['C088'] + C['C0C5'] + C['C082'] + C['C09D'] == 434 ) 
solver.add( C['C095'] + C['C08B'] + C['C092'] + C['C061'] + C['C08A'] == 377 ) 
solver.add( C['C0AC'] + C['C093'] + C['C0CE'] + C['C0AD'] + C['C075'] + C['C0CC'] + C['C0BC'] + C['C0CA'] + C['C069'] == 579 ) 
solver.add( C['C058'] + C['C069'] + C['C0A3'] + C['C0C0'] + C['C077'] + C['C047'] + C['C08B'] + C['C0B2'] + C['C0B5'] + C['C07A'] + C['C045'] + C['C0AE'] + C['C072'] + C['C047'] + C['C080'] + C['C06B'] + C['C0A8'] + C['C061'] == 1318 ) 
solver.add( C['C0A9'] + C['C08A'] + C['C079'] + C['C0C3'] == 339 ) 
solver.add( C['C0D0'] + C['C0A4'] + C['C0C1'] + C['C08C'] + C['C07F'] + C['C0B4'] + C['C0CD'] + C['C0C7'] + C['C0A0'] + C['C09E'] + C['C074'] + C['C085'] + C['C08F'] + C['C061'] + C['C0CB'] + C['C0C2'] + C['C05D'] + C['C08D'] + C['C047'] == 1411 ) 
solver.add( C['C087'] + C['C0C8'] + C['C09E'] == 186 ) 
solver.add( C['C05B'] + C['C08A'] + C['C070'] + C['C0C2'] + C['C0A6'] + C['C061'] + C['C043'] + C['C06D'] == 596 ) 
solver.add( C['C0C8'] + C['C0B2'] + C['C04D'] + C['C073'] + C['C0BA'] + C['C0BF'] + C['C058'] + C['C0C3'] + C['C080'] + C['C04C'] == 756 ) 
solver.add( C['C093'] + C['C085'] + C['C0AE'] + C['C0B8'] == 278 ) 
solver.add( C['C0C7'] + C['C0C1'] + C['C093'] + C['C094'] + C['C0C3'] + C['C057'] + C['C069'] + C['C08C'] + C['C05D'] + C['C0C9'] + C['C0C2'] + C['C071'] + C['C049'] + C['C081'] == 968 ) 
solver.add( C['C0A9'] + C['C067'] + C['C0AD'] + C['C0A9'] + C['C08C'] + C['C080'] + C['C069'] + C['C097'] + C['C0C5'] + C['C0A6'] + C['C086'] + C['C041'] + C['C096'] + C['C0B0'] + C['C089'] + C['C08F'] + C['C0AC'] + C['C07D'] == 1480 ) 
solver.add( C['C05B'] + C['C043'] + C['C048'] + C['C059'] == 294 ) 
solver.add( C['C0A0'] + C['C08E'] + C['C094'] + C['C05A'] == 274 ) 
solver.add( C['C067'] + C['C09F'] + C['C070'] + C['C088'] + C['C079'] + C['C068'] + C['C05B'] + C['C075'] + C['C0BC'] + C['C079'] == 766 ) 
solver.add( C['C091'] + C['C0C2'] + C['C0C0'] + C['C0BA'] + C['C0B5'] + C['C08B'] + C['C072'] + C['C046'] + C['C074'] + C['C05C'] + C['C07A'] + C['C05A'] + C['C05C'] + C['C09C'] + C['C09D'] + C['C0CE'] == 1257 ) 
solver.add( C['C07D'] + C['C0B6'] == 151 ) 
solver.add( C['C079'] + C['C054'] + C['C04B'] + C['C091'] + C['C0B8'] + C['C058'] + C['C07C'] + C['C070'] + C['C0AC'] + C['C0BB'] + C['C093'] == 788 ) 
solver.add( C['C069'] + C['C097'] + C['C044'] + C['C0BC'] + C['C0A0'] + C['C0B6'] + C['C0C2'] + C['C056'] + C['C05F'] + C['C042'] + C['C0C5'] + C['C042'] + C['C073'] == 1043 ) 
solver.add( C['C077'] + C['C06F'] + C['C099'] + C['C0B7'] + C['C085'] + C['C098'] + C['C0B8'] + C['C0BB'] + C['C0BE'] + C['C074'] + C['C062'] + C['C08C'] + C['C054'] + C['C0A5'] + C['C0CF'] + C['C048'] + C['C082'] + C['C086'] == 1334 ) 
solver.add( C['C072'] + C['C0BB'] + C['C096'] + C['C044'] + C['C086'] + C['C081'] + C['C0AD'] + C['C06F'] + C['C042'] + C['C065'] + C['C0CE'] + C['C065'] + C['C0B0'] + C['C069'] + C['C0C0'] + C['C07F'] + C['C0B9'] + C['C094'] == 1400 ) 
solver.add( C['C043'] + C['C068'] + C['C047'] + C['C043'] + C['C073'] + C['C0B3'] + C['C041'] == 582 ) 
solver.add( C['C077'] + C['C067'] + C['C082'] + C['C097'] + C['C0BE'] + C['C044'] + C['C087'] + C['C0B1'] + C['C0CC'] + C['C0A2'] + C['C084'] + C['C085'] + C['C0CF'] + C['C055'] + C['C047'] + C['C074'] + C['C067'] + C['C06B'] == 1374 ) 
solver.add( C['C06C'] + C['C0A6'] + C['C08F'] + C['C0A7'] + C['C049'] + C['C083'] + C['C06F'] + C['C06F'] + C['C09A'] + C['C060'] + C['C08F'] + C['C0BD'] + C['C0A5'] == 1069 ) 
solver.add( C['C082'] + C['C095'] + C['C07B'] == 216 ) 
solver.add( C['C053'] + C['C05E'] + C['C06B'] + C['C069'] + C['C086'] + C['C094'] + C['C09D'] + C['C0B0'] + C['C08A'] + C['C053'] + C['C0BE'] + C['C092'] == 896 ) 
solver.add( C['C045'] + C['C087'] + C['C08C'] + C['C092'] + C['C052'] + C['C081'] + C['C0BA'] + C['C0A5'] + C['C054'] + C['C09E'] + C['C04D'] + C['C08D'] + C['C074'] + C['C060'] + C['C04B'] + C['C0BD'] + C['C09F'] + C['C07F'] == 1408 ) 
solver.add( C['C07F'] + C['C0B1'] + C['C053'] + C['C0B3'] + C['C070'] + C['C04A'] + C['C079'] + C['C070'] + C['C091'] + C['C07A'] + C['C0A5'] == 867 ) 
solver.add( C['C0B5'] + C['C05B'] + C['C062'] + C['C048'] == 297 ) 
solver.add( C['C097'] + C['C089'] + C['C056'] + C['C0C0'] + C['C069'] + C['C04B'] + C['C041'] + C['C042'] + C['C06C'] + C['C0BA'] + C['C0AB'] + C['C046'] + C['C04E'] + C['C08B'] + C['C08B'] == 1357 ) 
solver.add( C['C0B3'] + C['C087'] + C['C0A8'] + C['C07B'] + C['C086'] + C['C0C3'] + C['C0BA'] + C['C080'] + C['C049'] + C['C089'] == 797 ) 
solver.add( C['C0AC'] + C['C074'] + C['C053'] + C['C084'] + C['C04D'] + C['C0A5'] + C['C0AD'] + C['C088'] + C['C099'] + C['C05E'] + C['C09F'] + C['C0B0'] + C['C084'] == 1029 ) 
solver.add( C['C04C'] + C['C04D'] + C['C0A8'] == 232 ) 
solver.add( C['C0BB'] + C['C078'] + C['C06F'] + C['C074'] + C['C07C'] + C['C074'] == 467 ) 
solver.add( C['C04C'] + C['C0B6'] + C['C0B9'] + C['C0CA'] + C['C082'] + C['C0BA'] + C['C0BE'] + C['C08B'] == 599 ) 
solver.add( C['C04D'] + C['C062'] + C['C08E'] + C['C0C1'] + C['C0C6'] + C['C0B0'] + C['C055'] + C['C0B8'] + C['C086'] + C['C04D'] + C['C0AD'] + C['C0CE'] + C['C0A5'] + C['C087'] + C['C05D'] + C['C082'] == 1249 ) 
solver.add( C['C0A9'] + C['C062'] + C['C05F'] + C['C076'] + C['C0AE'] + C['C0A4'] + C['C087'] + C['C07E'] + C['C07A'] + C['C046'] + C['C095'] + C['C07E'] + C['C0C2'] + C['C097'] + C['C09A'] == 1156 ) 
solver.add( C['C07C'] + C['C086'] + C['C0C6'] + C['C0B1'] + C['C053'] + C['C087'] + C['C04C'] + C['C095'] + C['C0BF'] + C['C084'] + C['C074'] == 865 ) 
solver.add( C['C05D'] + C['C0B8'] + C['C04C'] + C['C095'] + C['C04F'] + C['C081'] + C['C092'] + C['C095'] + C['C068'] + C['C0BC'] + C['C0C5'] + C['C0AE'] + C['C056'] + C['C06C'] + C['C0B1'] + C['C063'] + C['C0A0'] + C['C043'] + C['C07D'] == 1439 ) 
solver.add( C['C0B8'] + C['C0C2'] + C['C06F'] + C['C0BC'] + C['C099'] + C['C057'] + C['C095'] == 489 ) 
solver.add( C['C095'] + C['C042'] + C['C09D'] + C['C05C'] + C['C04D'] + C['C086'] + C['C0AE'] + C['C05F'] + C['C08C'] + C['C0B3'] == 804 ) 
solver.add( C['C078'] + C['C0B3'] + C['C0BC'] + C['C08F'] + C['C04E'] + C['C0A3'] + C['C0AC'] + C['C08B'] + C['C0C7'] + C['C064'] + C['C099'] + C['C05E'] + C['C052'] + C['C0C2'] == 1030 ) 
solver.add( C['C089'] + C['C048'] + C['C0BD'] + C['C061'] + C['C069'] + C['C0BD'] + C['C05A'] + C['C09E'] + C['C0C7'] + C['C0CE'] + C['C049'] + C['C0C9'] + C['C0A0'] + C['C0AC'] + C['C040'] + C['C079'] + C['C095'] + C['C047'] == 1270 ) 
solver.add( C['C051'] + C['C0B7'] + C['C055'] + C['C099'] + C['C09F'] + C['C05B'] + C['C0BC'] + C['C075'] + C['C050'] == 620 ) 
solver.add( C['C061'] + C['C0D0'] + C['C055'] + C['C075'] + C['C050'] + C['C0B2'] + C['C0CF'] + C['C06F'] == 622 ) 
solver.add( C['C0C8'] + C['C05B'] + C['C0B8'] + C['C081'] + C['C069'] + C['C064'] + C['C0A2'] + C['C095'] + C['C09B'] + C['C08B'] + C['C06B'] + C['C050'] + C['C0CD'] + C['C0CD'] + C['C09F'] + C['C05F'] + C['C0B0'] + C['C094'] + C['C0C0'] == 1483 ) 
solver.add( C['C091'] + C['C0A5'] + C['C075'] + C['C06E'] + C['C0B3'] + C['C041'] + C['C0CC'] + C['C042'] + C['C068'] + C['C0A5'] + C['C09D'] + C['C0B9'] + C['C051'] == 1146 ) 
solver.add( C['C047'] + C['C0C1'] + C['C0D0'] + C['C0A1'] == 360 ) 
solver.add( C['C0CD'] + C['C078'] + C['C08C'] + C['C078'] + C['C065'] + C['C09E'] + C['C08A'] + C['C04C'] + C['C08D'] + C['C063'] + C['C073'] == 846 ) 
solver.add( C['C0B3'] + C['C053'] + C['C095'] + C['C07F'] + C['C06B'] + C['C08A'] + C['C059'] + C['C07E'] + C['C0D0'] + C['C064'] + C['C0BF'] + C['C07D'] + C['C09C'] + C['C0BD'] + C['C041'] + C['C041'] == 1307 ) 
solver.add( C['C0C4'] + C['C0A0'] + C['C0BD'] + C['C07A'] + C['C0A4'] + C['C0C8'] + C['C0B7'] + C['C06A'] + C['C083'] + C['C0B8'] + C['C077'] + C['C0AB'] + C['C08A'] + C['C0C7'] + C['C0A1'] + C['C07F'] + C['C0AD'] + C['C073'] + C['C069'] + C['C0C4'] == 1435 ) 
solver.add( C['C060'] + C['C063'] + C['C089'] + C['C07F'] + C['C0B3'] + C['C071'] + C['C093'] + C['C097'] + C['C0B0'] + C['C06F'] + C['C0CB'] + C['C0A1'] + C['C06A'] + C['C09E'] + C['C081'] == 1068 ) 
solver.add( C['C089'] + C['C059'] + C['C079'] + C['C0D0'] + C['C072'] == 414 ) 
solver.add( 2 * C['C0A4'] == 110 ) 
solver.add( C['C077'] + C['C084'] + C['C0BA'] + C['C05C'] + C['C078'] + C['C04A'] + C['C064'] + C['C055'] + C['C0C7'] + C['C092'] + C['C09B'] + C['C055'] + C['C0B2'] + C['C0B5'] + C['C07F'] + C['C0A0'] + C['C06B'] == 1286 ) 
solver.add( C['C08E'] + C['C06B'] + C['C053'] + C['C07D'] + C['C049'] + C['C0C9'] + C['C096'] + C['C043'] + C['C059'] + C['C053'] + C['C0AA'] == 759 ) 
solver.add( C['C0AC'] + C['C0A3'] + C['C099'] + C['C071'] == 322 ) 
solver.add( C['C075'] + C['C073'] + C['C0CD'] + C['C0B9'] + C['C04D'] + C['C077'] + C['C053'] + C['C088'] + C['C08C'] + C['C0B3'] + C['C062'] + C['C084'] == 1009 ) 
solver.add( C['C0D0'] + C['C09F'] + C['C0BF'] + C['C09B'] + C['C088'] + C['C0A2'] + C['C0BF'] + C['C046'] + C['C067'] == 697 ) 
solver.add( C['C0C3'] + C['C0BC'] == 150 ) 
solver.add( C['C09E'] + C['C063'] + C['C0C8'] + C['C09E'] + C['C0A4'] == 276 ) 
solver.add( C['C0CB'] + C['C09E'] + C['C05D'] + C['C044'] == 276 ) 
solver.add( C['C0CB'] + C['C065'] + C['C083'] + C['C08D'] + C['C069'] + C['C0A3'] + C['C0C5'] + C['C0AA'] + C['C06E'] + C['C09C'] + C['C0A7'] + C['C0C5'] + C['C066'] + C['C0AE'] + C['C044'] + C['C0C2'] == 1152 ) 
solver.add( C['C0C5'] + C['C080'] == 115 ) 
solver.add( C['C068'] + C['C06C'] + C['C0A6'] + C['C09B'] + C['C0BE'] + C['C09E'] + C['C0AE'] + C['C0BC'] + C['C062'] + C['C058'] + C['C060'] == 814 ) 
solver.add( C['C09C'] + C['C0B2'] + C['C0AA'] == 202 ) 
solver.add( C['C0A3'] + C['C0BE'] + C['C045'] + C['C051'] + C['C065'] + C['C0B8'] + C['C0B9'] + C['C082'] + C['C094'] + C['C055'] + C['C061'] == 874 ) 
solver.add( C['C08B'] + C['C050'] + C['C068'] + C['C041'] + C['C0AF'] + C['C04B'] + C['C0A9'] + C['C0BD'] + C['C0BA'] == 761 ) 
solver.add( C['C0C6'] + C['C09F'] + C['C05C'] + C['C073'] + C['C0AF'] == 364 ) 
solver.add( C['C085'] + C['C073'] + C['C0A7'] + C['C07F'] + C['C045'] + C['C0B1'] + C['C077'] + C['C0BA'] + C['C0BC'] + C['C04A'] + C['C04E'] + C['C075'] + C['C08E'] + C['C06E'] + C['C0BF'] + C['C0C2'] + C['C088'] + C['C0BA'] + C['C0BF'] == 1409 ) 
solver.add( C['C05F'] + C['C051'] + C['C0A3'] + C['C0B0'] + C['C079'] + C['C0B7'] + C['C065'] + C['C081'] + C['C06A'] + C['C059'] + C['C0B5'] + C['C0AA'] + C['C09E'] + C['C04A'] + C['C069'] == 1107 ) 
solver.add( C['C092'] + C['C0B7'] + C['C07E'] + C['C091'] + C['C0BB'] + C['C082'] + C['C09D'] + C['C0CA'] + C['C086'] + C['C0BB'] + C['C0AF'] + C['C0A6'] == 853 ) 
solver.add( C['C0C3'] + C['C07E'] + C['C084'] + C['C088'] == 364 ) 
solver.add( C['C041'] + C['C0C8'] + C['C095'] + C['C0A4'] + C['C0AD'] + C['C06A'] + C['C0AD'] + C['C078'] + C['C064'] + C['C076'] == 717 ) 
solver.add( C['C063'] + C['C067'] + C['C04F'] + C['C086'] + C['C065'] + C['C0AD'] + C['C096'] + C['C046'] == 575 ) 
solver.add( C['C0C3'] + C['C058'] + C['C0B0'] + C['C072'] + C['C09F'] + C['C06D'] + C['C06F'] + C['C072'] + C['C06B'] + C['C04B'] + C['C056'] + C['C0B1'] + C['C079'] + C['C060'] == 1052 ) 
solver.add( C['C0AD'] + C['C0C3'] + C['C045'] + C['C07F'] + C['C0A1'] + C['C09F'] + C['C09A'] + C['C0CC'] + C['C092'] + C['C0A6'] + C['C0CC'] + C['C071'] + C['C0AB'] + C['C097'] + C['C07E'] == 1162 ) 
solver.add( C['C055'] + C['C071'] + C['C048'] + C['C0AE'] + C['C0C7'] + C['C0A0'] + C['C0B9'] + C['C048'] + C['C075'] + C['C06A'] + C['C056'] + C['C059'] + C['C06A'] + C['C087'] + C['C093'] + C['C0B0'] + C['C0B1'] == 1220 ) 
solver.add( C['C098'] + C['C0A0'] + C['C0B4'] + C['C09A'] + C['C067'] + C['C068'] == 429 ) 
solver.add( C['C0B6'] + C['C072'] + C['C066'] + C['C0B5'] == 273 ) 
solver.add( C['C0A1'] + C['C099'] + C['C099'] + C['C04E'] + C['C07C'] + C['C0D0'] + C['C074'] + C['C0A3'] + C['C059'] + C['C0C9'] == 756 ) 
solver.add( C['C0A9'] + C['C0C7'] == 153 ) 
solver.add( C['C0D0'] + C['C0AF'] + C['C053'] + C['C041'] + C['C098'] + C['C080'] + C['C053'] + C['C0BB'] + C['C08F'] + C['C09B'] + C['C046'] + C['C0AC'] + C['C0AA'] + C['C09F'] + C['C080'] + C['C07F'] + C['C09F'] + C['C08E'] + C['C0C9'] == 1398 ) 
solver.add( C['C05C'] + C['C06D'] + C['C0B8'] + C['C047'] + C['C092'] + C['C09B'] + C['C0C4'] + C['C087'] + C['C0BF'] + C['C0B9'] + C['C0BF'] + C['C049'] + C['C084'] + C['C04E'] + C['C071'] + C['C0B4'] == 1293 ) 
solver.add( C['C0A1'] + C['C06D'] + C['C053'] + C['C098'] + C['C043'] + C['C0A1'] + C['C094'] + C['C069'] + C['C05C'] + C['C04F'] + C['C09A'] + C['C07B'] + C['C095'] == 950 ) 
solver.add( C['C0B9'] + C['C07E'] + C['C044'] + C['C08F'] + C['C05A'] + C['C09E'] + C['C05B'] + C['C0AE'] + C['C0B1'] + C['C042'] + C['C045'] + C['C052'] + C['C056'] + C['C06F'] + C['C0BC'] + C['C04A'] + C['C07F'] + C['C047'] == 1501 ) 
solver.add( C['C058'] + C['C09B'] + C['C0CB'] + C['C0C1'] + C['C071'] + C['C065'] + C['C0AD'] + C['C0C6'] + C['C04C'] + C['C09B'] + C['C091'] == 826 ) 
solver.add( C['C067'] + C['C087'] + C['C0C8'] + C['C05E'] == 291 ) 
solver.add( C['C0C0'] + C['C09E'] + C['C0C4'] == 202 ) 
solver.add( C['C08E'] + C['C052'] + C['C09A'] + C['C0CA'] + C['C08E'] + C['C0CD'] + C['C06F'] + C['C05E'] + C['C0CA'] + C['C082'] + C['C0B5'] + C['C04F'] + C['C090'] + C['C0BE'] + C['C08A'] + C['C0C3'] + C['C0C7'] + C['C0BB'] + C['C0D0'] == 1395 ) 
solver.add( C['C097'] + C['C05A'] + C['C0C1'] + C['C055'] + C['C0A8'] + C['C0A3'] + C['C08B'] + C['C0B7'] + C['C09F'] + C['C07D'] + C['C084'] + C['C075'] + C['C074'] + C['C0A6'] == 1130 ) 
solver.add( C['C064'] + C['C0B1'] + C['C090'] + C['C07E'] + C['C0B8'] + C['C089'] + C['C0B5'] + C['C04D'] + C['C07E'] + C['C078'] == 847 ) 
solver.add( C['C063'] + C['C05D'] + C['C061'] + C['C089'] + C['C08C'] + C['C083'] + C['C057'] + C['C05C'] + C['C0C2'] + C['C0AE'] + C['C0CD'] == 803 ) 
solver.add( C['C08B'] + C['C047'] + C['C072'] + C['C0AA'] == 286 ) 
solver.add( C['C082'] + C['C078'] + C['C05E'] + C['C072'] + C['C04B'] + C['C078'] + C['C06E'] + C['C04C'] == 613 ) 
solver.add( C['C09D'] + C['C064'] + C['C050'] + C['C087'] + C['C0BA'] + C['C0AD'] + C['C098'] + C['C092'] + C['C09E'] + C['C06D'] + C['C0B6'] == 813 ) 
solver.add( C['C0C1'] + C['C091'] + C['C0C5'] + C['C064'] + C['C040'] + C['C06B'] + C['C07A'] + C['C04C'] + C['C0A5'] + C['C045'] + C['C08F'] + C['C045'] + C['C071'] + C['C0CC'] + C['C08B'] + C['C04E'] + C['C088'] + C['C0B9'] + C['C05E'] == 1492 ) 
solver.add( C['C095'] + C['C07E'] + C['C059'] + C['C073'] + C['C082'] + C['C09A'] + C['C061'] + C['C061'] + C['C09E'] + C['C0CA'] + C['C04E'] + C['C041'] + C['C091'] + C['C06C'] + C['C062'] + C['C0AF'] + C['C0CA'] == 1173 ) 
solver.add( C['C04C'] + C['C0AD'] + C['C054'] + C['C096'] + C['C05C'] + C['C0A1'] == 441 ) 
solver.add( C['C0D0'] + C['C069'] + C['C059'] + C['C047'] + C['C0A1'] + C['C059'] + C['C06B'] + C['C0A8'] + C['C085'] + C['C079'] + C['C058'] + C['C0CF'] + C['C065'] + C['C09A'] + C['C0AC'] + C['C046'] + C['C0A1'] + C['C099'] + C['C077'] + C['C096'] == 1514 ) 
solver.add( C['C074'] + C['C05E'] + C['C056'] + C['C061'] + C['C099'] + C['C08C'] + C['C050'] == 519 ) 


if solver.check() == sat:
    model = solver.model()
    for var in C:
        print(f'{model[C[var]]}',end=', ')
else:
    print("No solution found")
```
# Perf  
đếm instruction  
```python= 
from subprocess import Popen, PIPE, STDOUT

# Define the path to perf once
perf_path = "/usr/lib/linux-tools/5.15.0-136-generic/perf"
target_binary = "/home/unix/kjh"

cmd = perf_path +" stat -x, -e instructions:u " +target_binary
key = b''

while True:
    maximum = 0, 0
    for i in range(0x20, 0x7f):
        p = Popen(cmd, stdout=PIPE, stdin=PIPE, stderr=STDOUT, shell=True)
        _input = key + bytes([i])
        stdout, _ = p.communicate(input=_input)
        #print(stdout)
        nb_instructions = int(stdout.split(b"\n")[2].split(b",,")[0].decode())
        if nb_instructions > maximum[0]:
            maximum = nb_instructions, bytes([i])
    key += maximum[1]
    print(key)
```
# mimirev  
1 bài VM từ PWNME QUALS, được giải bằng gdb, không hiểu lắm nhưng vẫn lưu lại  
```
# init
break *0x4BA9E0
run

# create VM
set $rip=0x4BAFBF
break *0x4BAFDA
c

# store the address of the VM
set $v=$rax

# pass the check
set $rip=0x4BA665
set $r8=123456
set $rdx=190703
break *0x4ba728
c

# set the correct values for the hash
set $rax=123456
break *0x4ba749
c
set $rax=190703
break *0x4ba7ae
c

# restore the address of the VM
set $rdx=$v
set $rip=0x4ba7b6

# win
break *0x4BA7D2
c
ni
x/s $rax
```
# Dùng pip trong IDA  
```python=
import pip

def install(package):
    if hasattr(pip, 'main'):
        pip.main(['install', package])
    else:
        pip._internal.main(['install', package])

# Example
if __name__ == '__main__':
    install('z3-solver')
```