DiceCTF 2021 Writeup

この大会は2021/2/6 9:00(JST)～2021/2/8 9:00(JST)に開催されました。
今回もチームで参戦。結果は218点で1059チーム中265位でした。
自分で解けた問題をWriteupとして書いておきます。

Cuckoo's Nest (misc)

Discordに入り、#rulesチャネルのメッセージを見るとフラグが書いてあった。

dice{gang}

babymix (rev)

Ghidraでデコンパイルする。

undefined8 main(void)

{
  int iVar1;
  undefined8 uVar2;
  long in_FS_OFFSET;
  char local_48 [56];
  long local_10;
  
  local_10 = *(long *)(in_FS_OFFSET + 0x28);
  puts(&DAT_00103008);
  printf("Please enter your admin password: ");
  fgets(local_48,0x30,stdin);
  iVar1 = check815546(local_48);
  if (iVar1 == 0) {
    puts("\nIncorrect :(");
    uVar2 = 0xffffffff;
  }
  else {
    puts("Correct! Wrap password in dice{} for the flag :)");
    uVar2 = 0;
  }
  if (local_10 != *(long *)(in_FS_OFFSET + 0x28)) {
                    /* WARNING: Subroutine does not return */
    __stack_chk_fail();
  }
  return uVar2;
}

undefined8 check815546(long param_1)

{
  undefined8 uVar1;
  
  if ((int)*(char *)(param_1 + 8) + (int)*(char *)(param_1 + 0xc) +
      ((int)*(char *)(param_1 + 0xc) - (int)*(char *)(param_1 + 0x11)) == 0x99) {
    uVar1 = check921708(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check921708(long param_1)

{
  undefined8 uVar1;
  
  if ((int)(char)(*(byte *)(param_1 + 2) ^ *(byte *)(param_1 + 0x13)) +
      (int)*(char *)(param_1 + 0x15) + (int)*(char *)(param_1 + 10) == 0xd9) {
    uVar1 = check306697(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check306697(byte *param_1)

{
  undefined8 uVar1;
  
  if ((int)(char)(param_1[0x10] ^ *param_1) +
      (int)(char)param_1[3] + (int)(char)param_1[0x10] + (int)(char)(param_1[0x10] ^ param_1[5]) ==
      0xe8) {
    uVar1 = check358616(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check358616(byte *param_1)

{
  undefined8 uVar1;
  
  if ((int)(char)(*param_1 ^ param_1[0x13]) +
      (int)(char)param_1[10] + (int)(char)param_1[3] +
      ((int)(char)param_1[3] - (int)(char)param_1[0x13]) == 0x148) {
    uVar1 = check914884(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check914884(long param_1)

{
  undefined8 uVar1;
  
  if (((int)*(char *)(param_1 + 2) - (int)*(char *)(param_1 + 0x13)) +
      ((int)*(char *)(param_1 + 10) - (int)*(char *)(param_1 + 8)) == 0x4a) {
    uVar1 = check125197(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check125197(long param_1)

{
  undefined8 uVar1;
  
  if (((int)*(char *)(param_1 + 0x11) - (int)*(char *)(param_1 + 9)) +
      (int)*(char *)(param_1 + 4) + (int)*(char *)(param_1 + 0xb) +
      ((int)*(char *)(param_1 + 0x11) - (int)*(char *)(param_1 + 1)) == 0xa6) {
    uVar1 = check410842(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check410842(long param_1)

{
  undefined8 uVar1;
  
  if ((int)*(char *)(param_1 + 10) + (int)*(char *)(param_1 + 5) +
      ((int)*(char *)(param_1 + 0x12) - (int)*(char *)(param_1 + 9)) +
      (int)*(char *)(param_1 + 10) + (int)*(char *)(param_1 + 0xe) == 0x19d) {
    uVar1 = check123562(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check123562(long param_1)

{
  undefined8 uVar1;
  
  if ((int)*(char *)(param_1 + 0x15) + (int)*(char *)(param_1 + 1) +
      ((int)*(char *)(param_1 + 0xb) - (int)*(char *)(param_1 + 2)) +
      ((int)*(char *)(param_1 + 0x11) - (int)*(char *)(param_1 + 0xd)) +
      ((int)*(char *)(param_1 + 8) - (int)*(char *)(param_1 + 0xc)) +
      ((int)*(char *)(param_1 + 5) - (int)*(char *)(param_1 + 0x10)) == 0x62) {
    uVar1 = check56511(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check56511(long param_1)

{
  undefined8 uVar1;
  
  if ((int)(char)(*(byte *)(param_1 + 0xc) ^ *(byte *)(param_1 + 0x10)) +
      ((int)*(char *)(param_1 + 6) - (int)*(char *)(param_1 + 0xd)) +
      ((int)*(char *)(param_1 + 0x11) - (int)*(char *)(param_1 + 0xb)) +
      (int)(char)(*(byte *)(param_1 + 0xd) ^ *(byte *)(param_1 + 0x13)) == 0x55) {
    uVar1 = check561255(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check561255(long param_1)

{
  undefined8 uVar1;
  
  if ((int)(char)(*(byte *)(param_1 + 7) ^ *(byte *)(param_1 + 2)) +
      ((int)*(char *)(param_1 + 4) - (int)*(char *)(param_1 + 0x10)) == 0x4d) {
    uVar1 = check874387(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check874387(long param_1)

{
  undefined8 uVar1;
  
  if ((int)*(char *)(param_1 + 10) + (int)*(char *)(param_1 + 7) +
      (int)(char)(*(byte *)(param_1 + 0xe) ^ *(byte *)(param_1 + 8)) +
      (int)*(char *)(param_1 + 1) + (int)*(char *)(param_1 + 5) +
      ((int)*(char *)(param_1 + 0xe) - (int)*(char *)(param_1 + 3)) +
      ((int)*(char *)(param_1 + 8) - (int)*(char *)(param_1 + 0x11)) == 0x180) {
    uVar1 = check929976(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check929976(char *param_1)

{
  undefined8 uVar1;
  
  if ((int)param_1[2] + (int)param_1[0x11] +
      ((int)param_1[0xf] - (int)param_1[0x15]) + ((int)param_1[2] - (int)param_1[4]) +
      ((int)param_1[4] - (int)*param_1) == 0x109) {
    uVar1 = check421149(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check421149(long param_1)

{
  undefined8 uVar1;
  
  if ((int)*(char *)(param_1 + 6) + (int)*(char *)(param_1 + 7) +
      ((int)*(char *)(param_1 + 0x15) - (int)*(char *)(param_1 + 0x12)) +
      (int)*(char *)(param_1 + 2) + (int)*(char *)(param_1 + 0xf) +
      ((int)*(char *)(param_1 + 0x11) - (int)*(char *)(param_1 + 4)) +
      ((int)*(char *)(param_1 + 5) - (int)*(char *)(param_1 + 0x12)) == 0xfa) {
    uVar1 = check136292(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check136292(long param_1)

{
  undefined8 uVar1;
  
  if ((int)(char)(*(byte *)(param_1 + 0x12) ^ *(byte *)(param_1 + 0xc)) +
      ((int)*(char *)(param_1 + 7) - (int)*(char *)(param_1 + 0x12)) +
      ((int)*(char *)(param_1 + 0x15) - (int)*(char *)(param_1 + 0x13)) +
      ((int)*(char *)(param_1 + 0x10) - (int)*(char *)(param_1 + 0x15)) == 0x4b) {
    uVar1 = check29354(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check29354(long param_1)

{
  undefined8 uVar1;
  
  if ((int)*(char *)(param_1 + 6) + (int)*(char *)(param_1 + 9) +
      (int)(char)(*(byte *)(param_1 + 2) ^ *(byte *)(param_1 + 10)) +
      (int)*(char *)(param_1 + 7) + (int)*(char *)(param_1 + 2) +
      (int)*(char *)(param_1 + 0xd) + (int)*(char *)(param_1 + 0x14) +
      (int)(char)(*(byte *)(param_1 + 0x10) ^ *(byte *)(param_1 + 3)) == 0x26d) {
    uVar1 = check389170(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check389170(char *param_1)

{
  undefined8 uVar1;
  
  if (((int)param_1[1] - (int)param_1[0x13]) +
      (int)(char)(param_1[2] ^ param_1[0xe]) + (int)*param_1 + (int)param_1[0xb] +
      ((int)param_1[8] - (int)param_1[3]) == 0x11b) {
    uVar1 = check200582(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check200582(byte *param_1)

{
  undefined8 uVar1;
  
  if (((int)(char)param_1[0xd] - (int)(char)param_1[0x13]) +
      (int)(char)(param_1[0xb] ^ *param_1) + (int)(char)(param_1[0xe] ^ *param_1) +
      ((int)(char)param_1[0x10] - (int)(char)param_1[0xe]) == 0x6a) {
    uVar1 = check494505(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check494505(char *param_1)

{
  undefined8 uVar1;
  
  if (((int)param_1[3] - (int)param_1[0x12]) +
      ((int)*param_1 - (int)param_1[0x14]) + (int)param_1[0x13] + (int)param_1[10] +
      (int)param_1[10] + (int)param_1[0x13] == 0x129) {
    uVar1 = check225302(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check225302(char *param_1)

{
  undefined8 uVar1;
  
  if ((int)param_1[0x12] + (int)param_1[0x14] + ((int)*param_1 - (int)param_1[0xf]) == 0x9c) {
    uVar1 = check208407(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check208407(long param_1)

{
  undefined8 uVar1;
  
  if (((int)*(char *)(param_1 + 3) - (int)*(char *)(param_1 + 0x11)) +
      ((int)*(char *)(param_1 + 10) - (int)*(char *)(param_1 + 0x14)) +
      ((int)*(char *)(param_1 + 0xd) - (int)*(char *)(param_1 + 8)) == 0x55) {
    uVar1 = check966250(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check966250(long param_1)

{
  undefined8 uVar1;
  
  if (((int)*(char *)(param_1 + 10) - (int)*(char *)(param_1 + 2)) +
      (int)*(char *)(param_1 + 4) + (int)*(char *)(param_1 + 0x13) +
      (int)(char)(*(byte *)(param_1 + 0x11) ^ *(byte *)(param_1 + 0xc)) +
      ((int)*(char *)(param_1 + 3) - (int)*(char *)(param_1 + 0x11)) == 0xa0) {
    uVar1 = check2476(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check2476(long param_1)

{
  undefined8 uVar1;
  
  if (((int)*(char *)(param_1 + 0xc) - (int)*(char *)(param_1 + 10)) +
      ((int)*(char *)(param_1 + 0xb) - (int)*(char *)(param_1 + 0x15)) == 0x24) {
    uVar1 = check554366(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check554366(long param_1)

{
  undefined8 uVar1;
  
  if ((int)(char)(*(byte *)(param_1 + 0x10) ^ *(byte *)(param_1 + 5)) +
      ((int)*(char *)(param_1 + 6) - (int)*(char *)(param_1 + 0x10)) +
      (int)(char)(*(byte *)(param_1 + 0x13) ^ *(byte *)(param_1 + 0x12)) == 0x66) {
    uVar1 = check471672(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check471672(long param_1)

{
  undefined8 uVar1;
  
  if (((int)*(char *)(param_1 + 0x15) - (int)*(char *)(param_1 + 5)) +
      ((int)*(char *)(param_1 + 6) - (int)*(char *)(param_1 + 0xd)) +
      (int)(char)(*(byte *)(param_1 + 0xf) ^ *(byte *)(param_1 + 10)) == -0x30) {
    uVar1 = check656702(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check656702(long param_1)

{
  undefined8 uVar1;
  
  if ((int)(char)(*(byte *)(param_1 + 4) ^ *(byte *)(param_1 + 6)) +
      ((int)*(char *)(param_1 + 0xc) - (int)*(char *)(param_1 + 0xb)) +
      (int)(char)(*(byte *)(param_1 + 3) ^ *(byte *)(param_1 + 5)) == 0x1d) {
    uVar1 = check244553(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check244553(long param_1)

{
  undefined8 uVar1;
  
  if (((int)*(char *)(param_1 + 0x15) - (int)*(char *)(param_1 + 0xb)) +
      ((int)*(char *)(param_1 + 8) - (int)*(char *)(param_1 + 0xf)) +
      ((int)*(char *)(param_1 + 9) - (int)*(char *)(param_1 + 2)) +
      ((int)*(char *)(param_1 + 6) - (int)*(char *)(param_1 + 0xe)) == -0x6d) {
    uVar1 = check594146(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

undefined8 check594146(char *param_1)

{
  undefined8 uVar1;
  
  if ((int)param_1[0x11] + (int)param_1[0xb] +
      (int)*param_1 + (int)param_1[0x10] + ((int)param_1[0x13] - (int)param_1[7]) == 0x169) {
    uVar1 = check916070(param_1);
  }
  else {
    uVar1 = 0;
  }
  return uVar1;
}

bool check916070(long param_1)

{
  return (int)(char)(*(byte *)(param_1 + 0x13) ^ *(byte *)(param_1 + 0xf)) +
         (int)*(char *)(param_1 + 0xf) + (int)*(char *)(param_1 + 3) == 0x128;
}

以上から、z3で条件を羅列して解く。

from z3 import *

x = [BitVec('x%d' % i, 8) for i in range(22)]
s = Solver()

s.add(x[8] + x[12] + x[12] - x[17] == 0x99)
s.add((x[2] ^ x[19]) + x[21] + x[10] == 0xd9)
s.add((x[16] ^ x[0]) + x[3] + x[16] + (x[16] ^ x[5]) == 0xe8)
s.add((x[0] ^ x[19]) + x[10] + x[3] + x[3] - x[19] == 0x148)
s.add(x[2] - x[19] + x[10] - x[8] == 0x4a)
s.add(x[17] - x[9] + x[4] + x[11] + x[17] - x[1] == 0xa6)
s.add(x[10] + x[5] + x[18] - x[9] + x[10] + x[14] == 0x19d)
s.add(x[21] + x[1] + x[11] - x[2] + x[17] - x[13] + x[8] - x[12] + x[5] - x[16] == 0x62)
s.add((x[12] ^ x[16]) + x[6] - x[13] + x[17] - x[11] + (x[13] ^ x[19]) == 0x55)
s.add((x[7] ^ x[2]) + x[4] - x[16] == 0x4d)
s.add(x[10] + x[7] + (x[14] ^ x[8]) + x[1] + x[5] + x[14] - x[3] + x[8] - x[17] == 0x180)
s.add(x[2] + x[17] + x[15] - x[21] + x[2] - x[4] + x[4] - x[0] == 0x109)
s.add(x[6] + x[7] + x[21] - x[18] + x[2] + x[15] + x[17] - x[4] + x[5] - x[18] == 0xfa)
s.add((x[18] ^ x[12]) + x[7] - x[18] + x[21] - x[19] + x[16] - x[21] == 0x4b)
s.add(x[6] + x[9] + (x[2] ^ x[10]) + x[7] + x[2] + x[13] + x[20] + (x[16] ^ x[3]) == 0x26d)
s.add(x[1] - x[19] + (x[2] ^ x[14]) + x[0] + x[11] + x[8] - x[3] == 0x11b)
s.add(x[13] - x[19] + (x[11] ^ x[0]) + (x[14] ^ x[0]) + x[16] - x[14] == 0x6a)
s.add(x[3] - x[18] + x[0] - x[20] + x[19] + x[10] + x[10] + x[19] == 0x129)
s.add(x[18] + x[20] + x[0] - x[15] == 0x9c)
s.add(x[3] - x[17] + x[10] - x[20] + x[13] - x[8] == 0x55)
s.add(x[10] - x[2] + x[4] + x[19] + (x[17] ^ x[12]) + x[3] - x[17] == 0xa0)
s.add(x[12] - x[10] + x[11] - x[21] == 0x24)
s.add((x[16] ^ x[5]) + x[6] - x[16] + (x[19] ^ x[18]) == 0x66)
s.add(x[21] - x[5] + x[6] - x[13] + (x[15] ^ x[10]) == -0x30)
s.add((x[4] ^ x[6]) + x[12] - x[11] + (x[3] ^ x[5]) == 0x1d)
s.add(x[21] - x[11] + x[8] - x[15] + x[9] - x[2] + x[6] - x[14] == -0x6d)
s.add(x[17] + x[11] + x[0] + x[16] + x[19] - x[7] == 0x169)
s.add((x[19] ^ x[15]) + x[15] + x[3] == 0x128)

r = s.check()
if r == sat:
    m = s.model()
    password = ''
    for i in range(22):
        password += chr(m[x[i]].as_long())
    flag = 'dice{%s}' % password
    print flag

dice{m1x_it_4ll_t0geth3r!1!}