Intelligence Service
Files
Download: rev_intelligence_service.zip
Challenge Description
This is a reversing challenge from the HTB Business CTF 2023. The provided binary is a “key checker” that gates access behind a license/activation key, and our job is to recover a valid key.
We’ve received some powerful intelligence gathering software from intercepting Arodor communications. Unfortunately, it requires a license key. Can you try and crack the keychecker?
The key turns out to be a 41-character flag, which makes brute force impractical and points toward static analysis plus a constraint solver.
Recon
The program prompts for an activation key, reads it from stdin, validates it character-by-character against a long chain of arithmetic constraints, and prints success or failure. The main function below shows the overall flow: it reads 0x29 (41) bytes into a buffer and passes it to the validation routine sub_401a70. If that returns zero (no failed checks), the key is accepted.
extern unsigned long long stdin;
int main(unsigned int a0, unsigned long a1)
{
unsigned long v0; // [bp-0x58]
unsigned int v1; // [bp-0x4c]
void* v2; // [bp-0x48]
void* v3; // [bp-0x40]
void* v4; // [bp-0x38]
void* v5; // [bp-0x30]
void* v6; // [bp-0x28]
unsigned short v7; // [bp-0x20]
v1 = a0;
v0 = a1;
v2 = 0;
v3 = 0;
v4 = 0;
v5 = 0;
v6 = 0;
v7 = 0;
printf("Welcome to our premium agency intelligence service!\nTo start using the service, please enter the key provided in the confirmation e-mail.\nActivation Key: ");
fread(&v2, 0x29, 0x1, stdin);
if (!sub_401a70(&v2))
{
puts("[+] Activation key successfully redeemed; Thank you for using our services!");
return 0;
}
puts("[!] Activation key invalid or expired");
return 0;
}
The validation entry point sub_401a70 first loops over the input enforcing that every character is printable ASCII (> 32 and <= 126), then hands off to sub_4012f8, which begins the actual flag checks.
int sub_401a70(char *a0)
{
unsigned int v0; // [bp-0x38]
unsigned int v1; // [bp-0x34]
unsigned long v2; // [bp-0x10]
unsigned long v4; // rbx
unsigned long long v5; // rbx
v2 = v4;
v1 = 0;
v0 = 0;
while (true)
{
v5 = v0;
if (v0 >= strlen(a0))
{
break;
}
if (a0[v0] <= 32 || a0[v0] > 126)
{
v1 = 1;
}
v0 += 1;
}
return sub_4012f8(a0);
}
Understanding the Checks
The flag is 41 characters long, indexed 0 through 40. The first checker (sub_4012f8) validates the wrapper HTB{...}. The comment in the cleaned-up listing makes the intent explicit: it confirms H, T, B, { at the start and the relationship to the closing }.
// This checks HTB{ }
if (v0[0] != 72 || v0[1] - 94 + v0[2] != v0[40] - 69 || v0[0] + v0[2] - 50 != 88 || v0[3] != 123 || v0[1] != 84)
{
v2 += 1;
}
The remaining bytes are spread across a series of nested-if checker functions (sub_4011b6, sub_40140d, sub_4015fd, sub_4014a0, sub_4018cb, sub_40176b). Each function tests a handful of arithmetic relations between flag bytes. A representative one, sub_4011b6, uses left shifts (<<) as multiplications — for example (a0[21] << 1) is a0[21] * 2.
long long sub_4011b6(char a0[38])
{
unsigned long v0; // [bp+0x0]
v0 += 4;
if (a0[9] - 122 - a0[27] == -184)
{
if (a0[16] == 49)
{
if (a0[16] + 60 - a0[37] == -8)
{
if (a0[13] + a0[29] + 50 == 265)
{
if ((a0[21] << 1) + a0[29] == 316)
{
if (a0[9] == 55)
{
if (a0[37] == a0[29] + 5)
{
if ((a0[16] << 1) + a0[29] != 210)
{
return 1;
}
return 0;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
The note on the shift operator semantics, which is the key insight for translating these checks into solver constraints:
<<represents the left shift operator in C/C++. It shifts the binary representation ofxto the left by 3 positions, effectively multiplyingxby 2 raised to the power of 3 (2^3 = 8). In other words, it’s equivalent to multiplyingxby 8.
A few of the simpler standalone constraints, pulled out of the checker bodies:
a0[5] + a0[39] - 40 == 169
a0[7] + a0[25] == 198
(unsigned int)(a0[12] << 2) + a0[12] + a0[30] == 599
a0[22] == 114
And the HTB{...} wrapper conditions in source form:
if (user_input[0] != 'H' || user_input[1] != 'T' || user_input[2] != 'B' || user_input[3] != '{' || user_input[40] != '}')
{
v2 += 1;
}
Full Decompilation (angr / dogbolt)
To collect every constraint, the binary was decompiled (here via dogbolt’s angr backend). This full listing is what the constraints below were transcribed from.
long long sub_401000()
{
return 0;
if (false)
{
return 0();
}
}
long long sub_401020()
{
void* v0; // [bp-0x8]
v0 = 0;
goto *((long long *)4210704);
}
long long sub_401030()
{
void* v0; // [bp-0x8]
v0 = 0;
return sub_401020();
}
long long sub_401040()
{
unsigned long long v0; // [bp-0x8]
v0 = 1;
return sub_401020();
}
long long sub_401050()
{
unsigned long long v0; // [bp-0x8]
v0 = 2;
return sub_401020();
}
long long sub_401060()
{
unsigned long long v0; // [bp-0x8]
v0 = 3;
return sub_401020();
}
long long sub_401070()
{
unsigned long long v0; // [bp-0x8]
v0 = 4;
return sub_401020();
}
extern unsigned long long g_401b92;
long long _start()
{
unsigned long v0; // [bp+0x0], Other Possible Types: unsigned long long
unsigned long v1; // [bp+0x8]
unsigned long long v2; // rsi
unsigned long v3; // rax
unsigned long long v4; // rdx
v2 = v0;
v0 = v3;
__libc_start_main(&g_401b92, v2, &v1, 0x0, 0x0, v4); /* do not return */
}
// No decompilation output for function sub_4010f5
long long sub_401100()
{
unsigned long v1; // rax
return v1;
}
extern char stdin;
int sub_401110()
{
return;
if (false)
{
return;
}
}
long long sub_401131()
{
return 0;
if (false)
{
return 0;
}
}
extern char g_404058;
long long sub_401180()
{
unsigned long v0; // [bp-0x8]
unsigned long v2; // rax
if (!g_404058)
{
v0 = stack_base + 0;
g_404058 = 1;
return sub_401110();
}
return v2;
}
long long sub_4011b0()
{
}
long long sub_4011b6(char a0[38])
{
unsigned long v0; // [bp+0x0]
v0 += 4;
if (a0[9] - 122 - a0[27] == -184)
{
if (a0[16] == 49)
{
if (a0[16] + 60 - a0[37] == -8)
{
if (a0[13] + a0[29] + 50 == 265)
{
if ((a0[21] << 1) + a0[29] == 316)
{
if (a0[9] == 55)
{
if (a0[37] == a0[29] + 5)
{
if ((a0[16] << 1) + a0[29] != 210)
{
return 1;
}
return 0;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
int sub_4012f8(unsigned long long a0)
{
char v0[41]; // [bp-0x30]
char v1; // [bp-0x25]
unsigned int v2; // [bp-0x24]
unsigned long long v3; // [bp-0x20]
unsigned long long v4; // [bp-0x18]
unsigned long v5; // [bp-0x10], Other Possible Types: unsigned long long
unsigned long v6; // [bp+0x0]
unsigned long long v8; // r15
unsigned long v9; // r14
unsigned long long v10; // r14
unsigned long long v11; // rbx
unsigned int v12; // esi
*((unsigned long long *)&v0[0]) = a0;
v2 = 0;
v8 = a0;
v6 += 6;
if (v0[0] != 72 || v0[1] - 94 + v0[2] != v0[40] - 69 || v0[0] + v0[2] - 50 != 88 || v0[3] != 123 || v0[1] != 84)
{
v2 += 1;
}
v5 = v9;
v10 = v2;
v3 = 1102800496;
v4 = 1785159959;
while (true)
{
v5 = v3 - v4;
v1 = v3 != v4;
v3 = v4;
if (!v1)
{
break;
}
v4 = v5;
}
v11 = v3 - 3731729721;
v3 - 3731729721(a0, v12, -3731729721);
return 0;
}
int sub_40140d()
{
int tmp_34; // tmp #34
char v0[38]; // [bp-0x28]
unsigned int v1; // [bp-0x1c]
unsigned long long v2; // [bp+0x0]
unsigned long long v3; // [bp+0x8]
unsigned long v4; // rax
unsigned long v5; // r14
unsigned long long v6; // r14
unsigned long long v11; // rbp
tmp_34 = v4 + v5;
v6 = v2;
v1 = (int)tmp_34 * 2;
if ((v0[21] << 1) + v0[29] == 316)
{
if (v0[9] == 55)
{
if (v0[37] == v0[29] + 5)
{
if ((v0[16] << 1) + v0[29] != 210)
{
v1 += 1;
v11 = v3;
return;
}
v11 = v3;
return;
}
v1 += 1;
v11 = v3;
return;
}
v1 += 1;
v11 = v3;
return;
}
v1 += 1;
v11 = v3;
return;
}
int sub_4014a0(char a0[39])
{
unsigned long v0; // [bp+0x0]
v0 += 8;
if (a0[20] == 95)
{
if (a0[32] + a0[11] - 20 == 132)
{
if (a0[8] == a0[24] * -10 + 1141)
{
if (a0[35] + a0[18] - 50 == 186)
{
if (a0[23] + a0[4] == 97)
{
if (a0[26] + a0[10] - 34 == 127)
{
if (a0[34] + 50 == a0[15] - 49 << 1)
{
if (a0[19] + a0[38] + 253 != 484)
{
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
long long sub_4015fd(char a0[38])
{
unsigned long v0; // [bp-0x28]
unsigned int v1; // [bp-0xc]
unsigned long v17; // r14
unsigned long long v18; // r14
v1 = 0;
if ((a0[21] << 1) + a0[21] << 1 == a0[37] + 495)
{
if (a0[33] + a0[16] == 144)
{
if ((unsigned int)(a0[20] << 2) + a0[11] == 429)
{
if (a0[32] - 52 == a0[8])
{
if ((unsigned int)(a0[18] << 3) - a0[18] + a0[24] == 963)
{
if (((unsigned int)(a0[6] << 2) + a0[6] << 1) + a0[35] == 1064)
{
if (a0[28] + 13 != a0[18])
{
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
int sub_40175c()
{
int tmp_21; // tmp #21
unsigned int v0; // [bp-0x4]
unsigned long long v1; // [bp+0x0]
unsigned long v3; // rax
unsigned long v4; // r14
unsigned long long v5; // r14
unsigned long long v6; // rbp
tmp_21 = v3 + v4;
v5 = v1;
v0 = (int)tmp_21 * 2;
v6 = v1;
return;
}
int sub_40176b(char a0[40])
{
unsigned long v0; // [bp+0x0]
v0 += 6;
if ((unsigned int)(a0[36] << 2) + a0[36] - 50 == a0[17] + 68)
{
if (a0[22] + a0[39] - 40 == 174)
{
if ((unsigned int)(a0[22] << 2) + a0[22] + a0[25] - 10 == 655)
{
if (a0[7] + (unsigned int)(a0[7] << 2) == a0[30] + 466)
{
if (a0[31] + a0[12] + 69 == 289)
{
if (a0[36] + a0[14] + 121 == 264)
{
if ((a0[39] << 1) + a0[39] + a0[17] != 422)
{
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
int sub_4018cb(char a0[40])
{
unsigned long v0; // [bp-0x28]
unsigned int v1; // [bp-0xc]
char v2; // [bp-0x8]
unsigned long v3; // [bp+0x0]
unsigned long long v5; // rbp
unsigned long v24; // r14
unsigned long long v25; // r14
v5 = &v2;
v1 = 0;
v3 += 3;
if (a0[23] == 48)
{
if (a0[4] + 50 == a0[26] - 7)
{
if ((a0[34] << 1) + a0[10] + 83 == 242)
{
if (a0[38] + (unsigned int)(a0[15] << 2) + a0[15] + 20 == 630)
{
if (a0[5] + a0[39] - 40 == 169)
{
if (a0[7] + a0[25] == 198)
{
if ((unsigned int)(a0[12] << 2) + a0[12] + a0[30] == 599)
{
if (a0[22] == 114)
{
if (a0[31] + a0[14] + 70 != 275)
{
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
int sub_401a61()
{
int tmp_21; // tmp #21
unsigned int v0; // [bp-0x4]
unsigned long long v1; // [bp+0x0]
unsigned long v3; // rax
unsigned long v4; // r14
unsigned long long v5; // r14
unsigned long long v6; // rbp
tmp_21 = v3 + v4;
v5 = v1;
v0 = (int)tmp_21 * 2;
v6 = v1;
return;
}
int sub_401a70(char *a0)
{
unsigned int v0; // [bp-0x38]
unsigned int v1; // [bp-0x34]
unsigned long v2; // [bp-0x10]
unsigned long v4; // rbx
unsigned long long v5; // rbx
v2 = v4;
v1 = 0;
v0 = 0;
while (true)
{
v5 = v0;
if (v0 >= strlen(a0))
{
break;
}
if (a0[v0] <= 32 || a0[v0] > 126)
{
v1 = 1;
}
v0 += 1;
}
return sub_4012f8(a0);
}
int sub_401aea()
{
char v0; // [bp-0x48]
char v1; // [bp-0x31]
unsigned int v2; // [bp-0x2c]
unsigned long long v3; // [bp-0x28]
unsigned long long v4; // [bp-0x20]
unsigned long v5; // [bp-0x18]
unsigned long v6; // [bp-0x8]
unsigned int v8; // eax
unsigned long v9; // r14
unsigned long long v10; // rbx
unsigned long long v11; // r15
unsigned int v12; // esi
unsigned long long v13; // r14
v2 = v8;
v2 = v8 * 2;
v6 = v9;
v3 = 3977871074;
v4 = 2678894588;
while (true)
{
v5 = v3 - v4;
v1 = v3 != v4;
v3 = v4;
if (!v1)
{
break;
}
v4 = v5;
}
v10 = v3 - 3401491649;
v2 = (v3 - 3401491649(v11, v12, -3401491649) + v2) * 2;
v6 = v6;
v13 = v2;
sub_4018cb(*((long long *)&v0));
return;
}
int sub_401b7c()
{
unsigned int v0; // [bp-0x2c]
int tmp_27; // tmp #27
unsigned long long v1; // [bp-0x8]
unsigned long long v2; // [bp+0x0]
unsigned long v4; // rax
unsigned long v5; // r14
unsigned long long v6; // r14
unsigned long long v7; // rbx
unsigned long long v8; // rbp
v0 = v4;
tmp_27 = v4 + v5;
v6 = v2;
v0 = (int)tmp_27 * 2;
v7 = v1;
v8 = v2;
return;
}
extern unsigned long long stdin;
int main(unsigned int a0, unsigned long a1)
{
unsigned long v0; // [bp-0x58]
unsigned int v1; // [bp-0x4c]
void* v2; // [bp-0x48]
void* v3; // [bp-0x40]
void* v4; // [bp-0x38]
void* v5; // [bp-0x30]
void* v6; // [bp-0x28]
unsigned short v7; // [bp-0x20]
v1 = a0;
v0 = a1;
v2 = 0;
v3 = 0;
v4 = 0;
v5 = 0;
v6 = 0;
v7 = 0;
printf("Welcome to our premium agency intelligence service!\nTo start using the service, please enter the key provided in the confirmation e-mail.\nActivation Key: ");
fread(&v2, 0x29, 0x1, stdin);
if (!sub_401a70(&v2))
{
puts("[+] Activation key successfully redeemed; Thank you for using our services!");
return 0;
}
puts("[!] Activation key invalid or expired");
return 0;
}
long long sub_401c54()
{
unsigned long v1; // rax
return v1;
}
Solving with z3 (Constraint Solver)
Because each check is a linear arithmetic relation over the byte values, the whole thing reduces to a system of equations. z3 can solve this directly. The first solver script models all 64 bytes as 8-bit bitvectors, constrains each to printable ASCII, then transcribes every condition from the decompiled checkers. A handful of bytes are not pinned by the constraints transcribed into this script, so z3 leaves them free; they are set by hand to the values that make the flag read as words.
from z3 import *
def solve_constraints():
arg1 = [BitVec(f"param_1_{i}", 8) for i in range(0x40)]
s = Solver()
# each element must be a printable ASCII char
for i in range(48):
s.add(arg1[i] >= 32, arg1[i] <= 126)
# Adding all the conditions to the solver
s.add(arg1[0x9] - 0x7a - arg1[0x1b] == 0xffffff48)
s.add(arg1[0x10] == 0x31)
s.add(arg1[0x10] + 0x3c - arg1[0x25] == 0xfffffff8)
s.add(arg1[0xd] + arg1[0x1d] + 0x32 == 0x109)
s.add(arg1[0x15] * 2 + arg1[0x1d] == 0x13c)
s.add(arg1[0x9] == 0x37)
s.add(arg1[0x25] == arg1[0x1d] + 5)
s.add(arg1[0x10] * 2 + arg1[0x1d] == 0xd2)
s.add(arg1[0] + arg1[2] - 0x32 == ord('X'))
s.add(arg1[0] == ord('H'))
s.add(arg1[1] == ord('T'))
s.add(arg1[1] - 0x5e + arg1[2] == arg1[0x28] - 0x45)
s.add(arg1[3] == ord('{'))
s.add(arg1[0x17] == ord('0'))
s.add(arg1[4] + 0x32 == arg1[0x1a] - 7)
s.add(arg1[0x22]*2 + arg1[0xa] + 0x53 == 0xf2)
s.add(arg1[0x26] + arg1[0xf]*5 + 0x14 == 0x276)
s.add(arg1[5] + arg1[0x27] - 0x28 == 0xa9)
s.add(arg1[7] + arg1[0x19] == 0xc6)
s.add(arg1[0xc]*5 + arg1[0x1e] == 0x257)
s.add(arg1[0x16] == ord('r'))
s.add(arg1[0x1f] + arg1[0xe] + 0x46 == 0x113)
s.add(arg1[0x24]*5 - 0x32 == arg1[0x11] + 0x44)
s.add(arg1[0x16] + arg1[0x27] - 0x28 == 0xae)
s.add(arg1[0x16]*5 + arg1[0x19] - 0xa == 0x28f)
s.add(arg1[7]*5 == arg1[0x1e] + 0x1d2)
s.add(arg1[0x1f] + arg1[0xc] + 0x45 == 0x121)
s.add(arg1[0x24] + arg1[0xe] + 0x79 == 0x108)
s.add(arg1[0x27]*3 + arg1[0x11] == 0x1a6)
s.add(arg1[0x14] == 0x5f)
s.add(arg1[0x20] + (arg1[0xb] - 0x14) == 0x84)
s.add(arg1[8] == (arg1[0x18] * 0xfffffff6) + 0x475)
s.add(arg1[0x23] + (arg1[0x12] - 0x32) == 0xba)
s.add(arg1[0x17] + arg1[4] == 0x61)
s.add(arg1[0x1a] + (arg1[0xa] - 0x22) == 0x7f)
rax_52 = arg1[0xf] - 0x31
s.add((arg1[0x22] + 0x32) == (rax_52 + rax_52))
s.add((arg1[0x13] + arg1[0x26] + 0xfd) == 0x1e4)
# These indices aren't pinned by the constraints transcribed above, so z3
# leaves them free; set them by hand to the values that make the flag read as words
s.add(arg1[18] == ord('z'))
s.add(arg1[24] == ord('m'))
s.add(arg1[28] == ord('m'))
s.add(arg1[33] == ord('_'))
s.add(arg1[32] == ord('g'))
if s.check() == sat:
m = s.model()
solution = [m[arg1[i]] for i in range(0x40)]
print("".join([chr(int(str(i))) for i in solution if i != None]))
print(f"Solution: {solution}")
else:
print("Unsatisfiable")
if __name__ == "__main__":
solve_constraints()
Post-Solve: Annotated Decompilation
With the solution recovered, plugging the byte values back into the checkers makes the decompilation much more readable. Each comparison now resolves to a concrete character, confirming the per-index assignments. This annotated re-decompilation makes the structure of every checker obvious.
long long sub_401000()
{
return 0;
if (false)
{
return 0();
}
}
long long sub_401020()
{
void* v0; // [bp-0x8]
v0 = 0;
goto *((long long *)4210704);
}
long long sub_401030()
{
void* v0; // [bp-0x8]
v0 = 0;
return sub_401020();
}
long long sub_401040()
{
unsigned long long v0; // [bp-0x8]
v0 = 1;
return sub_401020();
}
long long sub_401050()
{
unsigned long long v0; // [bp-0x8]
v0 = 2;
return sub_401020();
}
long long sub_401060()
{
unsigned long long v0; // [bp-0x8]
v0 = 3;
return sub_401020();
}
long long sub_401070()
{
unsigned long long v0; // [bp-0x8]
v0 = 4;
return sub_401020();
}
extern unsigned long long g_401b92;
long long _start()
{
unsigned long v0; // [bp+0x0], Other Possible Types: unsigned long long
unsigned long v1; // [bp+0x8]
unsigned long long v2; // rsi
unsigned long v3; // rax
unsigned long long v4; // rdx
v2 = v0;
v0 = v3;
__libc_start_main(&g_401b92, v2, &v1, 0x0, 0x0, v4); /* do not return */
}
// No decompilation output for function sub_4010f5
long long sub_401100()
{
unsigned long v1; // rax
return v1;
}
extern char stdin;
int sub_401110()
{
return;
if (false)
{
return;
}
}
long long sub_401131()
{
return 0;
if (false)
{
return 0;
}
}
extern char g_404058;
long long sub_401180()
{
unsigned long v0; // [bp-0x8]
unsigned long v2; // rax
if (!g_404058)
{
v0 = stack_base + 0;
g_404058 = 1;
return sub_401110();
}
return v2;
}
long long sub_4011b0()
{
}
long long sub_4011b6(char a0[38])
{
unsigned long v0; // [bp+0x0]
v0 += 4;
if (a0[27] == 'u')
{
if (a0[16] == '1')
{
if (a0[37] == 'u')
{
if (a0[13] + 'p' + 50 == 265)
{
if (a0[21] == 'f')
{
if (a0[9] == '7')
{
if ('u' == 'p' + 5)
{
if (a0[29] == 'p')
{
return 1;
}
return 0;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
return 1;
}
int sub_4012f8(unsigned long long a0)
{
char v0[41]; // [bp-0x30]
char v1; // [bp-0x25]
unsigned int v2; // [bp-0x24]
unsigned long long v3; // [bp-0x20]
unsigned long long v4; // [bp-0x18]
unsigned long v5; // [bp-0x10], Other Possible Types: unsigned long long
unsigned long v6; // [bp+0x0]
unsigned long long v8; // r15
unsigned long v9; // r14
unsigned long long v10; // r14
unsigned long long v11; // rbx
unsigned int v12; // esi
*((unsigned long long *)&v0[0]) = a0;
v2 = 0;
v8 = a0;
v6 += 6;
// This checks HTB{ }
if (v0[0] != 72 || v0[1] - 94 + v0[2] != v0[40] - 69 || v0[0] + v0[2] - 50 != 88 || v0[3] != 123 || v0[1] != 84)
{
v2 += 1;
}
v5 = v9;
v10 = v2;
v3 = 1102800496;
v4 = 1785159959;
while (true)
{
v5 = v3 - v4;
v1 = v3 != v4;
v3 = v4;
if (!v1)
{
break;
}
v4 = v5;
}
v11 = v3 - 3731729721;
v3 - 3731729721(a0, v12, -3731729721);
return 0;
}
int sub_40140d()
{
int tmp_34; // tmp #34
char v0[38]; // [bp-0x28]
unsigned int v1; // [bp-0x1c]
unsigned long long v2; // [bp+0x0]
unsigned long long v3; // [bp+0x8]
unsigned long v4; // rax
unsigned long v5; // r14
unsigned long long v6; // r14
unsigned long long v11; // rbp
tmp_34 = v4 + v5;
v6 = v2;
v1 = (int)tmp_34 * 2;
if ((v0[21] << 1) + v0[29] == 316)
{
if (v0[9] == 55)
{
if (v0[37] == v0[29] + 5)
{
if ((v0[16] << 1) + v0[29] != 210)
{
v1 += 1;
v11 = v3;
return;
}
v11 = v3;
return;
}
v1 += 1;
v11 = v3;
return;
}
v1 += 1;
v11 = v3;
return;
}
v1 += 1;
v11 = v3;
return;
}
int sub_4014a0(char 'd')
{
unsigned long v0; // [bp+0x0]
v0 += 8;
if (a0[20] == '_')
{
if (a0[32] == 'g')
{
if (a0[24] == 'm')
{
if (a0[35] == 'r')
{
if (a0[4] == '1')
{
if (a0[10] == '7')
{
if (a0[15] == 'd')
{
if (a0[19] == 'y')
{
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
long long sub_4015fd(char a0[38])
{
unsigned long v0; // [bp-0x28]
unsigned int v1; // [bp-0xc]
unsigned long v17; // r14
unsigned long long v18; // r14
v1 = 0;
if ((a0[21] << 1) + a0[21] << 1 == 'u' + 495)
{
if ("_" == a0[33])
{
if ('1' == a0[11])
{
if ('3' == a0[8])
{
if ('z' == a0[18])
{
if (((unsigned int)(a0[6] << 2) + a0[6] << 1) + 'r' == 1064)
{
if (a0[28] == 'm') // != ...
{
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
v1 += 1;
v0 = v17;
v18 = v1;
sub_4014a0(a0);
return 0;
}
int sub_40175c()
{
int tmp_21; // tmp #21
unsigned int v0; // [bp-0x4]
unsigned long long v1; // [bp+0x0]
unsigned long v3; // rax
unsigned long v4; // r14
unsigned long long v5; // r14
unsigned long long v6; // rbp
tmp_21 = v3 + v4;
v5 = v1;
v0 = (int)tmp_21 * 2;
v6 = v1;
return;
}
int sub_40176b(char a0[40])
{
unsigned long v0; // [bp+0x0]
v0 += 6;
if (a0[36] == '0')
{
if (a0[39] == 'd')
{
if (a0[25] = "_")
{
if (a0[30] == "1")
{
if (a0[31] == "n")
{
if (a0[14] == "_")
{
if (a0[17] != "z")
{
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
return;
}
int sub_4018cb(char a0[40])
{
unsigned long v0; // [bp-0x28]
unsigned int v1; // [bp-0xc]
char v2; // [bp-0x8]
unsigned long v3; // [bp+0x0]
unsigned long long v5; // rbp
unsigned long v24; // r14
unsigned long long v25; // r14
v5 = &v2;
v1 = 0;
v3 += 3;
if (a0[23] == '0')
{
if (a0[26] == 'j')
{
if (a0[34] == '4')
{
if (a0[38] == 'n')
{
if (a0[5] == 'm')
{
if (a0[25] == '_')
{
if (a0[12] == "n")
{
if (a0[22] == "r")
{
if (a0[14] == "_")
{
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
v1 += 1;
v0 = v24;
v25 = v1;
sub_40176b(a0);
return;
}
int sub_401a61()
{
int tmp_21; // tmp #21
unsigned int v0; // [bp-0x4]
unsigned long long v1; // [bp+0x0]
unsigned long v3; // rax
unsigned long v4; // r14
unsigned long long v5; // r14
unsigned long long v6; // rbp
tmp_21 = v3 + v4;
v5 = v1;
v0 = (int)tmp_21 * 2;
v6 = v1;
return;
}
int sub_401a70(char *a0)
{
unsigned int v0; // [bp-0x38]
unsigned int v1; // [bp-0x34]
unsigned long v2; // [bp-0x10]
unsigned long v4; // rbx
unsigned long long v5; // rbx
v2 = v4;
v1 = 0;
v0 = 0;
while (true)
{
v5 = v0;
if (v0 >= strlen(a0))
{
break;
}
if (a0[v0] <= 32 || a0[v0] > 126)
{
v1 = 1;
}
v0 += 1;
}
return sub_4012f8(a0);
}
int sub_401aea()
{
char v0; // [bp-0x48]
char v1; // [bp-0x31]
unsigned int v2; // [bp-0x2c]
unsigned long long v3; // [bp-0x28]
unsigned long long v4; // [bp-0x20]
unsigned long v5; // [bp-0x18]
unsigned long v6; // [bp-0x8]
unsigned int v8; // eax
unsigned long v9; // r14
unsigned long long v10; // rbx
unsigned long long v11; // r15
unsigned int v12; // esi
unsigned long long v13; // r14
v2 = v8;
v2 = v8 * 2;
v6 = v9;
v3 = 3977871074;
v4 = 2678894588;
while (true)
{
v5 = v3 - v4;
v1 = v3 != v4;
v3 = v4;
if (!v1)
{
break;
}
v4 = v5;
}
v10 = v3 - 3401491649;
v2 = (v3 - 3401491649(v11, v12, -3401491649) + v2) * 2;
v6 = v6;
v13 = v2;
sub_4018cb(*((long long *)&v0));
return;
}
int sub_401b7c()
{
unsigned int v0; // [bp-0x2c]
int tmp_27; // tmp #27
unsigned long long v1; // [bp-0x8]
unsigned long long v2; // [bp+0x0]
unsigned long v4; // rax
unsigned long v5; // r14
unsigned long long v6; // r14
unsigned long long v7; // rbx
unsigned long long v8; // rbp
v0 = v4;
tmp_27 = v4 + v5;
v6 = v2;
v0 = (int)tmp_27 * 2;
v7 = v1;
v8 = v2;
return;
}
extern unsigned long long stdin;
int main(unsigned int a0, unsigned long a1)
{
unsigned long v0; // [bp-0x58]
unsigned int v1; // [bp-0x4c]
void* v2; // [bp-0x48]
void* v3; // [bp-0x40]
void* v4; // [bp-0x38]
void* v5; // [bp-0x30]
void* v6; // [bp-0x28]
unsigned short v7; // [bp-0x20]
v1 = a0;
v0 = a1;
v2 = 0;
v3 = 0;
v4 = 0;
v5 = 0;
v6 = 0;
v7 = 0;
printf("Welcome to our premium agency intelligence service!\nTo start using the service, please enter the key provided in the confirmation e-mail.\nActivation Key: ");
fread(&v2, 0x29, 0x1, stdin);
if (!sub_401a70(&v2))
{
puts("[+] Activation key successfully redeemed; Thank you for using our services!");
return 0;
}
puts("[!] Activation key invalid or expired");
return 0;
}
long long sub_401c54()
{
unsigned long v1; // rax
return v1;
}
Alternative: angr Symbolic Execution
Instead of transcribing constraints by hand, angr can symbolically execute the binary and find an input that reaches the success path. This script marks stdin as a 41-byte symbolic password, pins the bytes that are already known, constrains the rest to the alphanumeric/underscore charset, and explores until it reaches the address of the correct-password branch.
import angr
import claripy
def is_alphanum(c):
# This function checks if a character is alphanumeric or _
return claripy.Or(
claripy.And(c >= ord("a"), c <= ord("z")),
claripy.And(c >= ord("A"), c <= ord("Z")),
claripy.And(c >= ord("0"), c <= ord("9")),
c == ord("_"),
)
proj = angr.Project("./service", auto_load_libs=False)
# Create a symbolic bitvector for the password
password = claripy.BVS("password", 8 * 41)
state = proj.factory.entry_state(stdin=password)
# Known characters in the password
known_chars = {
0: "H",
1: "T",
2: "B",
3: "{",
9: "7",
16: "1",
21: "f",
32: "p",
40: "}",
}
# Add constraints for the known characters
for i, c in known_chars.items():
state.solver.add(password.get_byte(i) == ord(c))
# Add constraints for alphanumeric characters
for i in range(4, 39):
if i not in known_chars:
state.solver.add(is_alphanum(password.get_byte(i)))
simgr = proj.factory.simgr(state)
# Explore the state space until we find the address of the correct password check
simgr.explore(find=0x401C26)
if len(simgr.found) > 0:
found = simgr.found[0]
solution = found.solver.eval(password, cast_to=bytes)
print(f"Password: {solution}")
else:
print("No solution found!")
Alternative z3 Scripts
The same idea was also written up as a couple of standalone z3 scripts grouping the constraints by the checker function they came from. The first uses integer variables s0..s40 with comments mapping each block back to its address (0x4011b6, 0x40140d, 0x401601, 0x4014a4, 0x4018cb, 0x40176b).
#!/usr/bin/env python3
from z3 import *
s0 = Int('s0')
s1 = Int('s1')
s2 = Int('s2')
s3 = Int('s3')
s4 = Int('s4')
s5 = Int('s5')
s6 = Int('s6')
s7 = Int('s7')
s8 = Int('s8')
s9 = Int('s9')
s10 = Int('s1O')
s11 = Int('s11')
s12 = Int('s12')
s13 = Int('s13')
s14 = Int('s14')
s15 = Int('s15')
s16 = Int('s16')
s17 = Int('s17')
s18 = Int('s18')
s19 = Int('s19')
s20 = Int('s20')
s21 = Int('s21')
s22 = Int('s22')
s23 = Int('s23')
s24 = Int('s24')
s25 = Int('s25')
s26 = Int('s26')
s27 = Int('s27')
s28 = Int('s28')
s29 = Int('s29')
s30 = Int('s30')
s31 = Int('s31')
s32 = Int('s32')
s33 = Int('s33')
s34 = Int('s34')
s35 = Int('s35')
s36 = Int('s36')
s37 = Int('s37')
s38 = Int('s38')
s39 = Int('s39')
s40 = Int('s40')
s = z3.Solver()
## part 1
s.add(((s2 - 0x32) + s0) == 0x58)
s.add(s0 == ord('H'))
s.add(s1 == ord('T'))
s.add(((s1 - 0x5e) + s2) == (s40-0x45))
s.add(s3 == ord('{'))
## part 2 - 0x4011b6
s.add(((s9 - 0x7a) - s27) == -184)
s.add(s16 == 0x31)
s.add(((s16 + 0x3c) - s37) == -8)
s.add(s13 + (s29 + 0x32) == 0x109)
s.add((s21 + s21) + s29 == 0x13c)
s.add(s9 == 0x37)
s.add(s37 == (s29 + 5))
s.add(((s16 + s16) + s29) == 0xd2)
# part 3 - 40140d
s.add(((s21 + s21) + s29) == 0x13c)
s.add(s9 == 0x37)
s.add(s37 == (s29 + 5))
s.add(((s16 + s16) + s29) == 0xd2)
# part 4 - 401601
s.add(((s21 + s21 + s21) + (s21 + s21 + s21)) == (s37 + 0x1ef))
s.add(s33 + s16 == 0x90)
s.add(((s20 * 4) + s11) == 0x1ad) # *4 => shl eax,2
s.add((s32 - 0x34) == s8)
s.add((((s18 * 8) - s18) + s24) == 0x3c3) # *8 => shl eax,3
s.add(((((s6 * 4) + s6) * 2) + s35) == 0x428) # *4 => shl eax,2
s.add((s28 + 13) == s18)
#part 5 - 4014A4
s.add(s20 == 0x5f)
s.add((s32 + (s11 - 0x14)) == 0x84)
s.add(s8 == ((s24 * -10) + 0x475))
s.add((s35 + (s18 - 0x32)) == 0xba)
s.add(s23 + s4 == 0x61)
s.add((s26 + (s10 - 0x22)) == 0x7f)
s.add((s34 + 0x32) == ((s15 - 0x31) + (s15 - 0x31)))
s.add(s19 + (s38 + 0xfd) == 0x1e4)
# part 6 - 04018cb
s.add(s23 == 0x30)
s.add(((s4 + 0x32) == s26 - 7))
s.add(((s34 + s34) + (s10 + 0x53)) == 0xf2)
s.add((s38 + (((s15 * 4) + s15) + 0x14)) == 0x276) # *4 => shl eax,2
s.add((s5 + (s39 - 0x28)) == 0xa9)
s.add(s7 + s25 == 0xc6)
s.add((((s12 * 4) + s12) + s30) == 0x257) # *4 => shl eax,2
s.add(s22 == 0x72)
s.add((s31 + (s14 + 0x46)) == 0x113)
# part 7 - 40176b
s.add((((s36 * 4) + s36) - 0x32) == (s17 + 0x44)) # *4 => shl eax,2
s.add((s22 + (s39 - 0x28) == 0xae))
s.add((((s22 * 4) + s22) + (s25 - 0xa)) == 0x28f) # *4 => shl eax,2
s.add((s7 + (s7 * 4)) == (s30 + 0x1d2)) # *4 => shl eax,2
s.add((s31 + (s12 + 0x45)) == 0x121)
s.add((s36 + (s14 + 0x79)) == 0x108)
s.add((((s39 + s39) + s39) + s17) == 0x1a6)
if s.check():
m = s.model()
serial = [
chr(m[s0].as_long()) if m[s0] != None else 'A',
chr(m[s1].as_long()) if m[s0] != None else 'A',
chr(m[s2].as_long()) if m[s0] != None else 'A',
chr(m[s3].as_long()) if m[s3] != None else 'A',
chr(m[s4].as_long()) if m[s4] != None else 'A',
chr(m[s5].as_long()) if m[s5] != None else 'A',
chr(m[s6].as_long()) if m[s6] != None else 'A',
chr(m[s7].as_long()) if m[s7] != None else 'A',
chr(m[s8].as_long()) if m[s8] != None else 'A',
chr(m[s9].as_long()) if m[s9] != None else 'A',
chr(m[s10].as_long()) if m[s10] != None else 'A',
chr(m[s11].as_long()) if m[s11] != None else 'A',
chr(m[s12].as_long()) if m[s12] != None else 'A',
chr(m[s13].as_long()) if m[s13] != None else 'A',
chr(m[s14].as_long()) if m[s14] != None else 'A',
chr(m[s15].as_long()) if m[s15] != None else 'A',
chr(m[s16].as_long()) if m[s16] != None else 'A',
chr(m[s17].as_long()) if m[s17] != None else 'A',
chr(m[s18].as_long()) if m[s18] != None else 'A',
chr(m[s19].as_long()) if m[s19] != None else 'A',
chr(m[s20].as_long()) if m[s20] != None else 'A',
chr(m[s21].as_long()) if m[s21] != None else 'A',
chr(m[s22].as_long()) if m[s22] != None else 'A',
chr(m[s23].as_long()) if m[s23] != None else 'A',
chr(m[s24].as_long()) if m[s24] != None else 'A',
chr(m[s25].as_long()) if m[s25] != None else 'A',
chr(m[s26].as_long()) if m[s26] != None else 'A',
chr(m[s27].as_long()) if m[s27] != None else 'A',
chr(m[s28].as_long()) if m[s28] != None else 'A',
chr(m[s29].as_long()) if m[s29] != None else 'A',
chr(m[s30].as_long()) if m[s30] != None else 'A',
chr(m[s31].as_long()) if m[s31] != None else 'A',
chr(m[s32].as_long()) if m[s32] != None else 'A',
chr(m[s33].as_long()) if m[s33] != None else 'A',
chr(m[s34].as_long()) if m[s34] != None else 'A',
chr(m[s35].as_long()) if m[s35] != None else 'A',
chr(m[s36].as_long()) if m[s36] != None else 'A',
chr(m[s37].as_long()) if m[s37] != None else 'A',
chr(m[s38].as_long()) if m[s38] != None else 'A',
chr(m[s39].as_long()) if m[s39] != None else 'A',
chr(m[s40].as_long()) if m[s40] != None else 'A',
]
serial_final = "".join(serial)
print("%s => size : 0x%x" % (serial_final, len(serial_final)))
The cleanest version reads the flag length from a flag import, builds one bitvector per character, applies every constraint, and asserts the recovered string matches the flag.
from z3 import *
from flag import flag
x = [BitVec(f"x{i}", 8) for i in range(len(flag)) ]
s = Solver()
for i in range(len(flag)):
s.add(x[i] > 32)
s.add(x[i] < 127)
s.add(x[2] - 50 + x[0] == 88 )
s.add(x[0] + 20 == 92)
s.add(50 + x[1] == 134)
s.add(x[1] - 94 + x[2] == x[40] - 69)
s.add(-55 + x[3] == 68)
s.add(x[9] - 122 - x[27] == -184)
s.add(x[16] - 7 == 42)
s.add(x[16] + 60 - x[37] + 7 == -1)
s.add(50 + x[29] + x[13] - 10 == 255)
s.add(x[29] + 2*x[21] + 70 == 386)
s.add(-5 == x[9] - 60)
s.add(x[37] + 65 == x[29] + 70)
s.add(x[29] + 2*x[16] + 70 == 280)
s.add(50 + 6*x[21] == 545 + x[37])
s.add(x[16] + x[33] == 144)
s.add(x[11] + 4*x[20] == 429)
s.add(-72 + x[32] + 5 == x[8] - 15)
s.add(x[24] + 7*x[18] == 963)
s.add(x[35] + 10 * x[6] == 1064)
s.add(x[28] + 65 == 52 + x[18])
s.add(x[20] - 50 == 45)
s.add(x[11] - 20 + x[32] == 132)
s.add(x[8] + 52 == 1193 - 10 * x[24])
s.add(-50 + x[18] + x[35] == 186)
s.add(x[4] + x[23] == 97)
s.add(x[10] - 34 + x[26] + 60 == 187)
s.add(x[34] + 50 == -98 + 2*x[15])
s.add(x[38] + 253 + x[19] == 484)
s.add(x[23] - 10 == 38)
s.add(x[4] + 50 == -7 + x[26])
s.add(x[10] + 83 + 2 * x[34] == 242)
s.add(5 * x[15] + 20 + x[38] - 40 == 590)
s.add(x[39] - 40 + x[5] == 169)
s.add(x[25] + x[7] + 6 == 204)
s.add(x[30] + 5 * x[12] + 50 == 649)
s.add(2 * x[22] + 76 == 304)
s.add(-10 + x[14] + 80 + x[31] == 275)
s.add(5*x[36] - 50 == 68 + x[17])
s.add(x[39] - 40 + x[22] == 174)
s.add(-10 + x[25] + 5 * x[22] == 655)
s.add(5 * x[7] + 243 == 709 + x[30])
s.add(x[12] + 69 + x[31] == 289)
s.add(x[14] + 121 + x[36] == 264)
s.add(x[17] + 3*x[39] == 422)
if s.check() == sat:
m = s.model()
s = ''
for i in range(len(flag)):
s += chr(m[x[i]].as_long())
print(f'Found Solution: {s}')
assert s == flag
else:
print('Unsat :(')
Flag
Reassembling the per-index byte values recovered by the solver gives the 41-character activation key. The full character map:
0 = 'H'
1 = 'T' = 84
2 = 'B'
3 = '{'
4 = '1'
5 = 'm'
6 = '_'
7 = 'g'
8 = '3'
9 = '7'
10 = '7'
11 = '1'
12 = 'n'
13 = 'g'
14 = '_'
15 = 'd'
16 = '1'
17 = 'z'
18 = 'z'
19 = 'y'
20 = '_'
21 = 'f'
22 = 'r'
23 = '0'
24 = 'm'
25 = '_'
26 = 'j'
27 = 'u'
28 = 'm'
29 = 'p'
30 = '1'
31 = 'n'
32 = 'g'
33 = '_'
34 = '4'
35 = 'r'
36 = '0'
37 = 'u'
38 = 'n'
39 = 'd'
40 = '}'
Concatenated, this is the flag:
HTB{1m_g3771ng_d1zzy_fr0m_jump1ng_4r0und}