MidnightSunCTF Finals 2021 - Climb & Crackme (4 solves & 2 solves)

Эльбрус Reversing

September 20, 2021
rev elbrus e2k

Элбрус reversing


I played on the team “An Equal Mix” for MidnightSunCTF Finals 2021 and we got 5th place. Unfortunately the competition was held virtually (instead of in Sweden) so the start time ended up being relatively unfavorable for our US-based team (6am eastern and 3am pacific!).

This write up covers two of the challenges from finals: “Climb the mountain” and “Crack me if you can.” Both of these were reversing challenges written for the esoteric, Russian Эльбрус (Elbrus) CPU. I ended up spending most of the CTF working on these two problems due to several reasons discussed below but I learned a lot about this strange architecture and developed some new skills related to patching.

A brief guide to reversing Эльбрус

For a more complete (external) guide, see https://github.com/nrdmn/elbrus-docs

The most notable feature about Эльбрус assembly is the use of VLIW instructions. A single 512-bit word can encode several instructions that execute simultaneously. In objdump disassembly, these instructions appear in blocks like this:

10818:	13 90 00 04 20 04 00 c0 01 80 c6 8c 05 00 00 50 	
    ipd 3
    sxt,0,sm 6, %r0, %db[1]
    call %ctpr1, wbs = 0x5 

10828:	12 40 00 04 83 83 c1 10 f8 ff ff 4f 00 00 00 00 	
    adds,0 1, %r3, %r3
    disp %ctpr1,107e8 <start+0xc8>
10838:	81 01 00 04 22 c8 83 20 

    nop 3
    cmpbsb,0 %r3, 8, %pred2

10840:	01 10 00 00 42 04 00 c0 	
    ct %ctpr1 ? %pred2
    ipd 3

Most of the time this simultaneity is not relevant for reversing purposes and it is sufficient to pretend that instructions are executed one after the other.


Эльбрус has 32- and 64-bit regigisters %r0, %r1, … and %dr0, %dr1, … as well as mobile-base registers (kind of like stack arguments) %b[0], %b[1], … and %db[0], %db[1], …

Basic instructions

Most instructions are familiar to someone with experience in any RISC architecture. e2k-objdump includes information about instruction packing/encoding which usually can be ignored. For example here are some e2k instructions and their function:

  • adds,0 1, %r3, %r3: Add 1 to %r3 and store in %r3
  • addd,0,sm 0, _f64,_lts0 0x1af2d0, %db[1]: Add 0 to 0x1af2d0 and store in %db[1]
  • std,2,sm %db[0], [ %dr1 ]: Store the 64-bit value %db[0] in the address %dr1
  • ldw,0 [ _f64,_lts0 0x1b0968 ], %r8: Load a 32-bit value from address 0x1b0968 into %r8


Subroutine calls require a disp instruction followed later by a call instruction. For example, the following two blocks set up and invoke a call to start:

    nop 4
    disp %ctpr1,10720 <start>
    ipd 3
    call %ctpr1, wbs = 0x4

disp %ctpr1 configures the control transfer preparation register %ctpr1 and the following call %ctpr1 invokes the jump. Note that the call can occur much later in a given program.

In e2k-lcc calling convention, arguments are passed in the mobile-base registers or on the stack. For example, examine the following assembly code:

    getsp,0 _f32,_lts1 0xffffffe0, %dr1
    disp %ctpr1,6aec0 <__libc_write>
    setwd wsz = 0x8, nfx = 0x1
    setbn rsz = 0x3, rbs = 0x4, rcur = 0x0 
    addd,0,sm 0, _f32,_lts2 0x25, %db[2]
    addd,1,sm 0, _f64,_lts0 0x190264, %db[1]
    addd,2,sm 0, 1, %db[0]
    std,2,sm %db[2], [ 16 + %dr1 ]
    std,5,sm %db[1], [ 8 + %dr1 ]
    nop 2
    std,2,sm %db[0], [ %dr1 ]
    ipd 3
    call %ctpr1, wbs = 0x4

This code prepares a call to __libc_write and then configures three arguments 1, 0x190264, and 0x25 which are placed on the stack by three std instructions. Finally the call invokes the subroutine.

Equivalent C code would look like:

__libc_write(1, (const char *)0x190264, 0x25);


Conditional logic is obtained through the use of predicates. Compare instructions set predicate registers which can be used to conditionally execute subsequent instructions.

Take the following assembly in the func3 subroutine for example:

    ldw,0 [ _f64,_lts0 0x1af2dc ], %r1
    disp %ctpr1,10708 <func3+0x1a0>
    nop 2
    cmpesb,0 %r1, _f32,_lts0 0x3baeb3e2, %pred7
    ct %ctpr1 ? %pred7
    ipd 3

The first block prepares a control transfer preparation register with a label address (func3+0x1a0). The second block executes %pred7 = (%r1 == 0x3baeb3e2). The third block conditionally invokes ct %ctpr1 (a control transfer) if %pred7 is true. Note that instructions can also execute if a predicate is false, i.e. ct %ctpr1 ? ~ %pred7 would be the inverted variant.

Part 1: Climb the Mountain

I started working on this problem at 8am eastern (2 hours into the competition). My only previous experience with Elbrus was a CSAW problem from 2019 which I didn’t solve so I was determined to overcome that hurdle.

In the old CSAW problem, the challenge author had provided an e2k-linux-gnu binutils toolchain containing things like objdump and gcc (https://drive.google.com/file/d/1rdlSKGkOXC9ejXaWC2mUKZd6GYxdtHLt/view?usp=sharing) so I used this objdump to disassemble the climb binary.

Luckily for us, the binary is not stripped so we have function names and we can see that libc has been statically linked.

The challenge-relevant part of the binary is surprisingly short and we only have the following functions to deal with: swap, func1, func2, func3, start and main.


In main, we see a call to __libc_write (provided in the example above) which simply prints Mountain Base, the hike starts here. followed by a call to start.


At a cursory glance, start invokes __libc_read(0, 0x1b2638, 0x20) then func1, then func2 a bunch of times and finally func3. There is some nuance in the middle part so I decided to start with the actual func subroutines first.


The first function proved to be relatively short as you can see:

    adds,0,sm 0, 0, %r2
    disp %ctpr1,10428 <func1+0x90>
    setwd wsz = 0x5, nfx = 0x1
    nop 3
    cmplsb,0 %r2, _f16s,_lts0hi 0x20, %pred0
    ct %ctpr1 ? ~ %pred0
    ipd 3
    sxt,0 2, %r2, %dr0
    sxt,1 2, %r2, %dr1
    adds,2 1, %r2, %r2
    disp %ctpr1,103c8 <func1+0x30>
    nop 2
    ldb,0 [ %dr0 + _f64,_lts1 0x1b2638 ], %r0
    cmplsb,1 %r2, _f16s,_lts0hi 0x20, %pred1
    sxt,0 0, %r0, %dr0
    nop 2
    ldb,0 [ %dr0 + _f64,_lts0 0x1af1c0 ], %r0
    ct %ctpr1 ? %pred1
    ipd 3
    stb,2,sm %r0, [ %dr1 + _f64,_lts0 0x1b2638 ]
    nop 5
    return %ctpr3
    ct %ctpr3
    ipd 3

I hand-reversed this into the following C-pseudocode:

uint8_t user[0x20]; // 0x1b2638
uing8_t lookup[0x100]; // 0x1af1c0

void func1() {
    for (int i = 0; i < 32; ++i) {
        user[i] = lookup[user[i]];

In essense it is simply applying a map on the user input buffer. If we example the bytes at address 0x1af1c0, we see that this is the reverse-sbox from AES.


The second function performed a parity check given two input values. I cross-referenced the usage in start to identify the parameters and then obtained this psueocode:

uint32_t boxes[8]; // 0x1af2c0

void func2(int idx, uint32_t val) {
    int parity;
    for (int i = 0; i < 32; ++i) {
        parity ^= ((boxes[idx] >> i) & 1) & ((val >> i) & 1);
    // shift box and push parity bit
    boxes[idx] = (parity << 0x1f) | (boxes[idx] >> 1);


This third function simply compares the values in boxes with fixed, target values and prints Ok if they match.

back to start

I returned back to the start method and figured out that there is some boxes parameter with 8 x 4-byte values (as seen in func2).

In essense, start does the following:

void start() {

    for (int n = 0; n < 32; ++n) {
        for (int idx = 0; idx < 8; ++idx) {
            func2(idx, user[idx]);

        // swap boxes by index


So overall, this seems to be some cipher that uses our (presumably flag) input to mutate values in boxes which are then compared to a fixed output. I didn’t recogize this cipher as an off-the-shelf implementation of anything (and neither did my crypto teammates) so I set about implementing a z3 version.

z3 implementation

I quickly translated this C psueocode into Python and then into z3 statements but I was getting unsat despite double checking everything. At 1:34 pm eastern (3.5 hours into this problem), I posted the following z3 script into our team discord and my teammated hpvm started to help debug the problem:

boxes = [
    0x13371337, 0x69696969, 0x51335133, 0x90909090,
    0x73317331, 0xb4b3b4b3, 0xc453c453, 0xd34dd43d

target = [
    0x268dee8d, 0xc444444, 0x28d078d0, 0x31b1b1b3,
    0x7ac17ad, 0x143814, 0x4267a267, 0x3baeb3e2

user = [BitVec('d%d' % x, 8) for x in range(32)]

def swap(a,b):
    boxes[a], boxes[b] = boxes[b], boxes[a]

def func2(idx, val):
    eq = boxes[idx] & val
    parity = BitVecVal(0, 1)
    for i in range(32):
        parity ^= Extract(i,i,eq)

    boxes[idx] = Concat(parity, Extract(30,0,LShR(boxes[idx], 1)))

def start():
    for r2 in range(0x20):
        for r3 in range(8):
            user_val = Concat(
            func2(r3, user_val)

        swap(0, 4)
        swap(1, 2)
        swap(6, 7)
        swap(3, 5)

s = Solver()

for i in range(8):
    s.add(boxes[i] == target[i])


the long climb

Unfortunately, this z3 script should have solved the problem but there were several bugs in the challenge which changed the functionality of the cipher and we ended up spending 14 more hours on this challenge.

The first issue was with the func2 call. See if you can spot the problem with this C code:

uint8_t user[32];

void func2(int idx, uint32_t val);

void start() {

    for (int n = 0; n < 32; ++n) {
        for (int idx = 0; idx < 8; ++idx) {
            func2(idx, user[idx]); // !!!



The issue is that the second argument to func2 should be a 32-bit word, but only the first byte of each 32-bit block is being read. This means that the output buffer only depends on every four bytes in the input (i.e. there’s no way that you can solve for the whole input).

In Elbrus assembly, the issue was a single instruction:

ldb,0 [ %dr0 + _f64,_lts0 0x1b2638 ], %r0

should have been

ldw,0 [ %dr0 + _f64,_lts0 0x1b2638 ], %r0

I.e. ldb -> ldw.

I reached out to the author about this bug at 1:44 pm eastern after spotting it, but since the author had validated the flag by running the binary, it seemed like a false alarm. Unfortunately a consequence of this bug is that the original flag would still work but so would a bunch of false positive flags. Up until now, I had been doing everything statically so I assumed I was just misreading the assembly.

Around this point I found the OpenE2K project which provided a qemu-e2k and I started working on setting this up to help debug. hpmv also started reading through the disassembly in case I had missed or misinterpreted anything. Once I got qemu working, I started looking for a suitable e2k-gdb (which I think exists but for the life of me I can’t find). After a few hours, I gave up on gdb and just started patching print statements into the binary to debug. Once we had a version that just printed the final box values, hpvm confirmed very convincingly that only the first byte in each 4-byte block was affecting the output values (since now we could see the output values directly). I reached out to the author again at 6:14 pm eastern, this time with better evidence, and the author agreed that this was a bug.

Once the author fixed all the bugs, I ran my z3 script again but it still didn’t work, this time it was sat but the output was jibberish. hpmv and I started debugging a bit more. We modified the outer loop to run just once instead of 32 times and noticed that our parity calculating seemed to be off.

We spent an embarassingly long time trying to figure this issue out, involving many different patched versions and various python scripts to run different combinations of user-input and custom intial box values. Around 10pm eastern this challenge was solved by the team Armia Prezesa which meant it was definitely solveable.

Around 2am eastern, hpvm ran some really nice tests where he took a fixed user value (U) and checked all the 1-bit box values (B) that would result in a parity bit being set in func2 and produced beautiful visualizations like the following:

U 1------- ----1--1 ----1--1 -------1
B 1------- -------- -------- --------
B -------- ----1--- -------- --------
B -------- -------1 -------- --------
B -------- -------- 1------- --------
B -------- -------- -1------ --------
B -------- -------- --1----- --------
B -------- -------- ---1---- --------
B -------- -------- -------1 --------
B -------- -------- -------- 1-------
B -------- -------- -------- -1------
B -------- -------- -------- --1-----
B -------- -------- -------- ---1----
B -------- -------- -------- ----1---
B -------- -------- -------- -----1--
B -------- -------- -------- ------1-

Surprisingly, the flippable bits do not seem to correlate 1:1 as we would expect and after some investigating, we found that sign bits seem to have some weird, cross-byte behavior. This prompted me to re-read the assembly and I found the culprit:

    shls,0 %r3, 2, %r0
    sxt,1,sm 6, %r3, %db[0]
    disp %ctpr1,10438 <func2>
    sxt,0 6, %r0, %dr5
    adds,1 1, %r0, %r6
    adds,2 2, %r0, %r7
    adds,3 3, %r0, %r0
    ldb,0 [ %dr5 + _f64,_lts0 0x1b2638 ], %r5
    sxt,1 6, %r6, %dr6
    sxt,2 6, %r7, %dr7
    sxt,3 6, %r0, %dr0
    ldb,0 [ %dr6 + _f64,_lts0 0x1b2638 ], %r6
    ldb,2 [ %dr7 + _f64,_lts2 0x1b2638 ], %r7
    nop 1
    ldb,0 [ %dr0 + _f64,_lts0 0x1b2638 ], %r0
    sxt,0 0, %r5, %dr5             (!!!)
    sxt,0 0, %r6, %dr6             (!!!)
    sxt,1 0, %r7, %dr7             (!!!)
    sxt,2 0, %r0, %dr0             (!!!)
    shls,0 %r6, 8, %r6
    shls,1 %r7, _f16s,_lts0hi 0x10, %r7
    shls,2 %r0, _f16s,_lts0lo 0x18, %r0
    adds,0 %r5, %r6, %r5
    adds,0 %r5, %r7, %r5
    adds,0 %r5, %r0, %r4
    ipd 3
    sxt,0,sm 6, %r4, %db[1]
    call %ctpr1, wbs = 0xe 

The byte values are sign-extended before being added together! On my initial read through, I didn’t think this would affect anything since the %rx registers are supposedly 32 bits so sign extending should be zero. But evidently this was not working as expected. It’s not obvious to me if this is actually what is supposed to happen in the assembly or if this behavior is a qemu-e2k bug (because it was cobbled together by hobbiests from sparse Russian documentation) but in our debug-patched binary, each byte was being invididually sign-extended to 32-bits before being shifted and added. We identified this by patching in print statements to func2 and looking at the arguments.

For example, if the user buffer looked like [0x80, 0x80, 0x80, 0x80, ...] the value actually passed to func2 would be:

+ 0xffff80
+ 0xff80
+ 0x80

This wouldn’t be a problem if our input was passed directly since ASCII doesn’t use the sign bit, however our input passes through an sbox first so we end up with many “negative” values.

Once we figured this out, we modified the z3 script to sign extend the user values and got multiple solutions. The side-effect of this sign-extension is that there are multiple ways to obtain the same 4-byte user value and hence there are multiple solutions. However we were able to identify key-words in the possible solutions and do a “z3-crib-drag” to pull out the flag:


We ended up getting the second of four solves for this challenge.

Part 2: Crack me if you can

“Crack me if you can” was the second of the two Elbrus reversing challenges, released at 8pm eastern (14 hours into the ctf). I started working on this around 10pm eastern (taking a break from Climb) and solved it in 2 hours.

I started this challenge the same as before, using e2k-objdump to disassemble it. Just like the other challenge, this one was compiled statically with libc and has symbols. The functions of interest are: health, gen, add, get, run, check, and main.


The main function is rather straightforward:

int main() {
    __libc_read(0, 0x1b2608, 0x24);

    if (health()) {
        // *COUGH*, you have poor health...
    } else {

I decided to try to start working through each other function in the calling order.


Unfortunately, gen proved to be more difficult than expected, with two calls to __libc_malloc and a ton of buffer manipulation:

    getsp,0 _f32,_lts1 0xffffffe0, %dr2
    setwd wsz = 0xc, nfx = 0x1
    setbn rsz = 0x3, rbs = 0x8, rcur = 0x0 
    addd,0 %dr2, _f32,_lts2 0x20, %dr1
    addd,1 0, _f64,_lts0 0x190530, %dr4
    disp %ctpr1,546b8 <__libc_malloc>
    ldd,0 [ %dr4 ], %dr5
    addd,1,sm 0, _f16s,_lts0hi 0xe8, %db[0]
    ldd,2 [ 8 + %dr4 ], %dr4
    nop 1
    addd,0 %dr1, _f16s,_lts0hi 0xfff0, %dr6
    std,2,sm %dr5, [ %dr6 ]
    std,5,sm %dr4, [ 8 + %dr6 ]
    std,2,sm %db[0], [ %dr2 ]
    ipd 3
    call %ctpr1, wbs = 0x8 
    sxt,0 2, %b[0], %dr4
    addd,1,sm 16, 0, %db[0]
    disp %ctpr1,546b8 <__libc_malloc>
    nop 3
    std,2,sm %dr4, [ %dr1 + _f16s,_lts0hi 0xfff8 ]
    std,5,sm %db[0], [ %dr2 ]
    ipd 3
    call %ctpr1, wbs = 0x8 
    sxt,0 2, %b[0], %dr3
    ldd,2 [ %dr6 ], %dr4
    ldd,3 [ 8 + %dr6 ], %dr5
    return %ctpr3
    nop 1
    addd,0 0, %dr3, %dr6
    addd,1,sm 0, %dr3, %dr0
    nop 2
    std,2,sm %dr4, [ %dr6 ]
    std,5,sm %dr5, [ 8 + %dr6 ]
    ct %ctpr3
    ipd 3

I translated to this C pseudocode but was having a hard time making sense of it at a higher level:

void gen(int size /* ?? */) {
    int *dr2; // stack?

    int *dr1 = dr2 + 0x20;
    void *buf_a = __libc_malloc(0xe8);
    int dr5 = 29;
    int dr4 = 0;

    int *dr6 = dr1 - 0x10;
    dr6[0] = dr5;
    dr6[1] = dr4;

    dr2[0] = 0xe8;

    dr4 = buf_a;
    void *buf_b = __libc_malloc(0x10);

    *(dr1 - 8) = dr4;
    dr2[0] = 0x10;

    int dr3 = buf_b;
    dr4 = dr6[0];
    dr5 = dr6[1];

    dr6 = dr3;
    int dr0 = dr3;

    dr6[0] = dr4;
    dr6[1] = dr5;

Since I was approaching my 15th hour overall of staring at Elbrus assembly, I decided to try a dynamic reversing approach.


From the name, I guessed the check function would somehow check the flag so I quickly scanned it and saw a simple buffer comparison of 36 bytes between 0x1af250 and 0x1b25d8, neither of which is our raw input buffer (0x1b2608). So our input is probably being processed into one of these buffers and then compared against a fixed target.

Most of my experience with patching at this point relied on either disassemblers like Binary Ninja or programatically modifying certain instructions at the assembly level. However, since there is no existing interactive disassembler for Elbrus and I don’t understand it well enough to program assembly for it, I used the e2k-gcc tool to compile C code and then simply copied the instructions directly into the binary. Admittedly, this technique is not particularly hard and I’m sure many other people are familiar with it. However, it was new to me so I decided to include it in this writeup in the hopes it will be helpful to others.

In short, we write a C program like the following:

// Patch into check
void foo() {
    void (*_target)() = (void (*)())(0x53b10);

// Patch into 0x53b10
int main() {
    void (*__libc_write)(int fd, const void *buffer, unsigned long size) = (void (*)())(0x6b188);
    void (*_exit)(int r) = (void (*)())(0x68cf8);
    void *buf1 = (void *)0x1af250;
    void *buf2 = (void *)0x1b25d8;

    __libc_write(1, buf1, 12 * 4);
    __libc_write(1, buf2, 12 * 4);

In the binary, I patch foo into the start of check and patch main into a random, unused libc function. In this case check is too small to hold all three of the calls so we need to use a short trampoline to jump into a separate area.

I patched manually by compiling this C program and then examining the function start and end addresses in objdump, using a short python script to overwrite sections of the original binary.

I ran this several times with different inputs and observed that the first buffer was fixed while the second buffer depends on our input. The first buffer looks like this:

$ echo "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" | ./qemu-e2k/build/qemu-e2k ./crack_mod | xxd
00000000: 0119 1700 4f0a 0000 35e4 0000 ad13 0000  ....O...5.......
00000010: d9ab 0000 c516 0000 c93c 0500 f97c 0000  .........<...|..
00000020: eb0f 0600

Interestingly there are a lot of null bytes and this actually looks like a little-endian int array instead of a char array.


I searched for other references to the computed buffer 0x1b25d8 and found several in the run function. I hand-decompiled to the following code:

static char *user; // 0x1b2608
static int* lookup; // 0x1af1c0
static int* output; // 0x1b25d8

void run() {
    int dr0; // ??

    int out_idx = 0;
    int curr_char = 0; // prev lookup index
    int acc = 1;

    for (int i = 0; i < 0x24; ++i) {
        char u = user[curr_char];

        acc *= get(dr0, u);
        curr_char = lookup[r3 * 4];

        if (i == 0) continue;
        if (i % 3 == 0) {
            output[out_idx++] = acc;
            acc = 1;

    output[out_idx++] = acc;

The one part I couldn’t figure out was what %dr0 contained. I’m pretty sure this is a pointer that is passed as an argument but I didn’t end up figure out this structure. The only usage is in the call to get so I didn’t worry about reversing that in too much detail at this stage.

In short, the rest of the code does the following: Iterate through the user buffer in an order determined by the lookup table. Compute a value by multiplying three consecutive results of get and store them, in order, in the output buffer.

Note that the first output value is actually the product of four steps and the final output value is the product of two steps. All the intermediate values are three steps.

Additionally, this code seems to verify that our output buffer is an int array.


As a side note, this was one function where the parallel execution of instructions actually ended up being important. See the following code:

    adds,0,sm 0, 1, %r6
    stw,2,sm %r6, [ %dr1 + _f64,_lts0 0x1b25d8 ]

Here %r6 is our acc variable and this corresponds to acc = 1 and output[out_idx] = acc. At first, I interpreted this as setting acc to 1 before storing it. However, since these instructions execute at the same time, the stored value of %r6 is actually the original value and not the new value of 1.

If we enter an input like aaaaa..., we get the following processed buffer:

[0x51, 0x1b, 0x1b, ..., 0x9]

Entering bbb... we get: [0x271, 0x7d, 0x7d, ..., 0x19]

Entering ccc... we get: [0x961, 0x157, 0x157, ..., 0x31]

If we look at these values we see that the buffers are the following:

a: [3**4, 3**3, 3**3, ..., 3**2]

b: [5**4, 5**3, 5**3, ..., 5**2]

c: [7**4, 7**3, 7**3, ..., 7**2]

However, for d we get: [0x3931, 0x533, 0x533, ..., 0x79] i.e. [11**4, 11**3, 11**3, ..., 11**2].

Hmm, this looks like sequential prime numbers!

To verify, I tested xxx... and got [0x546d981, 0xded21, 0xded21, ..., 0x24c1] i.e. [97**4, 97**3, 97**3, ..., 97**2].


During testing, I noticed that some input characters resulted in the *COUGH*, you have poor health... message. Specifically, I could only enter lowercase a-z and _{}.

A quick gance at health confirms this behavior and in the binary data section we see the following string: abcdefghijklmnopqrstuvwxyz_{}. So for our prime values as before, a corresponds to the 1st prime (starting at 3), b to the 2nd, z to the 26th and _{} to the 27-29th respectively.


Without even looking at this function, we’ve identified that it returns the Nth prime number where n is a user char.


Now that we understand the encoding procedure, we can use something like z3 to solve this.

import struct
from z3 import *

alph = 'abcdefghijklmnopqrstuvwxyz_{}'

primes = []
for i in range(3,1000):
    skip = False
    for j in range(2,i):
        if i % j == 0:
            skip = True
    if skip:

def char_factors(v):
    if v == 1:
        return []
    for i in range(len(primes)):
        if v % primes[i] == 0:
            return [alph[i]] + char_factors(v // primes[i])
    return []

dat = open('./crackme', 'rb').read()
order = list(struct.unpack('<36I', dat[0x19f1c0:0x19f1c0+(0x24*4)]))
target = list(struct.unpack('<12I', dat[0x19f250:0x19f250+(12*4)]))

inp = [BitVec('b%d' % x, 8) for x in range(36)]

# Which indexes will be used for a particular output value?
ranges = []
for i in range(0, len(order), 3):

s = Solver()

# Possible values for an index.
poss = {x: [] for x in range(36)}

for i in range(12):
    r = ranges[i]
    fac = char_factors(target[i])
    for k in range(len(r)):
        for j in range(k):
            s.add(inp[r[k]] != inp[r[j]])
        for f in fac:
            poss[r[k]].append(inp[r[k]] == ord(f))

for k in poss:

# Enumerate 100 solutions
for i in range(100):
    if s.check() != sat:

    m = s.model()
    flag = bytes([m[x].as_long() for x in inp])
    # Prevent this specific result.
    s.add(Not(And([inp[i] == flag[i] for i in range(36)])))

However, we get a bunch of solutions:


Even if we constrain the flag format, we get a bunch:

key = b'midnight{'
for i in range(len(key)):
    s.add(inp[i] == (key[i]))
end = b'}'
for i in range(1,len(end)+1):
    s.add(inp[-i] == end[-i])

However we can pick out some words like cracked and hell and guess the positions to constrain a bit more:


And finally we get something in English: midnight{cracked_in_quarentine_hell}.

We got 1st blood for this challenge.


If anyone knows where to find e2k-gdb please let me know!

comments powered by Disqus