[HITCON CTF 2023 Quals] LessEQualmore

lessequalmore

33 solves

I did play this ctf as team 프로그램털모찌.

It was about 7 am for me in korea when I solved this.

I spent the night with no sleep. Then I fell asleep right after I solved this.

I realized that.. guys, try to sleep at the appropriate time, or you gon miss upcoming challenges.

When I opened my eyes, there was already "subformore" released long time ago :(

(this is why I could only give an aaw primitive function to a skilled pwner, not aaw and aar both...but he solved it lol)

 

chal.txt:

0 0 1070 0 0 0 0 0 1023 0 -1 1 16 1040 16777216 -16777216 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 16774200 1411 16776275 3646 1532 6451 2510 16777141 16775256 2061 16776706 2260 2107 6124 878 16776140 16775299 1374 16776956 2212 1577 4993
1351 16777040 16774665 1498 16776379 3062 1593 5966 1924 16776815 16774318 851 16775763 3663 711 5193 2591 16777069 16774005 1189 16776283 3892 1372 6362 2910 307 16775169 1031 16776798 2426
1171 4570 1728 33 16775201 819 16776898 2370 1132 4255 1900 347 42 42 42 32 70 108 97 103 32 67 104 101 99 107 101 114 32 42
42 42 0 89 111 117 32 101 110 116 101 114 101 100 58 0 67 111 110 103 114 97 116 115 33 32 89 111 117 32
103 111 116 32 116 104 101 32 102 108 97 103 33 0 83 111 114 114 121 44 32 119 114 111 110 103 32 102 108 97
103 33 0 228 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
...

lessequalmore:

int __cdecl main(int argc, const char **argv, const char **envp)
{
  init_buf();
  init_mem();
  if ( argc == 2 )
  {
    read_program(argv[1]);
    run_program();
    return 0;
  }
  else
  {
    puts("usage: ./lessequalmore <file>");
    return 1;
  }
}

_QWORD *init_mem()
{
  _QWORD *result; // rax

  result = malloc(0x80000uLL);
  mem = result;
  return result;
}

void run_program()
{
  int i; // [rsp+Ch] [rbp-4h]

  i = 0;
  while ( i >= 0 )
  {
    op1(mem[i], mem[i + 1]);
    if ( op2(mem[i + 1]) )
      i = toint(mem[i + 2]);
    else
      i += 3;
  }
}

int __fastcall op1(__int64 idx1, __int64 idx2)
{
  _QWORD *mem_; // rbx
  __int64 print_bignum_to_char; // rax
  __int64 bignum_neg_mem_idx2; // rax
  _QWORD *mem___; // rbx
  __int64 *mem_idx2_; // r12
  _QWORD *mem__; // rbx
  __int64 *mem_idx2; // rbx
  __int64 bignum; // [rsp+18h] [rbp-28h]

  toint(idx1);
  toint(idx2);
  if ( is_negative(idx1) )
  {
    bignum = get_bignum();                      // %x(hexnum) or %(decimal)
  }
  else
  {
    mem_ = mem;
    bignum = mem_[toint(idx1)];
  }
  if ( is_negative(idx2) )
  {
    print_bignum_to_char = toint(bignum);
    LODWORD(bignum_neg_mem_idx2) = printf("%c", print_bignum_to_char);
  }
  else
  {
    mem___ = mem;
    mem_idx2_ = &mem___[toint(idx2)];
    mem__ = mem;
    mem_idx2 = &mem__[toint(idx2)];
    bignum_neg_mem_idx2 = bignum_sub(bignum, *mem_idx2_);
    *mem_idx2 = bignum_neg_mem_idx2;
  }
  return bignum_neg_mem_idx2;
}

_BOOL8 __fastcall op2(__int64 idx_)
{
  _QWORD *mem_; // rbx
  __int64 idx; // rax

  mem_ = mem;
  idx = toint(idx_);
  return toint(mem_[idx]) <= 0;
}

__int64 __fastcall bignum_sub(__int64 a1, __int64 a2)
{
  return a2 - a1;
}

It reads a file like chal.txt and store the integers in mem.

The first 2 integers and the third integer are interpreted as operators and jump index of mem inside while loop.

 

__int64 get_bignum()
{
  char getch; // [rsp+7h] [rbp-9h]
  char getch2; // [rsp+7h] [rbp-9h]
  _BYTE tmp[9]; // [rsp+7h] [rbp-9h]

  getch = getchar();
  if ( getch != '%' )
  {
    *(_QWORD *)&tmp[1] = getch;
    return -*(_QWORD *)&tmp[1];
  }
  getch2 = getchar();
  if ( getch2 == 'x' )                          // hex
  {
    tmp[8] = 0;
    *(_QWORD *)tmp = (unsigned __int8)getchar();
    while ( tmp[0] != '\n' )
    {
      *(_QWORD *)&tmp[1] *= 16LL;
      if ( tmp[0] <= '@' || tmp[0] > 'F' )
      {
        if ( tmp[0] <= '`' || tmp[0] > 'f' )
          *(_QWORD *)&tmp[1] += tmp[0] - '0';
        else
          *(_QWORD *)&tmp[1] += tmp[0] - 'W';
      }
      else
      {
        *(_QWORD *)&tmp[1] += tmp[0] - '7';
      }
      tmp[0] = getchar();
    }
  }
  else
  {
    if ( getch2 > 'x' )
      goto hell;
    if ( getch2 == '%' )
    {
      *(_QWORD *)&tmp[1] = getch2;
      return -*(_QWORD *)&tmp[1];
    }
    if ( getch2 < '%' || getch2 - (unsigned int)'0' > 9 )
    {                                           // decimal
hell:
      *(_QWORD *)&tmp[1] = getch2;
      return -*(_QWORD *)&tmp[1];
    }
    *(_QWORD *)&tmp[1] = getch2 - '0';
    for ( tmp[0] = getchar(); tmp[0] != '\n'; tmp[0] = getchar() )
      *(_QWORD *)&tmp[1] = 10LL * *(_QWORD *)&tmp[1] + tmp[0] - '0';
  }
  return -*(_QWORD *)&tmp[1];
}

It reads input like this. It just calls getchar and interprets characters as hex and decimal.

 

wrong flag

The integers inside chal.txt are the instructions that read input numbers and check if it is a valid flag.

 

I made a python script same with this binary implementation.

Then I printed out the vm instructions.

 

important vm instructions

I found out that input integers are calculated in some way and the flow goes to op2 function to check if the resultant integer of that calculation is correct.

If it isn't correct, it goes to index 3317 of mem. (where the instructions that print out "Sorry blah blah.." are located)

So, in my python script, I made the second mem for z3 values to track the inputs and I forced the op2 function to return True if the type of  parameter in mem_z3 is z3.z3.ArithRef not to jump to 3317.

When the program ends with success message, make another python script to run z3 solver to calculate flag using z3.z3.ArithRef expressions that triggered force-return-True in op2. (the length of input integers is 64 which can be figured out using success message)

I executed solve.py, then I got flag.

 

got flag

import sys
from time import sleep
from z3 import *
from pwn import pause
with open('./chal.txt', 'rt') as f:
    mem = [int(i) for i in f.read().split()]
mem_z3 = mem.copy()
input_z3 = list(b'hitcon{') + [Int('input[%d]'%i) for i in range(8 * 7 + 1)]
input_z3.append(-10)

input_int = []
for i in [ord(j) for j in 'hitcon{H'+'ABCDEFGH' * 7]:
    input_int.append(i)
input_int.append(10)

def is_negative(a1):
    return (a1 >> 0x3f) & 0xff

def get_bignum():
    return -input_int.pop(0)

z3_idx = 0
str_to_print = ''
def op1(idx1, idx2):
    global str_to_print, z3_idx, mem, mem_z3
    #print(idx1, idx2)
    if is_negative(idx1) != 0:
        bignum = get_bignum()
        bignum_z3 = -1*input_z3[z3_idx]
        z3_idx += 1
        #print(f'    bignum = get_bignum() ({bignum}) ({bignum_z3})')
    else:
        #print(f'    bignum = mem[{idx1}] ({mem[idx1]}) ({mem_z3[idx1]})')
        bignum = mem[idx1]
        bignum_z3 = mem_z3[idx1]
    if is_negative(idx2) != 0:
        #print(f'    print {chr(bignum)} ({bignum_z3})')
        str_to_print += chr(bignum&0x7f)
    else:
        #print(f'    mem[{idx2}] -= {bignum} ({mem[idx2]} -> {mem[idx2] - bignum})')
        mem[idx2] -= bignum
        mem_z3[idx2] -= bignum_z3
        if type(mem_z3[idx2]) != int:
            #print(mem_z3[idx2], simplify(mem_z3[idx2]))
            mem_z3[idx2] = simplify(mem_z3[idx2])
        #print(f'    ({mem[idx2]} -> {mem[idx2] - bignum})')
z3_list = []
z3_hit_list_for_solver = []
hell_list = 3317
prev_hell = 0
def op2(idx):
    global z3_hit, prev_hell
    #print(f'    if {mem[idx]} <= 0 ({mem_z3[idx]} <= 0)')
    if type(mem_z3[idx]) == z3.z3.ArithRef:
        z3_list.append(mem_z3[idx])
        if i + 3 == 3317:
            if 'input[0]' in str(z3_list[-1]):
                z3_hit_list_for_solver.append('s.add('+str(z3_list[-1]).replace('input','input_z3')+' == 0)')
            else:
                z3_hit_list_for_solver.append('s.add('+str(z3_list[-1]).replace('input','input_z3').replace('+', '+\\')+' == 0)')
            mem[idx] = 0
            return True
        prev_hell = i + 3
    return mem[idx] <= 0

i = 0
while i >= 0:
    #print(f'{i}:')
    #print(f'    {mem[i]} {mem[i+1]}')
    op1(mem[i], mem[i+1])
    if op2(mem[i+1]):
        #print(f'    i = mem[{i+2}] ({mem[i+2]}) ({mem_z3[i+2]})')
        i = mem[i+2]
    else:
        #print('    i += 3')
        i += 3
print(str_to_print)

#print(len(z3_list)-1)
#print(str(z3_list[-1]).replace('input','input_z3'))
#print('prev_hell', prev_hell)


with open('./solve.py', 'wt') as f:
    f.write("from z3 import *\x0as = Solver()\x0ainput_z3 = [BitVec('input[%d]'%i,8) for i in range(8 * 7 + 1)]\x0a"+'\n\n'.join(z3_hit_list_for_solver)+"""
      
for i in range(len(input_z3)-1):
    s.add(input_z3[i] >= 0x20)
    s.add(input_z3[i] <= ord('~'))
s.add(input_z3[-1] == ord('}'))
print(s.check())
m = s.model()
flag = 'hitcon{'
for i in range(len(input_z3)):
    flag += chr(m[input_z3[i]].as_long())
print(flag)
"""
            )
    
from pwn import process
process(['python3', 'solve.py']).interactive()
#python3 solve.py
#hitcon{r3vErs1ng_0n3_1ns7ruction_vm_1s_Ann0ying_c9adf98b67af517}

 

ps.

def aaw(value_idx, relative_addr_from_libc_base, ret_idx):
    return f'%x{hex(0x10+value_idx)[2:]}\n%x{hex(0x107fe+relative_addr_from_libc_base//8)[2:]}\n%x1\n%x1\n%xffffffffffffffff\n%x{hex(0x10+ret_idx)[2:]}\n'

This is my aaw primiitve function for "subformore".

The first index from mem of the first input integer is 0x10.

So, I did add values to the front of the inputs like this and made a payload referencing those values to write, adding 0x10 to them.

payload = f"%x{hex(0xfbad2887 - 0xfbad1800)[2:]}\n%x4141414141414141\n"
payload += aaw(0, libc.symbols['_IO_2_1_stdout_'], 2+6)

 

It was quite hard to aaw properly cause it was ridiculously sensitive, but anyway shout out to qwerty who solved it with my poor aaw :)