DEF CON CTF 2016 Qualifiers のbaby-re問題のメモ

DEF CON CTF 2016 Qualifiers の baby-re の問題を解いてみた。

謎の実行ファイルとフラグ投稿用のフォームだけが与えられているので、これを解析してフラグを見つけて投稿するというのが目標。

デコンパイル

とりあえず、実行ファイルをHopperで開き、適当にmain関数とそこから呼ばれていたCheckSolution関数をデコンパイルしてみると、以下のようになった。

main.c

int main() {
    var_28 = *0x28;
    printf("Var[0]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60);
    printf(0x402a14);
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x4);
    printf("Var[2]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x8);
    printf("Var[3]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0xc);
    printf("Var[4]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x10);
    printf("Var[5]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x14);
    printf("Var[6]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x18);
    printf("Var[7]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x1c);
    printf("Var[8]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x20);
    printf("Var[9]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x24);
    printf("Var[10]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x28);
    printf("Var[11]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x2c);
    printf("Var[12]: ");
    rax = *__TMC_END__;
    fflush(rax);
    __isoc99_scanf(0x402a11, var_60 + 0x30);
    if (CheckSolution(var_60) != 0x0) {
            printf("The flag is: %c%c%c%c%c%c%c%c%c%c%c%c%c\n", var_60, var_5C, var_58, var_54, var_50, var_4C, var_48, var_44, var_40, var_3C, var_38, var_34, var_30);
    }
    else {
            puts("Wrong");
    }
    rax = 0x0;
    rbx = var_28 ^ *0x28;
    COND = rbx == 0x0;
    if (!COND) {
            rax = __stack_chk_fail();
    }
    return rax;
}

CheckSolution.c

int CheckSolution(int arg0) {
    var_2B8 = arg0;
    var_8 = *0x28;
    var_2B0 = 0x926c ^ 0x1;
    var_2AC = SAR(0x2a3a8, 0x3);
    var_2A8 = SAR(0x3a90, 0x3);
    var_2A0 = 0xc514 ^ 0xdd;
    var_298 = SAR(0x1cdc8, 0x2);
    var_294 = SAR(0x10010, 0x2);
    var_288 = 0x524c ^ 0x2e;
    var_27C = SAR(0xc6f80, 0x4);
    var_278 = SAR(0x12c90, 0x4);
    var_268 = 0x5808 ^ 0x4f;
    var_260 = SAR(0x11eee, 0x1);
    var_250 = SAR(0x90a0, 0x2);
    var_248 = SAR(0x974a0, 0x4);
    var_244 = SAR(0x19d9e, 0x1);
    var_240 = SAR(0x20f90, 0x3);
    var_234 = 0x4865 ^ 0xcc;
    var_22C = 0xb947 ^ 0xf0;
    var_21C = 0x1466 ^ 0x9d;
    var_214 = SAR(0x3864c, 0x2);
    var_210 = 0x5d02 ^ 0x53;
    var_20C = SAR(0xcb40, 0x1);
    var_1FC = SAR(0xa664, 0x2);
    var_1F8 = 0x878d ^ 0x78;
    var_1F4 = SAR(0x23d30, 0x4);
    var_1F0 = 0x59a7 ^ 0xe0;
    var_1EC = SAR(0x86b4, 0x2);
    var_1E8 = SAR(0x4f4, 0x1);
    var_1D8 = 0xabd9 ^ 0x65;
    var_1CC = SAR(0x2ffa, 0x1);
    var_1C8 = 0x8a42 ^ 0x21;
    var_1C0 = 0x6d95 ^ 0x73;
    var_1B4 = SAR(0x79b4, 0x1);
    var_1AC = SAR(0x27ce0, 0x2);
    var_1A0 = 0x13c5 ^ 0x97;
    var_19C = SAR(0x343f0, 0x3);
    var_194 = 0x9a9f ^ 0x2c;
    var_190 = 0x357e ^ 0x5c;
    var_188 = SAR(0xffc4, 0x1);
    var_184 = 0x72a3 ^ 0x3e;
    var_180 = 0x28d2 ^ 0x93;
    var_178 = SAR(0x2e62c, 0x2);
    var_16C = SAR(0x4fd6, 0x1);
    var_168 = 0x1342 ^ 0xea;
    var_164 = 0x52ed ^ 0xc2;
    var_160 = 0x73a4 ^ 0x3;
    var_15C = 0xd75a ^ 0x93;
    var_158 = SAR(0x5ec4, 0x2);
    var_154 = SAR(0xfabc, 0x2);
    var_150 = SAR(0x8e50, 0x3);
    var_144 = 0xff11 ^ 0x9a;
    var_140 = 0x438f ^ 0x98;
    var_13C = SAR(0x4984, 0x1);
    var_134 = SAR(0x33264, 0x2);
    var_130 = SAR(0x4826, 0x1);
    var_128 = SAR(0x5d928, 0x3);
    var_120 = 0xa1d6 ^ 0x9f;
    var_110 = SAR(0x1c34, 0x2);
    var_10C = 0x10fe ^ 0xd9;
    var_104 = 0x825b ^ 0x3e;
    var_100 = SAR(0x2dabc, 0x2);
    var_F4 = 0xaf41 ^ 0x39;
    var_EC = SAR(0x140c8, 0x2);
    var_E8 = SAR(0x1ea98, 0x3);
    var_E4 = 0x8e6b ^ 0x9e;
    var_DC = 0xa7ac ^ 0x11;
    var_C8 = 0x67ce ^ 0xf9;
    var_C4 = 0xb7c3 ^ 0xf;
    var_BC = SAR(0x1d5c8, 0x3);
    var_B8 = 0x4a9d ^ 0x82;
    var_B0 = 0x828e ^ 0xa9;
    var_A8 = SAR(0x24374, 0x2);
    var_A4 = 0xc95d ^ 0xdb;
    var_9C = 0x2776 ^ 0xf9;
    var_98 = SAR(0x19948, 0x1);
    var_88 = SAR(0x10268, 0x3);
    var_84 = SAR(0xb0aa, 0x1);
    var_80 = 0x7848 ^ 0x69;
    var_7C = 0x517f ^ 0xa;
    var_78 = 0x7da5 ^ 0x7d;
    var_74 = 0x8fc6 ^ 0xec;
    var_70 = 0xb910 ^ 0xde;
    var_68 = SAR(0xe72c0, 0x4);
    var_64 = 0xfe5e ^ 0xf2;
    var_60 = 0x24ef ^ 0xe3;
    var_5C = 0xe871 ^ 0xbe;
    var_58 = 0xf551 ^ 0xf9;
    var_54 = SAR(0x5f278, 0x3);
    var_40 = 0xca69 ^ 0x7e;
    var_34 = 0x101e ^ 0x18;
    var_28 = 0x5182 ^ 0xa3;
    var_24 = SAR(0xcf2a, 0x1);
    var_20 = SAR(0x1b7e4, 0x2);
    var_1C = SAR(0x62a40, 0x4);
    var_14 = SAR(0xc842, 0x1);
    var_10 = 0x1c85 ^ 0x17;
    if (*(int32_t *)(var_2B8 + 0x30) * 0xd5e5 + *(int32_t *)(var_2B8 + 0x2c) * 0x99ae + *(int32_t *)(var_2B8 + 0x28) * var_288 + *(int32_t *)(var_2B8 + 0x24) * 0x3922 + *(int32_t *)(var_2B8 + 0x20) * 0xe15d + *(int32_t *)(var_2B8 + 0x1c) * var_294 + *(int32_t *)(var_2B8 + 0x18) * var_298 + *(int32_t *)(var_2B8 + 0x14) * 0xa89e + (var_2B0 * *(int32_t *)var_2B8 - *(int32_t *)(var_2B8 + 0x4) * var_2AC - *(int32_t *)(var_2B8 + 0x8) * var_2A8 - *(int32_t *)(var_2B8 + 0xc) * 0xb4c1) + *(int32_t *)(var_2B8 + 0x10) * var_2A0 != 0x1468753) {
            rax = 0x0;
    }
    else {
            if (*(int32_t *)(var_2B8 + 0x30) * 0xcfec + (*(int32_t *)(var_2B8 + 0x14) * var_268 + *(int32_t *)(var_2B8 + 0x10) * 0x39ca + (var_27C * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * var_278 - *(int32_t *)(var_2B8 + 0x8) * 0x1783) + *(int32_t *)(var_2B8 + 0xc) * 0x9832 - *(int32_t *)(var_2B8 + 0x18) * 0x345 - *(int32_t *)(var_2B8 + 0x1c) * var_260 - *(int32_t *)(var_2B8 + 0x20) * 0xc5a0 - *(int32_t *)(var_2B8 + 0x24) * 0x2e35 - *(int32_t *)(var_2B8 + 0x28) * 0x4e4e - *(int32_t *)(var_2B8 + 0x2c) * var_250) != 0x162f30) {
                    rax = 0x0;
            }
            else {
                    if (*(int32_t *)(var_2B8 + 0x30) * 0x2ccd + *(int32_t *)(var_2B8 + 0x2c) * var_21C + (((-var_248 * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * var_244 - *(int32_t *)(var_2B8 + 0x8) * var_240) + *(int32_t *)(var_2B8 + 0xc) * 0x691b - *(int32_t *)(var_2B8 + 0x10) * 0xad9e - *(int32_t *)(var_2B8 + 0x14) * var_234 - *(int32_t *)(var_2B8 + 0x18) * 0xfec5 - *(int32_t *)(var_2B8 + 0x1c) * var_22C) + *(int32_t *)(var_2B8 + 0x20) * 0x4526 - *(int32_t *)(var_2B8 + 0x24) * 0x8476) + *(int32_t *)(var_2B8 + 0x28) * 0xa69e != 0xffb2939c) {
                            rax = 0x0;
                    }
                    else {
                            if ((*(int32_t *)(var_2B8 + 0x1c) * var_1F8 + ((var_214 * *(int32_t *)var_2B8 - *(int32_t *)(var_2B8 + 0x4) * var_210 - *(int32_t *)(var_2B8 + 0x8) * var_20C - *(int32_t *)(var_2B8 + 0xc) * 0x6252) + *(int32_t *)(var_2B8 + 0x10) * 0xd42d - *(int32_t *)(var_2B8 + 0x14) * 0x7e51) + *(int32_t *)(var_2B8 + 0x18) * var_1FC - *(int32_t *)(var_2B8 + 0x20) * var_1F4 - *(int32_t *)(var_2B8 + 0x24) * var_1F0) + *(int32_t *)(var_2B8 + 0x28) * var_1EC - *(int32_t *)(var_2B8 + 0x2c) * var_1E8 - *(int32_t *)(var_2B8 + 0x30) * 0x2e58 != 0xffac90e3) {
                                    rax = 0x0;
                            }
                            else {
                                    if (*(int32_t *)(var_2B8 + 0x30) * 0xc3a2 + (*(int32_t *)(var_2B8 + 0x24) * 0xa8b2 + (*(int32_t *)(var_2B8 + 0x10) * 0xd669 + *(int32_t *)(var_2B8 + 0xc) * 0x876e + *(int32_t *)(var_2B8 + 0x8) * var_1D8 + -0x36b5 * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * 0x3fc3 - *(int32_t *)(var_2B8 + 0x14) * var_1CC - *(int32_t *)(var_2B8 + 0x18) * var_1C8 - *(int32_t *)(var_2B8 + 0x1c) * 0xf219) + *(int32_t *)(var_2B8 + 0x20) * var_1C0 - *(int32_t *)(var_2B8 + 0x28) * 0xe91c) + *(int32_t *)(var_2B8 + 0x2c) * var_1B4 != 0x76d288) {
                                            rax = 0x0;
                                    }
                                    else {
                                            if (*(int32_t *)(var_2B8 + 0x2c) * var_180 + (*(int32_t *)(var_2B8 + 0x1c) * var_190 + ((-var_1AC * *(int32_t *)var_2B8 - *(int32_t *)(var_2B8 + 0x4) * 0x55fe) + *(int32_t *)(var_2B8 + 0x8) * 0x3528 - *(int32_t *)(var_2B8 + 0xc) * var_1A0 - *(int32_t *)(var_2B8 + 0x10) * var_19C - *(int32_t *)(var_2B8 + 0x14) * 0x7bdc) + *(int32_t *)(var_2B8 + 0x18) * var_194 - *(int32_t *)(var_2B8 + 0x20) * 0xe6af - *(int32_t *)(var_2B8 + 0x24) * var_188) + *(int32_t *)(var_2B8 + 0x28) * var_184 - *(int32_t *)(var_2B8 + 0x30) * 0x3d22 != 0xff78bf99) {
                                                    rax = 0x0;
                                            }
                                            else {
                                                    if (*(int32_t *)(var_2B8 + 0x30) * 0x49d7 + (((*(int32_t *)(var_2B8 + 0x8) * 0x34a5 + -var_178 * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * 0xe200 - *(int32_t *)(var_2B8 + 0xc) * var_16C - *(int32_t *)(var_2B8 + 0x10) * var_168 - *(int32_t *)(var_2B8 + 0x14) * var_164 - *(int32_t *)(var_2B8 + 0x18) * var_160) + *(int32_t *)(var_2B8 + 0x1c) * var_15C - *(int32_t *)(var_2B8 + 0x20) * var_158) + *(int32_t *)(var_2B8 + 0x24) * var_154 - *(int32_t *)(var_2B8 + 0x28) * var_150 - *(int32_t *)(var_2B8 + 0x2c) * 0x8d6) != 0xfff496e3) {
                                                            rax = 0x0;
                                                    }
                                                    else {
                                                            if ((*(int32_t *)(var_2B8 + 0x1c) * var_128 + (-var_144 * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * var_140 - *(int32_t *)(var_2B8 + 0x8) * var_13C - *(int32_t *)(var_2B8 + 0xc) * 0x57f2 - *(int32_t *)(var_2B8 + 0x10) * var_134 - *(int32_t *)(var_2B8 + 0x14) * var_130) + *(int32_t *)(var_2B8 + 0x18) * 0xd03d - *(int32_t *)(var_2B8 + 0x20) * 0xe6e7 - *(int32_t *)(var_2B8 + 0x24) * var_120 - *(int32_t *)(var_2B8 + 0x28) * 0x5f66) + *(int32_t *)(var_2B8 + 0x2c) * 0xa0da - *(int32_t *)(var_2B8 + 0x30) * 0x5b97 != 0xff525e90) {
                                                                    rax = 0x0;
                                                            }
                                                            else {
                                                                    if (*(int32_t *)(var_2B8 + 0x30) * 0x4737 + ((*(int32_t *)(var_2B8 + 0x14) * 0xe4b7 + *(int32_t *)(var_2B8 + 0x10) * var_100 + (var_110 * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * var_10C - *(int32_t *)(var_2B8 + 0x8) * 0x4204) + *(int32_t *)(var_2B8 + 0xc) * var_104 - *(int32_t *)(var_2B8 + 0x18) * 0x8546 - *(int32_t *)(var_2B8 + 0x1c) * var_F4 - *(int32_t *)(var_2B8 + 0x20) * 0x2e9d - *(int32_t *)(var_2B8 + 0x24) * var_EC) + *(int32_t *)(var_2B8 + 0x28) * var_E8 - *(int32_t *)(var_2B8 + 0x2c) * var_E4) != 0xfffd7704) {
                                                                            rax = 0x0;
                                                                    }
                                                                    else {
                                                                            if (*(int32_t *)(var_2B8 + 0x30) * 0xf8c0 + (*(int32_t *)(var_2B8 + 0x28) * 0x2a24 + *(int32_t *)(var_2B8 + 0x24) * var_B8 + *(int32_t *)(var_2B8 + 0x20) * var_BC + *(int32_t *)(var_2B8 + 0x1c) * 0xa57b + ((-var_DC * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * 0xee80 - *(int32_t *)(var_2B8 + 0x8) * 0xb071) + *(int32_t *)(var_2B8 + 0xc) * 0xa144 - *(int32_t *)(var_2B8 + 0x10) * 0x6ba - *(int32_t *)(var_2B8 + 0x14) * var_C8) + *(int32_t *)(var_2B8 + 0x18) * var_C4 - *(int32_t *)(var_2B8 + 0x2c) * var_B0) != 0x897cbb) {
                                                                                    rax = 0x0;
                                                                            }
                                                                            else {
                                                                                    if (*(int32_t *)(var_2B8 + 0x30) * var_78 + (*(int32_t *)(var_2B8 + 0x28) * var_80 + (*(int32_t *)(var_2B8 + 0x1c) * 0xe5a2 + *(int32_t *)(var_2B8 + 0x18) * 0x312b + (-var_A8 * *(int32_t *)var_2B8 - *(int32_t *)(var_2B8 + 0x4) * var_A4 - *(int32_t *)(var_2B8 + 0x8) * 0x4586 - *(int32_t *)(var_2B8 + 0xc) * var_9C - *(int32_t *)(var_2B8 + 0x10) * var_98) + *(int32_t *)(var_2B8 + 0x14) * 0x31ca - *(int32_t *)(var_2B8 + 0x20) * var_88) + *(int32_t *)(var_2B8 + 0x24) * var_84 - *(int32_t *)(var_2B8 + 0x2c) * var_7C) != 0xffc05f9f) {
                                                                                            rax = 0x0;
                                                                                    }
                                                                                    else {
                                                                                            if (*(int32_t *)(var_2B8 + 0x30) * 0x9e3e + (*(int32_t *)(var_2B8 + 0x24) * 0xb8f4 + (*(int32_t *)(var_2B8 + 0x14) * var_60 + (var_74 * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * var_70 - *(int32_t *)(var_2B8 + 0x8) * 0x8202 - *(int32_t *)(var_2B8 + 0xc) * var_68) + *(int32_t *)(var_2B8 + 0x10) * var_64 - *(int32_t *)(var_2B8 + 0x18) * var_5C - *(int32_t *)(var_2B8 + 0x1c) * var_58) + *(int32_t *)(var_2B8 + 0x20) * var_54 - *(int32_t *)(var_2B8 + 0x28) * 0x92d8) + *(int32_t *)(var_2B8 + 0x2c) * 0xe10c != 0x3e4761) {
                                                                                                    rax = 0x0;
                                                                                            }
                                                                                            else {
                                                                                                    if (*(int32_t *)(var_2B8 + 0x30) * var_10 + (*(int32_t *)(var_2B8 + 0x24) * var_1C + *(int32_t *)(var_2B8 + 0x20) * var_20 + (*(int32_t *)(var_2B8 + 0x10) * 0xe877 + (var_40 * *(int32_t *)var_2B8 + *(int32_t *)(var_2B8 + 0x4) * 0x8c27 - *(int32_t *)(var_2B8 + 0x8) * 0xf992) + *(int32_t *)(var_2B8 + 0xc) * var_34 - *(int32_t *)(var_2B8 + 0x14) * 0x538a - *(int32_t *)(var_2B8 + 0x18) * var_28) + *(int32_t *)(var_2B8 + 0x1c) * var_24 - *(int32_t *)(var_2B8 + 0x28) * 0xab0d) + *(int32_t *)(var_2B8 + 0x2c) * var_14 != 0x1b4945) {
                                                                                                            rax = 0x0;
                                                                                                    }
                                                                                                    else {
                                                                                                            rax = 0x1;
                                                                                                    }
                                                                                            }
                                                                                    }
                                                                            }
                                                                    }
                                                            }
                                                    }
                                            }
                                    }
                            }
                    }
            }
    }
    rsi = var_8 ^ *0x28;
    COND = rsi == 0x0;
    if (!COND) {
            rax = __stack_chk_fail();
    }
    return rax;
}

連立方程式の作成

CheckSolutionの中身を読むと、各if文の比較が「≠」になると0が返り、その場合にはmainで「Wrong」となることが分かる。逆に、すべてのif文の比較が「=」になるような入力が求まれば、それがmainでフラグとしてprintfで表示される。

CheckSolution の引数として渡される入力に関して Var[0],…,Var[12] に戻したうえで、これら条件を連立方程式として書き表すと、以下の様な感じになる。

var_2B0 = 0x926c ^ 0x1;
var_2AC = SAR(0x2a3a8, 0x3);
var_2A8 = SAR(0x3a90, 0x3);
var_2A0 = 0xc514 ^ 0xdd;
var_298 = SAR(0x1cdc8, 0x2);
var_294 = SAR(0x10010, 0x2);
var_288 = 0x524c ^ 0x2e;
var_27C = SAR(0xc6f80, 0x4);
var_278 = SAR(0x12c90, 0x4);
var_268 = 0x5808 ^ 0x4f;
var_260 = SAR(0x11eee, 0x1);
var_250 = SAR(0x90a0, 0x2);
var_248 = SAR(0x974a0, 0x4);
var_244 = SAR(0x19d9e, 0x1);
var_240 = SAR(0x20f90, 0x3);
var_234 = 0x4865 ^ 0xcc;
var_22C = 0xb947 ^ 0xf0;
var_21C = 0x1466 ^ 0x9d;
var_214 = SAR(0x3864c, 0x2);
var_210 = 0x5d02 ^ 0x53;
var_20C = SAR(0xcb40, 0x1);
var_1FC = SAR(0xa664, 0x2);
var_1F8 = 0x878d ^ 0x78;
var_1F4 = SAR(0x23d30, 0x4);
var_1F0 = 0x59a7 ^ 0xe0;
var_1EC = SAR(0x86b4, 0x2);
var_1E8 = SAR(0x4f4, 0x1);
var_1D8 = 0xabd9 ^ 0x65;
var_1CC = SAR(0x2ffa, 0x1);
var_1C8 = 0x8a42 ^ 0x21;
var_1C0 = 0x6d95 ^ 0x73;
var_1B4 = SAR(0x79b4, 0x1);
var_1AC = SAR(0x27ce0, 0x2);
var_1A0 = 0x13c5 ^ 0x97;
var_19C = SAR(0x343f0, 0x3);
var_194 = 0x9a9f ^ 0x2c;
var_190 = 0x357e ^ 0x5c;
var_188 = SAR(0xffc4, 0x1);
var_184 = 0x72a3 ^ 0x3e;
var_180 = 0x28d2 ^ 0x93;
var_178 = SAR(0x2e62c, 0x2);
var_16C = SAR(0x4fd6, 0x1);
var_168 = 0x1342 ^ 0xea;
var_164 = 0x52ed ^ 0xc2;
var_160 = 0x73a4 ^ 0x3;
var_15C = 0xd75a ^ 0x93;
var_158 = SAR(0x5ec4, 0x2);
var_154 = SAR(0xfabc, 0x2);
var_150 = SAR(0x8e50, 0x3);
var_144 = 0xff11 ^ 0x9a;
var_140 = 0x438f ^ 0x98;
var_13C = SAR(0x4984, 0x1);
var_134 = SAR(0x33264, 0x2);
var_130 = SAR(0x4826, 0x1);
var_128 = SAR(0x5d928, 0x3);
var_120 = 0xa1d6 ^ 0x9f;
var_110 = SAR(0x1c34, 0x2);
var_10C = 0x10fe ^ 0xd9;
var_104 = 0x825b ^ 0x3e;
var_100 = SAR(0x2dabc, 0x2);
var_F4 = 0xaf41 ^ 0x39;
var_EC = SAR(0x140c8, 0x2);
var_E8 = SAR(0x1ea98, 0x3);
var_E4 = 0x8e6b ^ 0x9e;
var_DC = 0xa7ac ^ 0x11;
var_C8 = 0x67ce ^ 0xf9;
var_C4 = 0xb7c3 ^ 0xf;
var_BC = SAR(0x1d5c8, 0x3);
var_B8 = 0x4a9d ^ 0x82;
var_B0 = 0x828e ^ 0xa9;
var_A8 = SAR(0x24374, 0x2);
var_A4 = 0xc95d ^ 0xdb;
var_9C = 0x2776 ^ 0xf9;
var_98 = SAR(0x19948, 0x1);
var_88 = SAR(0x10268, 0x3);
var_84 = SAR(0xb0aa, 0x1);
var_80 = 0x7848 ^ 0x69;
var_7C = 0x517f ^ 0xa;
var_78 = 0x7da5 ^ 0x7d;
var_74 = 0x8fc6 ^ 0xec;
var_70 = 0xb910 ^ 0xde;
var_68 = SAR(0xe72c0, 0x4);
var_64 = 0xfe5e ^ 0xf2;
var_60 = 0x24ef ^ 0xe3;
var_5C = 0xe871 ^ 0xbe;
var_58 = 0xf551 ^ 0xf9;
var_54 = SAR(0x5f278, 0x3);
var_40 = 0xca69 ^ 0x7e;
var_34 = 0x101e ^ 0x18;
var_28 = 0x5182 ^ 0xa3;
var_24 = SAR(0xcf2a, 0x1);
var_20 = SAR(0x1b7e4, 0x2);
var_1C = SAR(0x62a40, 0x4);
var_14 = SAR(0xc842, 0x1);
var_10 = 0x1c85 ^ 0x17;

Var[12] * 0xd5e5 + Var[11] * 0x99ae + Var[10] * var_288 + Var[9] * 0x3922 + Var[8] * 0xe15d + Var[7] * var_294 + Var[6] * var_298 + Var[5] * 0xa89e + (var_2B0 * Var[0] - Var[1] * var_2AC - Var[2] * var_2A8 - Var[3] * 0xb4c1) + Var[4] * var_2A0 == 0x1468753
Var[12] * 0xcfec + (Var[5] * var_268 + Var[4] * 0x39ca + (var_27C * Var[0] + Var[1] * var_278 - Var[2] * 0x1783) + Var[3] * 0x9832 - Var[6] * 0x345 - Var[7] * var_260 - Var[8] * 0xc5a0 - Var[9] * 0x2e35 - Var[10] * 0x4e4e - Var[11] * var_250) == 0x162f30
Var[12] * 0x2ccd + Var[11] * var_21C + (((-var_248 * Var[0] + Var[1] * var_244 - Var[2] * var_240) + Var[3] * 0x691b - Var[4] * 0xad9e - Var[5] * var_234 - Var[6] * 0xfec5 - Var[7] * var_22C) + Var[8] * 0x4526 - Var[9] * 0x8476) + Var[10] * 0xa69e == 0xffb2939c
Var[7] * var_1F8 + ((var_214 * Var[0] - Var[1] * var_210 - Var[2] * var_20C - Var[3] * 0x6252) + Var[4] * 0xd42d - Var[5] * 0x7e51) + Var[6] * var_1FC - Var[8] * var_1F4 - Var[9] * var_1F0) + Var[10] * var_1EC - Var[11] * var_1E8 - Var[12] * 0x2e58 == 0xffac90e3
Var[12] * 0xc3a2 + (Var[9] * 0xa8b2 + (Var[4] * 0xd669 + Var[3] * 0x876e + Var[2] * var_1D8 + -0x36b5 * Var[0] + Var[1] * 0x3fc3 - Var[5] * var_1CC - Var[6] * var_1C8 - Var[7] * 0xf219) + Var[8] * var_1C0 - Var[10] * 0xe91c) + Var[11] * var_1B4 == 0x76d288
Var[11] * var_180 + (Var[7] * var_190 + ((-var_1AC * Var[0] - Var[1] * 0x55fe) + Var[2] * 0x3528 - Var[3] * var_1A0 - Var[4] * var_19C - Var[5] * 0x7bdc) + Var[6] * var_194 - Var[8] * 0xe6af - Var[9] * var_188) + Var[10] * var_184 - Var[12] * 0x3d22 == 0xff78bf99
Var[12] * 0x49d7 + (((Var[2] * 0x34a5 + -var_178 * Var[0] + Var[1] * 0xe200 - Var[3] * var_16C - Var[4] * var_168 - Var[5] * var_164 - Var[6] * var_160) + Var[7] * var_15C - Var[8] * var_158) + Var[9] * var_154 - Var[10] * var_150 - Var[11] * 0x8d6) == 0xfff496e3
(Var[7] * var_128 + (-var_144 * Var[0] + Var[1] * var_140 - Var[2] * var_13C - Var[3] * 0x57f2 - Var[4] * var_134 - Var[5] * var_130) + Var[6] * 0xd03d - Var[8] * 0xe6e7 - Var[9] * var_120 - Var[10] * 0x5f66) + Var[11] * 0xa0da - Var[12] * 0x5b97 == 0xff525e90
Var[12] * 0x4737 + ((Var[5] * 0xe4b7 + Var[4] * var_100 + (var_110 * Var[0] + Var[1] * var_10C - Var[2] * 0x4204) + Var[3] * var_104 - Var[6] * 0x8546 - Var[7] * var_F4 - Var[8] * 0x2e9d - Var[9] * var_EC) + Var[10] * var_E8 - Var[11] * var_E4) == 0xfffd7704
Var[12] * 0xf8c0 + (Var[10] * 0x2a24 + Var[9] * var_B8 + Var[8] * var_BC + Var[7] * 0xa57b + ((-var_DC * Var[0] + Var[1] * 0xee80 - Var[2] * 0xb071) + Var[3] * 0xa144 - Var[4] * 0x6ba - Var[5] * var_C8) + Var[6] * var_C4 - Var[11] * var_B0) == 0x897cbb
Var[12] * var_78 + (Var[10] * var_80 + (Var[7] * 0xe5a2 + Var[6] * 0x312b + (-var_A8 * Var[0] - Var[1] * var_A4 - Var[2] * 0x4586 - Var[3] * var_9C - Var[4] * var_98) + Var[5] * 0x31ca - Var[8] * var_88) + Var[9] * var_84 - Var[11] * var_7C) == 0xffc05f9f
Var[12] * 0x9e3e + (Var[9] * 0xb8f4 + (Var[5] * var_60 + (var_74 * Var[0] + Var[1] * var_70 - Var[2] * 0x8202 - Var[3] * var_68) + Var[4] * var_64 - Var[6] * var_5C - Var[7] * var_58) + Var[8] * var_54 - Var[10] * 0x92d8) + Var[11] * 0xe10c == 0x3e4761
Var[12] * var_10 + (Var[9] * var_1C + Var[8] * var_20 + (Var[4] * 0xe877 + (var_40 * Var[0] + Var[1] * 0x8c27 - Var[2] * 0xf992) + Var[3] * var_34 - Var[5] * 0x538a - Var[6] * var_28) + Var[7] * var_24 - Var[10] * 0xab0d) + Var[11] * var_14 == 0x1b4945

これを解いて、printf("The flag is: %c%c%c%c%c%c%c%c%c%c%c%c%c\n", Var[0], Var[1], Var[2], Var[3], Var[4], Var[5], Var[6], Var[7], Var[8], Var[9], Var[10], Var[11], Var[12]);とすれば良さそうである。

連立方程式を解く

この連立方程式を解くべく、CVC4 向けに以下の様なファイルを生成。エディタの置換機能と簡単なスクリプトで変換したが、このファイルを作成するのがこの問題を解く中で一番時間のかかった部分だった。

OPTION "produce-models";

Var__0, Var__1, Var__2, Var__3, Var__4, Var__5, Var__6, Var__7, Var__8, Var__9, Var__10, Var__11, Var__12 : BITVECTOR(32);

var_2B0 : BITVECTOR(32) = BVXOR(0hex0000926c, 0hex00000001);
var_2AC : BITVECTOR(32) = 0hex0002a3a8 >> 3;
var_2A8 : BITVECTOR(32) = 0hex00003a90 >> 3;
var_2A0 : BITVECTOR(32) = BVXOR(0hex0000c514, 0hex000000dd);
var_298 : BITVECTOR(32) = 0hex0001cdc8 >> 2;
var_294 : BITVECTOR(32) = 0hex00010010 >> 2;
var_288 : BITVECTOR(32) = BVXOR(0hex0000524c, 0hex0000002e);
var_27C : BITVECTOR(32) = 0hex000c6f80 >> 4;
var_278 : BITVECTOR(32) = 0hex00012c90 >> 4;
var_268 : BITVECTOR(32) = BVXOR(0hex00005808, 0hex0000004f);
var_260 : BITVECTOR(32) = 0hex00011eee >> 1;
var_250 : BITVECTOR(32) = 0hex000090a0 >> 2;
var_248 : BITVECTOR(32) = 0hex000974a0 >> 4;
var_244 : BITVECTOR(32) = 0hex00019d9e >> 1;
var_240 : BITVECTOR(32) = 0hex00020f90 >> 3;
var_234 : BITVECTOR(32) = BVXOR(0hex00004865, 0hex000000cc);
var_22C : BITVECTOR(32) = BVXOR(0hex0000b947, 0hex000000f0);
var_21C : BITVECTOR(32) = BVXOR(0hex00001466, 0hex0000009d);
var_214 : BITVECTOR(32) = 0hex0003864c >> 2;
var_210 : BITVECTOR(32) = BVXOR(0hex00005d02, 0hex00000053);
var_20C : BITVECTOR(32) = 0hex0000cb40 >> 1;
var_1FC : BITVECTOR(32) = 0hex0000a664 >> 2;
var_1F8 : BITVECTOR(32) = BVXOR(0hex0000878d, 0hex00000078);
var_1F4 : BITVECTOR(32) = 0hex00023d30 >> 4;
var_1F0 : BITVECTOR(32) = BVXOR(0hex000059a7, 0hex000000e0);
var_1EC : BITVECTOR(32) = 0hex000086b4 >> 2;
var_1E8 : BITVECTOR(32) = 0hex000004f4 >> 1;
var_1D8 : BITVECTOR(32) = BVXOR(0hex0000abd9, 0hex00000065);
var_1CC : BITVECTOR(32) = 0hex00002ffa >> 1;
var_1C8 : BITVECTOR(32) = BVXOR(0hex00008a42, 0hex00000021);
var_1C0 : BITVECTOR(32) = BVXOR(0hex00006d95, 0hex00000073);
var_1B4 : BITVECTOR(32) = 0hex000079b4 >> 1;
var_1AC : BITVECTOR(32) = 0hex00027ce0 >> 2;
var_1A0 : BITVECTOR(32) = BVXOR(0hex000013c5, 0hex00000097);
var_19C : BITVECTOR(32) = 0hex000343f0 >> 3;
var_194 : BITVECTOR(32) = BVXOR(0hex00009a9f, 0hex0000002c);
var_190 : BITVECTOR(32) = BVXOR(0hex0000357e, 0hex0000005c);
var_188 : BITVECTOR(32) = 0hex0000ffc4 >> 1;
var_184 : BITVECTOR(32) = BVXOR(0hex000072a3, 0hex0000003e);
var_180 : BITVECTOR(32) = BVXOR(0hex000028d2, 0hex00000093);
var_178 : BITVECTOR(32) = 0hex0002e62c >> 2;
var_16C : BITVECTOR(32) = 0hex00004fd6 >> 1;
var_168 : BITVECTOR(32) = BVXOR(0hex00001342, 0hex000000ea);
var_164 : BITVECTOR(32) = BVXOR(0hex000052ed, 0hex000000c2);
var_160 : BITVECTOR(32) = BVXOR(0hex000073a4, 0hex00000003);
var_15C : BITVECTOR(32) = BVXOR(0hex0000d75a, 0hex00000093);
var_158 : BITVECTOR(32) = 0hex00005ec4 >> 2;
var_154 : BITVECTOR(32) = 0hex0000fabc >> 2;
var_150 : BITVECTOR(32) = 0hex00008e50 >> 3;
var_144 : BITVECTOR(32) = BVXOR(0hex0000ff11, 0hex0000009a);
var_140 : BITVECTOR(32) = BVXOR(0hex0000438f, 0hex00000098);
var_13C : BITVECTOR(32) = 0hex00004984 >> 1;
var_134 : BITVECTOR(32) = 0hex00033264 >> 2;
var_130 : BITVECTOR(32) = 0hex00004826 >> 1;
var_128 : BITVECTOR(32) = 0hex0005d928 >> 3;
var_120 : BITVECTOR(32) = BVXOR(0hex0000a1d6, 0hex0000009f);
var_110 : BITVECTOR(32) = 0hex00001c34 >> 2;
var_10C : BITVECTOR(32) = BVXOR(0hex000010fe, 0hex000000d9);
var_104 : BITVECTOR(32) = BVXOR(0hex0000825b, 0hex0000003e);
var_100 : BITVECTOR(32) = 0hex0002dabc >> 2;
var_F4 : BITVECTOR(32) = BVXOR(0hex0000af41, 0hex00000039);
var_EC : BITVECTOR(32) = 0hex000140c8 >> 2;
var_E8 : BITVECTOR(32) = 0hex0001ea98 >> 3;
var_E4 : BITVECTOR(32) = BVXOR(0hex00008e6b, 0hex0000009e);
var_DC : BITVECTOR(32) = BVXOR(0hex0000a7ac, 0hex00000011);
var_C8 : BITVECTOR(32) = BVXOR(0hex000067ce, 0hex000000f9);
var_C4 : BITVECTOR(32) = BVXOR(0hex0000b7c3, 0hex0000000f);
var_BC : BITVECTOR(32) = 0hex0001d5c8 >> 3;
var_B8 : BITVECTOR(32) = BVXOR(0hex00004a9d, 0hex00000082);
var_B0 : BITVECTOR(32) = BVXOR(0hex0000828e, 0hex000000a9);
var_A8 : BITVECTOR(32) = 0hex00024374 >> 2;
var_A4 : BITVECTOR(32) = BVXOR(0hex0000c95d, 0hex000000db);
var_9C : BITVECTOR(32) = BVXOR(0hex00002776, 0hex000000f9);
var_98 : BITVECTOR(32) = 0hex00019948 >> 1;
var_88 : BITVECTOR(32) = 0hex00010268 >> 3;
var_84 : BITVECTOR(32) = 0hex0000b0aa >> 1;
var_80 : BITVECTOR(32) = BVXOR(0hex00007848, 0hex00000069);
var_7C : BITVECTOR(32) = BVXOR(0hex0000517f, 0hex0000000a);
var_78 : BITVECTOR(32) = BVXOR(0hex00007da5, 0hex0000007d);
var_74 : BITVECTOR(32) = BVXOR(0hex00008fc6, 0hex000000ec);
var_70 : BITVECTOR(32) = BVXOR(0hex0000b910, 0hex000000de);
var_68 : BITVECTOR(32) = 0hex000e72c0 >> 4;
var_64 : BITVECTOR(32) = BVXOR(0hex0000fe5e, 0hex000000f2);
var_60 : BITVECTOR(32) = BVXOR(0hex000024ef, 0hex000000e3);
var_5C : BITVECTOR(32) = BVXOR(0hex0000e871, 0hex000000be);
var_58 : BITVECTOR(32) = BVXOR(0hex0000f551, 0hex000000f9);
var_54 : BITVECTOR(32) = 0hex0005f278 >> 3;
var_40 : BITVECTOR(32) = BVXOR(0hex0000ca69, 0hex0000007e);
var_34 : BITVECTOR(32) = BVXOR(0hex0000101e, 0hex00000018);
var_28 : BITVECTOR(32) = BVXOR(0hex00005182, 0hex000000a3);
var_24 : BITVECTOR(32) = 0hex0000cf2a >> 1;
var_20 : BITVECTOR(32) = 0hex0001b7e4 >> 2;
var_1C : BITVECTOR(32) = 0hex00062a40 >> 4;
var_14 : BITVECTOR(32) = 0hex0000c842 >> 1;
var_10 : BITVECTOR(32) = BVXOR(0hex00001c85, 0hex00000017);

ASSERT BVPLUS(32, BVMULT(32,Var__12,0hex0000d5e5), BVMULT(32,Var__11,0hex000099ae), BVMULT(32,Var__10,var_288), BVMULT(32,Var__9,0hex00003922), BVMULT(32,Var__8,0hex0000e15d), BVMULT(32,Var__7,var_294), BVMULT(32,Var__6,var_298), BVMULT(32,Var__5,0hex0000a89e), BVMULT(32,var_2B0,Var__0), BVUMINUS(BVMULT(32,Var__1,var_2AC)), BVUMINUS(BVMULT(32,Var__2,var_2A8)), BVUMINUS(BVMULT(32,Var__3,0hex0000b4c1)), BVMULT(32,Var__4,var_2A0)) = 0hex01468753;

ASSERT BVPLUS(32, BVMULT(32,Var__12,0hex0000cfec), BVMULT(32,Var__5,var_268), BVMULT(32,Var__4,0hex000039ca), BVMULT(32,var_27C,Var__0), BVMULT(32,Var__1,var_278), BVUMINUS(BVMULT(32,Var__2,0hex00001783)), BVMULT(32,Var__3,0hex00009832), BVUMINUS(BVMULT(32,Var__6,0hex00000345)), BVUMINUS(BVMULT(32,Var__7,var_260)), BVUMINUS(BVMULT(32,Var__8,0hex0000c5a0)), BVUMINUS(BVMULT(32,Var__9,0hex00002e35)), BVUMINUS(BVMULT(32,Var__10,0hex00004e4e)), BVUMINUS(BVMULT(32,Var__11,var_250))) = 0hex00162f30;

ASSERT BVPLUS(32, BVMULT(32,Var__12,0hex00002ccd), BVMULT(32,Var__11,var_21C), BVMULT(32,BVUMINUS(var_248),Var__0),  BVMULT(32,Var__1,var_244), BVUMINUS(BVMULT(32,Var__2,var_240)), BVMULT(32,Var__3,0hex0000691b), BVUMINUS(BVMULT(32,Var__4,0hex0000ad9e)), BVUMINUS(BVMULT(32,Var__5,var_234)), BVUMINUS(BVMULT(32,Var__6,0hex0000fec5)), BVUMINUS(BVMULT(32,Var__7,var_22C)), BVMULT(32,Var__8,0hex00004526), BVUMINUS(BVMULT(32,Var__9,0hex00008476)), BVMULT(32,Var__10,0hex0000a69e)) = 0hexffb2939c;

ASSERT BVPLUS(32, BVMULT(32,Var__7,var_1F8), BVMULT(32,var_214,Var__0), BVUMINUS(BVMULT(32,Var__1,var_210)), BVUMINUS(BVMULT(32,Var__2,var_20C)), BVUMINUS(BVMULT(32,Var__3,0hex00006252)), BVMULT(32,Var__4,0hex0000d42d), BVUMINUS(BVMULT(32,Var__5,0hex00007e51)), BVMULT(32,Var__6,var_1FC), BVUMINUS(BVMULT(32,Var__8,var_1F4)), BVUMINUS(BVMULT(32,Var__9,var_1F0)), BVMULT(32,Var__10,var_1EC), BVUMINUS(BVMULT(32,Var__11,var_1E8)), BVUMINUS(BVMULT(32,Var__12,0hex00002e58))) = 0hexffac90e3;

ASSERT BVPLUS(32, BVMULT(32,Var__12,0hex0000c3a2), BVMULT(32,Var__9,0hex0000a8b2), BVMULT(32,Var__4,0hex0000d669), BVMULT(32,Var__3,0hex0000876e), BVMULT(32,Var__2,var_1D8), BVUMINUS(BVMULT(32,0hex000036b5,Var__0)), BVMULT(32,Var__1,0hex00003fc3), BVUMINUS(BVMULT(32,Var__5,var_1CC)), BVUMINUS(BVMULT(32,Var__6,var_1C8)), BVUMINUS(BVMULT(32,Var__7,0hex0000f219)), BVMULT(32,Var__8,var_1C0), BVUMINUS(BVMULT(32,Var__10,0hex0000e91c)), BVMULT(32,Var__11,var_1B4)) = 0hex0076d288;

ASSERT BVPLUS(32, BVMULT(32,Var__11,var_180), BVMULT(32,Var__7,var_190), BVUMINUS(BVMULT(32,var_1AC,Var__0)), BVUMINUS(BVMULT(32,Var__1,0hex000055fe)), BVMULT(32,Var__2,0hex00003528), BVUMINUS(BVMULT(32,Var__3,var_1A0)), BVUMINUS(BVMULT(32,Var__4,var_19C)), BVUMINUS(BVMULT(32,Var__5,0hex00007bdc)), BVMULT(32,Var__6,var_194), BVUMINUS(BVMULT(32,Var__8,0hex0000e6af)), BVUMINUS(BVMULT(32,Var__9,var_188)), BVMULT(32,Var__10,var_184), BVUMINUS(BVMULT(32,Var__12,0hex00003d22))) = 0hexff78bf99;

ASSERT BVPLUS(32, BVMULT(32,Var__12,0hex000049d7), BVMULT(32,Var__2,0hex000034a5), BVUMINUS(BVMULT(32,var_178,Var__0)), BVMULT(32,Var__1,0hex0000e200), BVUMINUS(BVMULT(32,Var__3,var_16C)), BVUMINUS(BVMULT(32,Var__4,var_168)), BVUMINUS(BVMULT(32,Var__5,var_164)), BVUMINUS(BVMULT(32,Var__6,var_160)), BVMULT(32,Var__7,var_15C), BVUMINUS(BVMULT(32,Var__8,var_158)), BVMULT(32,Var__9,var_154), BVUMINUS(BVMULT(32,Var__10,var_150)), BVUMINUS(BVMULT(32,Var__11,0hex000008d6))) = 0hexfff496e3;

ASSERT BVPLUS(32, BVMULT(32,Var__7,var_128), BVUMINUS(BVMULT(32,var_144,Var__0)), BVMULT(32,Var__1,var_140), BVUMINUS(BVMULT(32,Var__2,var_13C)), BVUMINUS(BVMULT(32,Var__3,0hex000057f2)), BVUMINUS(BVMULT(32,Var__4,var_134)), BVUMINUS(BVMULT(32,Var__5,var_130)), BVMULT(32,Var__6,0hex0000d03d), BVUMINUS(BVMULT(32,Var__8,0hex0000e6e7)), BVUMINUS(BVMULT(32,Var__9,var_120)), BVUMINUS(BVMULT(32,Var__10,0hex00005f66)), BVMULT(32,Var__11,0hex0000a0da), BVUMINUS(BVMULT(32,Var__12,0hex00005b97))) = 0hexff525e90;

ASSERT BVPLUS(32, BVMULT(32,Var__12,0hex00004737), BVMULT(32,Var__5,0hex0000e4b7), BVMULT(32,Var__4,var_100), BVMULT(32,var_110,Var__0), BVMULT(32,Var__1,var_10C), BVUMINUS(BVMULT(32,Var__2,0hex00004204)), BVMULT(32,Var__3,var_104), BVUMINUS(BVMULT(32,Var__6,0hex00008546)), BVUMINUS(BVMULT(32,Var__7,var_F4)), BVUMINUS(BVMULT(32,Var__8,0hex00002e9d)), BVUMINUS(BVMULT(32,Var__9,var_EC)), BVMULT(32,Var__10,var_E8), BVUMINUS(BVMULT(32,Var__11,var_E4))) = 0hexfffd7704;

ASSERT BVPLUS(32, BVMULT(32,Var__12,0hex0000f8c0), BVMULT(32,Var__10,0hex00002a24), BVMULT(32,Var__9,var_B8), BVMULT(32,Var__8,var_BC), BVMULT(32,Var__7,0hex0000a57b), BVUMINUS(BVMULT(32,var_DC,Var__0)), BVMULT(32,Var__1,0hex0000ee80), BVUMINUS(BVMULT(32,Var__2,0hex0000b071)), BVMULT(32,Var__3,0hex0000a144), BVUMINUS(BVMULT(32,Var__4,0hex000006ba)), BVUMINUS(BVMULT(32,Var__5,var_C8)), BVMULT(32,Var__6,var_C4), BVUMINUS(BVMULT(32,Var__11,var_B0))) = 0hex00897cbb;

ASSERT BVPLUS(32, BVMULT(32,Var__12,var_78), BVMULT(32,Var__10,var_80), BVMULT(32,Var__7,0hex0000e5a2), BVMULT(32,Var__6,0hex0000312b), BVUMINUS(BVMULT(32,var_A8,Var__0)), BVUMINUS(BVMULT(32,Var__1,var_A4)), BVUMINUS(BVMULT(32,Var__2,0hex00004586)), BVUMINUS(BVMULT(32,Var__3,var_9C)), BVUMINUS(BVMULT(32,Var__4,var_98)), BVMULT(32,Var__5,0hex000031ca), BVUMINUS(BVMULT(32,Var__8,var_88)), BVMULT(32,Var__9,var_84), BVUMINUS(BVMULT(32,Var__11,var_7C))) = 0hexffc05f9f;

ASSERT BVPLUS(32, BVMULT(32,Var__12,0hex00009e3e), BVMULT(32,Var__9,0hex0000b8f4), BVMULT(32,Var__5,var_60), BVMULT(32,var_74,Var__0), BVMULT(32,Var__1,var_70), BVUMINUS(BVMULT(32,Var__2,0hex00008202)), BVUMINUS(BVMULT(32,Var__3,var_68)), BVMULT(32,Var__4,var_64), BVUMINUS(BVMULT(32,Var__6,var_5C)), BVUMINUS(BVMULT(32,Var__7,var_58)), BVMULT(32,Var__8,var_54), BVUMINUS(BVMULT(32,Var__10,0hex000092d8)), BVMULT(32,Var__11,0hex0000e10c)) = 0hex003e4761;

ASSERT BVPLUS(32, BVMULT(32,Var__12,var_10), BVMULT(32,Var__9,var_1C), BVMULT(32,Var__8,var_20), BVMULT(32,Var__4,0hex0000e877), BVMULT(32,var_40,Var__0), BVMULT(32,Var__1,0hex00008c27), BVUMINUS(BVMULT(32,Var__2,0hex0000f992)), BVMULT(32,Var__3,var_34), BVUMINUS(BVMULT(32,Var__5,0hex0000538a)), BVUMINUS(BVMULT(32,Var__6,var_28)), BVMULT(32,Var__7,var_24), BVUMINUS(BVMULT(32,Var__10,0hex0000ab0d)), BVMULT(32,Var__11,var_14)) = 0hex001b4945;

CHECKSAT;
COUNTERMODEL;

なお、整数線形算術ではなくビットベクタの連立方程式として解いているのは、オーバーフローする場合があり得るかも知れないと思ったため。また、ビットベクタ演算に関するソルバとしてはBoolectorが有名で、Boolectorをで解くことも考えたが、まずは使い慣れているCVC4で解いてみて、解けなかったらBoolectorを試してみようと考えた。

で、cvc4 baba-re.cvc4 として実行してみると、CHECKSATコマンドの結果として無事satが返ってきて、COUNTERMODELコマンドでこの連列方程式の解の値が得られた。

Var__0 : BITVECTOR(32) = 0bin00000000000000000000000001001101;
Var__1 : BITVECTOR(32) = 0bin00000000000000000000000001100001;
Var__2 : BITVECTOR(32) = 0bin00000000000000000000000001110100;
Var__3 : BITVECTOR(32) = 0bin00000000000000000000000001101000;
Var__4 : BITVECTOR(32) = 0bin00000000000000000000000000100000;
Var__5 : BITVECTOR(32) = 0bin00000000000000000000000001101001;
Var__6 : BITVECTOR(32) = 0bin00000000000000000000000001110011;
Var__7 : BITVECTOR(32) = 0bin00000000000000000000000000100000;
Var__8 : BITVECTOR(32) = 0bin00000000000000000000000001101000;
Var__9 : BITVECTOR(32) = 0bin00000000000000000000000001100001;
Var__10 : BITVECTOR(32) = 0bin00000000000000000000000001110010;
Var__11 : BITVECTOR(32) = 0bin00000000000000000000000001100100;
Var__12 : BITVECTOR(32) = 0bin00000000000000000000000000100001;

あとはこれを文字列化すれば良い。デコンパイル結果のようにprintfを呼び出しても良いが、C言語で2進数リテラルを書く方法を知らず億劫だったので、ここではHaskellのGHCiを使用した。（実際にはgcc拡張やC++14を使えばC/C++でも2進数リテラルを書けるようだ）

% ghci
> :set -XBinaryLiterals
> map toEnum [0b00000000000000000000000001001101,0b00000000000000000000000001100001,0b00000000000000000000000001110100,0b00000000000000000000000001101000,0b00000000000000000000000000100000,0b00000000000000000000000001101001,0b00000000000000000000000001110011,0b00000000000000000000000000100000,0b00000000000000000000000001101000,0b00000000000000000000000001100001,0b00000000000000000000000001110010,0b00000000000000000000000001100100,0b00000000000000000000000000100001] :: String
"Math is hard!"

補足

解いてから気づいたが……

係数の数は十分小さく、また変数の値域も%cで印字していることを考えると小さいと想定できるので、オーバーフローの心配をしてビットベクタ演算を解く必要はなく、整数線形算術として解けば十分だった。

さらに、変数の数と(実質的な)等式の数が等しい線形連立方程式で、退化してもいないので、解は一意に決まるはずで、整数線形算術として解く必要もなく、実数線形算術として解けば十分だった。

参考

終了後に公開されたソースコード
Defcon Quals 2016 - baby-re Writeup (RE)
- baby-re は concolic execution のツールとかで解くのにピッタリだと思いつつも、すぐに使えるツールを知らなかったので断念したんだけど、 angrという便利なツールがあったらしい。