N1CTF2020 n1vault, Thoughts & Solutions

Intro

I designed the RE challenge n1vault in the recent CTF N1CTF2020. In this post, I will talk about details about this chal and offer some possible solutions.

The core part of this challenge is to craft a file’s CRC to an arbitrary value(zero) by modifying some specified bytes (of the same bit size as the CRC value) in the file.

As for the binary n1vault, it uses SHA256 to digest all the bytes inside the file(credencial.png) except for the even-numbered bytes in the last 25 bytes(some twists were added to the sha256_update function, paving the way for the backdoor). Once the file’s CRC is faked to 0, a secret logic(backdoor) will be triggered by an exception FPE_INTDIV, since the verification inside the function main has an unnecessary comparison 4764888639493207598 / (crc32_result | crc64_result) == 1, which will trigger an FPE_INTDIV when both crc32_result and crc64_result are zero, and will be evaluated to true when given the original file credential.png. Players’ job is to to craft an input to trigger the backdoor, send the crafted bytes to the judging bot and receive the flag.

Solution

The reverse engineering part of the binary program is quite easy. Some junk codes with fixed patterns are inserted into the main logic, which can be bypassed by a simple pattern searching & replacing. Afterward, the program logic is straightforward, and we only have to solve the math problem left.

CRC has a property that the final result can be viewed as the linear combination of the influences of each bit in the message and an initial offset, on $GF(2)$. This can be described as follows:

where $f(0)$ is the initial offset, specifically for this challenge, is the CRC of the credential with all the even-numbered bytes in the last 25 bytes set to zero. Given this property, if we have enough $x_i$ to control, we can easily construct a matrix and solve each $x_i$ using gaussian elimination. The trick here is we have to ensure that both $f(x)=CRC32(credential)$ and $g(x)=CRC64(credential)$ are equal to zero. In fact, if we let $h(x)=(f(x) < < 64)+g(x)$ and focus on making $h(x)=0$, it has the same effect as making both $f(x)$ and $g(x)$ zero.

I wrote a tool based on this interesting property of CRC, allowing us to arbitrarily craft a file’s CRC by specifying certain bits available for modification. It can output all the available solutions and allows for fewer available bits than the bit size of the CRC result. You can check the tool here:

https://github.com/yype/crcollider

Using this tool we can easily solve the problem using the following Python code:

from crcollider import collcrc
from crc_funcs import crc64, crc32

def crc96(m):
    return (crc32(m) << 64) + crc64(m)

def solve_chal():
    with open('credential.png', 'rb') as f:
        org_img = f.read()

    rg = list(range(len(org_img)*8))
    available_bits = []
    for i in range(12):
        # even bytes in the last 25 bytes
        available_bits += rg[len(rg)-16*i-16:len(rg)-16*i-8]

    sol_num, sols = collcrc(crc96, 96, org_img, available_bits, 0x0)
    
    print(f'{sol_num} solution(s) found')

    for i, each in enumerate(sols):
        file_out = f'credential_sol{i}.png'
        print(f'Outputting sol{i} to {file_out}...')
        with open(file_out, 'wb') as f:
            f.write(each)

if __name__ == '__main__':
    solve_chal()

There are totally 4 solutions available for this challenge. One of them contains only visible characters, which is n1vaultadmin(intentionally crafted), while others are not. It might be better if I put some constraints to ensure that only one solution is available though.

solution> python3 .\main.py
4 solution(s) found
Outputting sol0 to credential_sol0.png...
Outputting sol1 to credential_sol1.png...
Outputting sol2 to credential_sol2.png...
Outputting sol3 to credential_sol3.png...

The source code of this challenge and a duplicate of this post are uploaded to GitHub. Check them out at: https://github.com/Nu1LCTF/n1ctf-2020/tree/main/RE/n1vault.