ImaginaryCTF 2022 reverse writeups

Introduction

At the last Imaginaryctf, we took 7th place, covering the entire reverse.

A small description of the tasks:

The House Always Wins - glibc random prediction
Jormungandr - python virual machine
One Liner Revenge - python labyrinth
xobeert - another python virual machine
wired - avr rng

The House Always Wins

Given a binary with the following content

unsigned int get_rand()
{
  FILE *stream; // [rsp+8h] [rbp-18h]
  int j; // [rsp+14h] [rbp-Ch]
  int i; // [rsp+18h] [rbp-8h]
  unsigned int seed; // [rsp+1Ch] [rbp-4h]

  rand();
  if ( !init )
  {
    init = 1;
    seed = 0;
    stream = fopen("/dev/urandom", "r");
    for ( i = 0; i <= 7; ++i )
    {
      seed += fgetc(stream);
      if ( i != 7 )
        seed <<= 8;
    }
    fclose(stream);
    srand(seed);
    for ( j = 0; j < rand() >> 15; ++j )
      rand();
  }
  return rand() >> 15;                          // 17 bit
}

int main(int argc, const char **argv, const char **envp)
{
  char v3[59]; // [rsp+0h] [rbp-70h] BYREF
  char aswer; // [rsp+3Bh] [rbp-35h] BYREF
  unsigned int bet; // [rsp+3Ch] [rbp-34h] BYREF
  FILE *v6; // [rsp+40h] [rbp-30h]
  int rand2; // [rsp+4Ch] [rbp-24h]
  unsigned int v8; // [rsp+50h] [rbp-20h]
  unsigned int v9; // [rsp+54h] [rbp-1Ch]
  float v10; // [rsp+58h] [rbp-18h]
  float v11; // [rsp+5Ch] [rbp-14h]
  int rand; // [rsp+60h] [rbp-10h]
  unsigned int prize; // [rsp+64h] [rbp-Ch]
  int is_win; // [rsp+68h] [rbp-8h]
  unsigned int dollar; // [rsp+6Ch] [rbp-4h]

  puts("You start with $100. Get 1 billion dollars, and we'll give you the flag.");
  puts("Run out of money, and we kick you out of the casino.\n");
  puts("Are you feeling lucky?\n");
  dollar = 100;
  while ( 1 )
  {
    rand = get_rand();
    printf("Current money: %u\n", dollar);
    if ( dollar > 1000000000 )
      break;
    puts("How much are you betting? (minimum bet $5)");
    printf(">>> ");
    __isoc99_scanf("%u%c", &bet, &dead);
    if ( bet <= 4 || dollar < bet )
    {
      puts("You can't bet that!");
      puts("Get out of here, and come back with some real money!");
      exit(1);
    }
    dollar -= bet;
    printf("The first number is %d.\n\n", (unsigned int)rand);
    v11 = (float)((float)rand + 1.0) / 65536.0; / (r+1)/65536
    v10 = 1.0 - v11;                            
    v9 = (int)((double)(int)bet * 0.99 / v11);
    v8 = (int)((double)(int)bet * 0.99 / (float)(1.0 - v11));
    printf(
      "Odds of higher: %.2f\tPayout of higher: %u\n",
      (float)(100.0 * v10),
      (unsigned int)(int)((double)(int)bet * 0.99 / v10));
    printf("Odds of lower:  %.2f\tPayout of lower:  %u\n\n", (float)(100.0 * v11), v9);
    puts("Do you think the next number will be:");
    puts("1) Higher");
    puts("2) Lower\n");
    puts("Remember, the house wins ties!");
    printf(">>> ");
    __isoc99_scanf("%c%c", &aswer, &dead);
    rand2 = get_rand();
    is_win = 0;
    prize = 0;
    printf("The second number is %d!\n", (unsigned int)rand2);
    if ( aswer == '1' && rand < rand2 )
    {
      is_win = 1;
      prize = v8;
    }
    else if ( aswer == '2' && rand > rand2 )
    {
      is_win = 1;
      prize = v9;
    }
    if ( is_win )
    {
      printf("Congrats! You won %u dollars!\n\n", prize);
      dollar += prize;
    }
    else
    {
      puts("You lost... Better luck next time!\n");
    }
  }
  v6 = fopen("./flag.txt", "r");
  __isoc99_fscanf(v6, "%s", v3);
  printf("How'd you beat the house? %s\n", v3);
  exit(0);
}

We are given the result of get_rand and are asked to guess from it whether the result of calling the next get_rand will be higher or lower. Since srand is called once the first time get_rand is run, the function becomes

unsigned int get_rand()
{
  rand();
  return rand() >> 15;                          // 17 bit
}

In this article has a good description of random in glibc and how to predict it:

Since rand is called 4 times in one move - [0,n1,0,n2] (where n1 is known, 0 is not, n2 we need to guess), the expression becomes o[i] = o[i-31-3] + o[i-31-31] + o[i-3-3] + o[i-3-31] = o[i-62] + o[i-9] + 2*o[i-34], therefore i>=62, so we need 62//4=16 rounds to start winning. We need about log(1000000000, 2)~=30 requests to get the flag, so we don’t have to worry about optimizing all this.

First, let’s test random prediction algorithm on the local:

from os import urandom
from ctypes import CDLL


libc = CDLL("libc.so.6")


def init():
    seed = int.from_bytes(urandom(8), "big")
    libc.srand(seed)
    for _ in range(libc.rand() >> 15):
        libc.rand()


def get_random():
    libc.rand()
    return libc.rand() >> 15

init()

o = []
for i in range(50):
    o.append(-1)
    libc.rand()
    o.append(libc.rand() >> 15)

get_mod = lambda x: ((x << 15) % 2147483647) >> 15
for i in range(63,100,4):
    print(o[i] - get_mod(o[i - 62] + o[i - 6] + o[i - 34] * 2))

It works! The difference between the predicted and actual value is less than 4, which suits us, since we don’t need such an accurate result. Final solution code:

from pwn import remote, context


context.log_level = "debug"

r = remote("the-house-always-wins.chal.imaginaryctf.org", 1337)
r.recvlines(6)
o = []


def bet():
    current_money = int(r.recvline().split()[-1])
    r.recvline()
    r.recv(4)
    if len(o) >= 31:
        r.sendline(str(current_money).encode())
        o.append(int(r.recvline().split()[-1][:-1]))
        predict = (((o[-17] * 2 + o[-31] + o[-3]) << 15) % 2147483647) >> 15
        if predict > o[-1]:
            status = b"1"
        else:
            status = b"2"
    else:
        r.sendline(b"5")
        o.append(int(r.recvline().split()[-1][:-1]))
        status = b"1"
    r.recvlines(9)
    r.recv(4)
    r.sendline(status)
    o.append(int(r.recvline().split()[-1][:-1]))
    r.recvlines(2)


for i in range(200):
    bet()
# ictf{if_the_house_isn't_using_cryptographically_secure_PRNG_the_house_deserves_to_lose}

– There was an insert in Russian from this meme https://www.youtube.com/watch?v=6mE_oQbl8Ig –

Jormungandr

We are given the following python stack virtual machine:

find=lambda v:(i:=0,len([(i:=i+1)for(c)in(iter(lambda:text[i].startswith(v), True))]))[1]

def p(N):
    Enter =1
    prime=2# flag
    while Enter<N:
        prime+=(1+prime%2)
        s =prime%N
        for( hile)in range(3, prime,int( hex (2),16)):# salt
            if( prime%hile)==0 : break
            j__f = prime
        else:
            Enter+=1
    return(prime)

text=open( __file__).read().split()

try:
    while False:0
    while 1:
        {**{chr(i):lambda:0for(i)in range(32,127)},**{
            'l':lambda:text.insert(find(text[0][1:])+1,input()),
            's':lambda:text.append(text.pop(0)),
            'd':lambda:(text.pop(),text.pop()),
            'w':lambda:(text.pop(find(text[0][1:])+1),text.insert(find(text[0][1:])+1,text[1])),
            'i':lambda:(b:=text[1],text.pop(1),text.insert(1,('{:0%dx}'%(len(b))).format((int(b[:len(b)],16)*(3**p(len(text)))+p(len(text)))%16**(len(b)))),text.append(text.pop(0))),# lit
            'q':lambda:[text.pop()for( d)in iter(int,1)],
            'j':lambda:( chile :=text[0][1:],[text.append(text.pop(0))for(i)in(iter(lambda:text[0].startswith(chile),True))]),'p':lambda:print(text[1],end=' j__f '*0),# kite ce10e59f40c8d954d9dad1ea81811a834d26580107149d16c3a769198fb158f0cb0e33dbd98f8dc8bb874105974b71719790b23c971736e8fe8ec88e8695 p
            'not' :lambda: print(' bad... '),
            'c':lambda:text.append(text.pop(0))if text[find(text[0][1:])+1][1]==text[1][0]else[text.append(text.pop(0))for(i)in' q'],
            'k':lambda:text.append(text.pop(0))if text[find(text[0][1:])+1]==text[1]else[text.append(text.pop(0))for(i)in' q'],
        }
        }[text[0][0]]()
        text.append(text.pop(0))
except:
    pass

The file reads itself and, apparently, the bytecode for vm is based on this:

text=open(__file__).read().split()
...
text.insert(find(text[0][1:])

This problem is easily solved by creating a new file and changing __file__ to original.py

text is clearly our machine’s stack, and the {'l':lambda:..., 's': lambda: ...,} dictionary is like instruction handlers. Let’s write a disassembler for them:

def disp(opc): # disp(text[0][0])
    if opc == 'l':
        print(f"text[{find(text[0][1:])+1}] = input()")
    elif opc == 's':
        print('POPINS # {text[0]}')
    elif opc == 'd':
        print('POP 2')
    elif opc == 'w':
        print(f'POP text[{find(text[0][1:])+1}] && text[{find(text[0][1:])+1}] = text[1] # {text[1]}')
    elif opc == 'i':
        b = text[1]
        pp = p(len(text)-1) # I spent 6 hours searching for an error in this opcode logger.
        res = (int(b,16)*(3**pp)+pp) % (16**(len(b))) # b*3**p + p mod 16**len(b)
        print(f'text[1] = ({int(b,16)} * {(3**pp)} + {pp}) % ({16**(len(b))}) = {res} && POPINS # pp = {pp}')
    elif opc == 'q':
        print(f'text = [] # QUIT')
    elif opc == 'j':
        print(f"POPINS while (text[0] not start '{text[0][1:]}' )")
    elif opc == 'p':
        print(f"Print {text[1]}")
    elif opc == 'c':
        print(f'if text[{find(text[0][1:])+1}][1] ({text[find(text[0][1:])+1][1]}) == text[1][0] ({text[1][0]}) then POPINS else POPINS 2')
    elif opc == 'k':
        print(f'if text[{find(text[0][1:])+1}] ({text[find(text[0][1:])+1]}) == text[1] ({text[1]}) then POPINS else POPINS 2
    print(f"POPINS")

A small comment on the instructions:

l - reads from input and pushes onto the stack
s - POPINS (POP & INSERT), that is, it removes the bottom element of the stack and pushes it to the top (in other words, it shifts the stack 1 element to the left)
d - removes the top 2 elements of the stack
w - removes the element at index find(text[0][1:])+1, and then puts it at the same index text[1] # if find(text[0][1:])+1 == 0, then this find(...) will return already a new index
q - removes all elements from the stack, which throws an exception, causing the machine to be interrupted
j - rotates the stack to the left until text[i] not starts with text[0][1:]
p - prints text[1] to the console
c, k - some comparisons
i - pushes to the top of the stack b*3**p + p mod 16**len(b) (where b=text[1], pp = p(len(text)-1), function p returns the nth prime number)

After these and any other opcodes, vm will make POPINS

So let’s run our disassembler with input a:

As you can see, int(input(), 16) is passed to the i handler, and then the result of the function goes further until it reaches the k (comparison) handler, in which it compares the results with a certain constant and depending on this produces bad... or not bad...:

As a result, we have an equation of the form ((b * 3^p1 + p2) * 3^p3 + p4) * ... == 0xce10e... mod m We solve it with sage and take the flag

m = 16**124 # easily to guess by looking at the length of the constant being compared ~= log(0xce10..., 16)
n = Mod(0xce10e59f40c8d954d9dad1ea81811a834d26580107149d16c3a769198fb158f0cb0e33dbd98f8dc8bb874105974b71719790b23c971736e8fe8ec88e8695,m)
n -= 277
n /= 1454077510067338869372316944847370699315973030897976908309312512336980481738317971337352174999857054574561953999845406588476984323763
n -= 283
n /= 1060022504839090035772419052793733239801344339524625166157488821493658771187233801104929735574895792784855664465887301402999721572023227
n -= 307
n /= 299381664701132778293030021884627147018656102332612973563127175701392996827190480510641050862491714816103809471587812971633152346558576658975844187
n -= 313
n /= 218249233567125795375618885953893190176600298600474857727519711086315494687021860292257326078756460100939677104787515656320568060641202384393390412323
n -= 331
n /= 84554224792451089968936207473892531191988484041341985013001115226199070159922911068116016183264280284215039063438883556666870418811396281309653281910088285947
n -= 347
n /= 3639782124011924976038695589926766574205325707740600894440840379831043263633626934257002144272462342660405490567954921015326460861727327341974159433117917530528729787
print(long_to_bytes(n)) # ictf{welcome_to_the_flag_at_the_end_of_the_universe!_8762a9ab}

xobeert

We are given ast (abstract syntax tree) dump of a python program. We try to parse it with ast.unparse (that nice feature was introduced in 3.9), but we get AttributeError: 'Assign' object has no attribute 'lineno' which is fixed with ast.fix_missing_locations:

from ast import *
tree = eval(open('boxast.txt').read()[1:-3])
tree = ast.fix_missing_locations(tree)
decompiled = unparse(tree)
open('out.py', 'w').write(decompiled)

We get another hellish obfuscated code (привет one liner):

As you can see, everything is tied to decorators. The easiest way to understand this is by looking at the main function from this task, which can be rewritten as follows:

def main():
    pass
main = print(fffffffffffffffffffffffffffffffffff(main))

So, let’s start deobfuscation main function’s decorators:

The first decorator in queue will be the function before bytes.decode in the screenshot above:

As you can see, this function calls some method from random, let’s start the log function to see what is in bytes.decode before calling random.__dict__.get:

def log(string):
    print(string)
    return string

ok, this is the random.seed function.

climb up the main function above

The function takes the length of our input, let’s call it get_input_len , and the function with getting input get_input

we rise even higher

using log find out what is random.randbytes

move on

This function xors our input with the y array that is passed into it, temporarily we call it xor_with_input

finally

The last function compares the value passed to it with a certain constant array, which we can pull out using the usual print ([123, 250, 94, 95, 121, 195, 249, 70, 71, 59, 137, 59, 5, 67, 65, 226, 17, 160, 205, 100, 251, 169, 50, 118, 184, 177, 1, 175, 133]), followed by wrong or correct. Let’s call the function cmp_with_some_array.

So we have a deobfuscated main:

With the help of log we pull out the initial seed for the random - debdbeef_or_sth , and then everything is quite easy:

import random
cmp_arr = [123, 250, 94, 95, 121, 195, 249, 70, 71, 59, 137, 59, 5, 67, 65, 226, 17, 160, 205, 100, 251, 169, 50, 118, 184, 177, 1, 175, 133]
random.seed('debdbeef_or_sth')
seed2 = random.randbytes(len(cmp_arr)) # because len(input) == len(cmp_arr)
random.seed(seed2)
print(xor(random.randbytes(len(cmp_arr)), cmp_arr)) # ictf{wh0_n33d5_c4ll5_4nyw4y?}

P.S. this task was broken and the orgs managed to fix it only on the second try

One Liner Revenge

We are given a file with the following content (more lambdas further):

I was a little taken aback. After jormungandr, I didn’t want to solve it at all, but still I managed to convince myself that this was a dream and you just need to deobfuscate the code a little and everything will be fine. So the first lines of code turn into

# globals().__setitem__(chr(0x67),globals())
g = globals()
# g.__setitem__(chr(0x74),lambda*a:bytes.fromhex('{:x}'.format(a[0])).decode())
t = lambda*a: bytes.fromhex('{:x}'.format(a[0])).decode()

Further down the code, we see that t decodes strings. We replace its calls with decoded strings, trying to bring the code to a human form:

It’s still better than the original hell, but still terrible. On line 7 we see a check that the file has not been patched (how to bypass it, I think, is clear without me). It would be possible to deobfuscate this cringe further, but a better idea came to my mind. What if we trace the execution of a huge array of lambdas and already navigate through them, what to do next? So, we start the aboba function, which will help us with this, and try to insert it into the lambda:

def aboba(a, *equations):
    print(a, equations)
    return equations
...
# *(lambda*a:(51*a[10]+56*a[0]+...), ...) -> *(lambda*a:aboba(a, 51*a[10]+56*a[0]+...)

As you can see, our input is passed to lambdas, and at the output we get the result of executing 4 equations. I immediately tried to make all the equations give me True, but it didn’t work. Then we try to see in what order the lambdas are executed:

def aboba(a, num, *equations):
    print(a, num, equations)
    return equations
...
# *(lambda*a:(51*a[10]+56*a[0]+...), ...) -> *(lambda*a:aboba(a,1, 51*a[10]+56*a[0]+...)

That is, the program quits after two lambdas. Wait, what if we replace (False,False,False,False) with, say, (2,2,2,2) ? The program throws an error ValueError: invalid literal for int() with base 2: '2222', by which we find its culprit:

I assumed that in order to move on to the next pair of equations, I need to find the desired pair of lambda results, that is, iterate over 2^8=256 (there can be 4 true or false values in the lambda result) values. To do this, I had to dodge a little by adding a new input to the code and removing the previous one:

i2 = list(map(int, input().split())) # we enter an extra 0, which is converted to (0,0,0,0) and (0,0,0,0) to see if we passed on the next 2 lambdas
print(i2)

def to_bits(i):
    return [int(j) for j in '{0:08b}'.format(int(i))]

bits = []
for i in i2:bits.extend(to_bits(i))
ctr = 4

def aboba(a, num, *equations):
    global ctr
    print(a, num, equations)
    res = bits[ctr-4:ctr]
    ctr+=4
    return res

And we start it all with the help of crutches:

for i1 in range(256):
    os.system(f"echo '{i1} {0}' | python3.9 ./ff2.py") # 0 is an extra value

18 (or rather 0, 0, 0, 1 and 0, 0, 1, 0) and is the desired result of the first lambda pair in order to proceed to the execution of the second (some kind of labyrinth). Similarly, we dump the necessary values of the remaining lambda pairs (I did it manually, only 8 requests were needed) - [18, 52, 86, 120, 154, 188, 222, 240]

Hurray, the path in the labyrinth of lambdas has been found, it remains only to make sure that our input allows us to pass it. The final script for the solution:

import z3

def to_bits(i):
    return [int(j) for j in '{0:08b}'.format(int(i))]

ll = (lambda *a: 51*a[10]+56*a[0]+... , lambda *a: ...)

sp = [16, 1, 15, 2, 14, 3, 13, 4, 12, 5, 11, 6, 10, 7, 9, 8]
lambd_results = [18, 52, 86, 120, 154, 188, 222, 240]
a = [z3.Int(f"flag[{i}]") for i in range(24)]

cons = []
for lambd_res in lambd_results:
    t = to_bits(lambd_res)
    cons.append(t[:4])
    cons.append(t[4:])

s = z3.Solver()

for i in range(16):
    l_result = ll[sp[i]-1](*a)
    for j in range(4):
        if cons[i][j] == 1:
            s.add(l_result[j])
        else:
            s.add(not l_result[j])

for k in range(24):
    s.add(a[k] <= 126)
    s.add(a[k] >= 32)

print(s.check())
res = s.model()
flag = ""
for letter in a:
    flag += chr(res.eval(letter).as_long())

print(flag)

# sat
# ictf{0n3l1n3is5uperior!}

wired

We are given firmware for arduino and a video showing how the board gives us flag encrypted with hardware rng module.

We find a good writeup with a detailed guide on the avr reverse, from which we take:

processor module ATmega328 for ida
diaphora plugin, with which we can make our life easier by finding a diff between the binary we compiled containing built-in functions and the desired binary. This is necessary to restore the function names, in our case, only 3 functions will be restored:

Looking at the video and measuring the delay that is created using delay, between the order of lighting up the LEDs, we understand that it is approximately equal to 200 ms, which corresponds to the following loop:

From here we extract the order of bits (Rock paintings of ancient Shiz in my performance):

Encryption algorithm:

We generate a random stream (in fact, it immediately XORs it with the flag, but for the sake of simplicity, I will omit it)

We see a loop in which the program waits for the input of an analog signal (voltage) and converts it into a ten-bit number, which is divided into registers r24 and r25.

We find out that this is the seed for our RNG. Since it only takes 10 bits, we need 2^10=1024 attempts to guess it, so it can be bruteforced.

The rng stream generation algorithm is above, stupidly rewrite it in C, adding the seed brute.

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

unsigned char orig[] = {????}; // program output

int check_rng(unsigned char r24, unsigned char r25) {
    unsigned char work[21];
    memcpy(work, orig, 21);

    for(int i = 0; i < 20; i ++) {
        unsigned char *c = &work[i];
        *c = *c ^ r24;
        unsigned char r18 = r24;
        unsigned char r19 = r25;
        unsigned int r25r24 = (r25 << 8) | r24;
        r25r24 = r25r24 >> 1;
        r25 = (r25r24 & 0xFF00) >> 8;
        r24 = (r25r24 & 0xFF);
        if (r18 & 1) {
            r25 ^= 0xAD;
        }
    }
    write(1, work, 20);

}

int main() {
    for(int seed = 0; seed < 1024; seed++) {
        unsigned char r24 = (seed & 0xFF00) >> 8;
        unsigned char r25 = (seed & 0xFF);
        check_rng(r25, r24);
    }
}

xor flag at 0x100 with rng stream
we output it to the LEDs, some of which are inverted

To put it quite simply, when jumping to a branch with sbrc, we have a bit inverted, when hitting sbrs - no. We get a mask that denotes the LEDs on which the bits are inverted - 0b10011010

We derive the formula for obtaining the flag: flag[i] ^ rng[i] ^ invert_mask = out[i] => flag[i] = rng[i] ^ 0b10011010 ^ out[i]

According to the video, we define the out array and immediately apply a mask to it.

a = [0b01010110, 0b10101011, 0b01000111, 0b10101000, 0b11001011, 0b01111000, 0b00110101, 0b00010110, 0b10011010, 0b11000111, 0b01011001, 0b00100110, 0b10010011, 0b01001110, 0b10011100, 0b00001111, 0b11111101, 0b10000011, 0b01101101, 0b00101101]
out = list(map(lambda o: o ^ 0b10011010, a)) # [204, 49, 221, 50, 81, 226, 175, 140, 0, 93, 195, 188, 9, 212, 6, 149, 103, 25, 247, 183]

Final solution code:

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

unsigned char orig[] = {204, 49, 221, 50, 81, 226, 175, 140, 0, 93, 195, 188, 9, 212, 6, 149, 103, 25, 247, 183, 0};

int check_rng(unsigned char r24, unsigned char r25) {
    unsigned char work[21];
    memcpy(work, orig, 21);

    for(int i = 0; i < 20; i ++) {
        unsigned char *c = &work[i];
        *c = *c ^ r24;
        unsigned char r18 = r24;
        unsigned char r19 = r25;
        unsigned int r25r24 = (r25 << 8) | r24;
        r25r24 = r25r24 >> 1;
        r25 = (r25r24 & 0xFF00) >> 8;
        r24 = (r25r24 & 0xFF);
        if (r18 & 1) {
            r25 ^= 0xAD;
        }
    }
    write(1, work, 20);

}

int main() {
    for(int i = 0; i < 1024; i ++) {
        unsigned char r24 = (i & 0xFF00) >> 8;
        unsigned char r25 = (i & 0xFF);
        check_rng(r25, r24);
    }
}

And run:

./a.out | grep -oaiP 'ictf{.*?}'
ictf{weird_rng_912b}

Last modified on 2022-07-20