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:
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')
```
Sign in with Wallet
Connect another wallet