Solution

First of all, we need to decompile the .apk file we are given:

public final class NativeValidator {
    public static final NativeValidator INSTANCE = new NativeValidator();

    public final native String deriveFlag(int g1, int g2, int g3, int g4, int kotlinToken);

    public final native boolean validateFull(int g1, int g2, int crc, int transformedG3, int interleaved, int g4, int mixedToken);

    private NativeValidator() {
    }

    static {
        System.loadLibrary("bedrockbank");
    }
}

public final class KeyValidator {
    private static final int CRC_POLY = 4129;
    private static final int INTERLEAVE_MASK = -16711936;
    private static final int MIX_ROUNDS = 7;
    private static final int TRANSFORM_SEED_A = 42240;
    private static final int TRANSFORM_SEED_B = 195;

    public final boolean validateFormat(String key) {
        Intrinsics.checkNotNullParameter(key, "key");
        Regex regex = new Regex("^BRCK-[0-9A-F]{4}-[0-9A-F]{4}-[0-9A-F]{4}-[0-9A-F]{4}$");
        return regex.matches(key);
    }

    public final boolean performFullValidation(String g1, String g2, String g3, String g4) {
        Intrinsics.checkNotNullParameter(g1, "g1");
        Intrinsics.checkNotNullParameter(g2, "g2");
        Intrinsics.checkNotNullParameter(g3, "g3");
        Intrinsics.checkNotNullParameter(g4, "g4");
        int g1Val = (int) Long.parseLong(g1, CharsKt.checkRadix(16));
        int g2Val = (int) Long.parseLong(g2, CharsKt.checkRadix(16));
        int g3Val = (int) Long.parseLong(g3, CharsKt.checkRadix(16));
        int g4Val = (int) Long.parseLong(g4, CharsKt.checkRadix(16));
        int crcValue = computeChecksum(g1Val, g2Val);
        int transformedG3 = g3Val ^ 42435;
        int interleaved = interleaveValues(g1Val, g2Val);
        int mixedToken = mixValues(g1Val, g2Val, g3Val);
        boolean result = NativeValidator.INSTANCE.validateFull(g1Val, g2Val, crcValue, transformedG3, interleaved, g4Val, mixedToken);
        return result;
    }

    public final String generateFlag(String g1, String g2, String g3, String g4) {
        Intrinsics.checkNotNullParameter(g1, "g1");
        Intrinsics.checkNotNullParameter(g2, "g2");
        Intrinsics.checkNotNullParameter(g3, "g3");
        Intrinsics.checkNotNullParameter(g4, "g4");
        int g1Val = (int) Long.parseLong(g1, CharsKt.checkRadix(16));
        int g2Val = (int) Long.parseLong(g2, CharsKt.checkRadix(16));
        int g3Val = (int) Long.parseLong(g3, CharsKt.checkRadix(16));
        int g4Val = (int) Long.parseLong(g4, CharsKt.checkRadix(16));
        int mixedToken = mixValues(g1Val, g2Val, g3Val);
        int interleaved = interleaveValues(g1Val, g2Val);
        int kotlinToken = mixedToken ^ interleaved;
        String flagBytes = NativeValidator.INSTANCE.deriveFlag(g1Val, g2Val, g3Val, g4Val, kotlinToken);
        return "dach2026{" + flagBytes + '}';
    }

    private final int computeChecksum(int v1, int v2) {
        int combined = (v1 << 16) | (v2 & SupportMenu.USER_MASK);
        int crc = SupportMenu.USER_MASK;
        for (int i = 0; i < 32; i++) {
            int bit = (combined >> (31 - i)) & 1;
            int xorBit = (crc >> 15) & 1;
            crc = (crc << 1) & SupportMenu.USER_MASK;
            if ((bit ^ xorBit) == 1) {
                crc ^= CRC_POLY;
            }
        }
        return 65535 & crc;
    }

    private final int interleaveValues(int v1, int v2) {
        int result = 0;
        for (int i = 0; i < 4; i++) {
            int nibble1 = (v1 >> (12 - (i * 4))) & 15;
            int nibble2 = (v2 >> (12 - (i * 4))) & 15;
            result = result | (nibble1 << (28 - (i * 8))) | (nibble2 << (24 - (i * 8)));
        }
   :    return Integer.rotateLeft(result, 5);
    }

    private final int mixValues(int v1, int v2, int v3) {
        int state = 1515870810 ^ v1;
        for (int round = 0; round < 7; round++) {
            int state2 = (Integer.rotateLeft(state, 3) ^ (v2 + round)) + Integer.rotateRight(v3, round * 2);
            state = state2 ^ ((state2 >> 16) | (state2 << 16));
        }
        return state;
    }
}

We can see that part of the validation happens in a native library. I opened the x86 variant of the libbedrockbank.so in Binary Ninja and cleaned it up a bit:

int32_t Java_com_bedrockbank_app_NativeValidator_validateFull(int32_t g1, int32_t g2, int16_t crcValue,
  int32_t transformedG3, int32_t interleaved, int32_t g4, int32_t mixedToken)

{
    if (set(g1) && eq(
        (g1 >> 3 & 0x1e) + (g1 >> 0xa & 0x3c) + (g1 & 0xf) + (g1 >> 8 & 0xf) * 3, 0x5e))
    {
        int32_t g1_g2_diff = g2 ^ g1;

        if (g1_g2_diff)
        {
            uint32_t g1_cast = (uint32_t)g1;
            uint32_t g2_cast = (uint32_t)g2;
            int32_t loopvar = 5;
            int32_t g1_g2_diff_1;

            do
            {
                loopvar -= 1;
                g1_g2_diff_1 = (g1_g2_diff - 1) & g1_g2_diff;
                g1_g2_diff = g1_g2_diff_1;
            } while (g1_g2_diff_1);

            if (!loopvar)
            {
                uint32_t crcValue_1 = (uint32_t)crcValue;

                if (eq(crcValue_1, 0xc430))
                {
                    int32_t edi_1;
                    edi_1 = ROLW(transformedG3, 3);

                    if (eq((uint32_t)edi_1 ^ 0xdead, 0xf646)
                        && eq(mixedToken, 0x12788169))
                    {
                        uint32_t eax_12 = interleaved >> 0x10;
                        int32_t pass = eq((uint32_t)g4,
                            (uint32_t)(crcValue_1 * 2) ^ (eax_12
                                + (int16_t)(eax_12 * 0xa) + (int16_t)(interleaved << 3)
                                - interleaved + g2_cast + (int16_t)(g2_cast << 2)
                                + g1_cast + (int16_t)(g1_cast << 1)) ^ 0x342e);

                        if (pass)
                        {
                            int32_t result;
                            result = sub_10d70();
                            return result;
                        }
                    }
                }
            }
        }
    }

    return 0;
}

All we need to do now is rewrite everything into z3 constraints. I didn’t get any usable results for a long time, until I realized that casting the variables to the right data type with a bitwise AND is important:

from z3 import *

s = Solver()

p1 = BitVec("x", 32)
p2 = BitVec("x2", 32)
p3 = BitVec("x3", 32)
p4 = BitVec("x4", 32)

s.add(p1 >> 16 == 0x0)
s.add(p2 >> 16 == 0x0)
s.add(p3 >> 16 == 0x0)
s.add(p4 >> 16 == 0x0)

###
# p3
###
di = p3 ^ 42435 # transformedG3
edi = ((di << 3) | (di >> (16 - 3))) & 0xFFFF
s.add(edi ^ 0xDEAD == 0xF646)

###
# p2
###
def mixValues(v1, v2, v3):
    state = BitVecVal(1515870810, 32) ^ v1
    for round in range(7):
        state2 = (RotateLeft(state, 3) ^ (v2 + round)) + RotateRight(v3, round * 2)
        state = state2 ^ (((state2 >> 16) & 0xffffffff) | ((state2 << 16) & 0xffffffff))
    return state
s.add(mixValues(p1, p2, p3) == 0x12788169)

###
# p1
###
def checksum(v1, v2):
    combined = (v1 << 16) | (v2 & 0xffff)
    crc = BitVecVal(0xffff, 32)
    for i in range(32):
        bit = (combined >> (31 - i)) & 1
        xorBit = (crc >> 15) & 1
        crc = (crc << 1) & 0xffff
        crc = If((bit ^ xorBit)==1, crc ^ 4129, crc)
    return crc
chcksum = checksum(p1,p2)
s.add(chcksum == 0xC430)


###
# p4
###
def interleaveValues(v1, v2):
    res = BitVecVal(0, 32)
    for i in range(4):
        nib1 = (v1 >> (12 - (i * 4 ))) & 15
        nib2 = (v2 >> (12 - (i * 4 ))) & 15
        res = res | (nib1 << (28 - (i * 8))) | (nib2 << (24 - (i*8)))
    return RotateLeft(res, 5)

interleaved = interleaveValues(p1, p2)
eax12= (interleaved >> 0x10) & 0xffff

s.add(
    p4 ==
    (0x18860 ^ (
        eax12 +
        ((eax12 * 0xa) & 0xffff)+
        ((interleaved << 3) & 0xffff) -
        (interleaved & 0xffff) +
        p2 + ((p2 << 2) & 0xffff) +
        p1 + ((p1 << 1) & 0xffff)
    ) ^ 0x342e) & 0xffff
)

while s.check() == sat:
    y = s.model()
    parts = [p1, p2, p3, p4]
    print("BRCK-"+"-".join([hex(y[p].as_long()).upper()[2:] for p in parts]))
    print()

This gives us the correct input of BRCK-D3AD-B33F-C0DE-7A55. Running the app and entering the code, we get the flag.

Flag:

dach2026{y4bb4_d4bb4_d00_1t!}

Solution#

Solution