Philip Snyder

Introduction

We're given a single executable called "timesup". I started by launching the executable to uncover its purpose. Sadly, the output proved to be no help at all. (I'm running this in Docker on my Mac).

The Challenge

The first thing I did was open up the executable in Ghidra to see what it was doing. I immediately navigated to the entry point function and main function, and started looking at the decompiled psuedo code generated by Ghidra (cause who the hell wants to read assembly?). We're greeted by some pretty accurate looking psuedo code.

undefined8 FUN_0010131a(void)
{
  int iVar1;
  tm *ptVar2;
  undefined4 local_64;
  undefined4 local_60;
  undefined4 local_5c;
  undefined8 local_58;
  ulong local_50;
  undefined8 local_48;
  undefined8 local_40;
  undefined8 local_38;
  long local_30;
  char *local_28;
  time_t local_20 [2];
  
  _INIT_0();
  local_20[0] = time((time_t *)0x0);
  ptVar2 = localtime(local_20);
  local_58._0_4_ = ptVar2->tm_sec;
  local_58._4_4_ = ptVar2->tm_min;
  local_50._0_4_ = ptVar2->tm_hour;
  local_50._4_4_ = ptVar2->tm_mday;
  local_48._0_4_ = ptVar2->tm_mon;
  local_48._4_4_ = ptVar2->tm_year;
  local_40._0_4_ = ptVar2->tm_wday;
  local_40._4_4_ = ptVar2->tm_yday;
  local_38 = *(undefined8 *)&ptVar2->tm_isdst;
  local_30 = ptVar2->tm_gmtoff;
  local_28 = ptVar2->tm_zone;
  puts("<<< Space Travel require precision.");
  printf("<<< Current Time Is: %02d:%02d:%02d
",local_50 & 0xffffffff,local_58 >> 0x20,
         local_58 & 0xffffffff);
  printf("Enter authorization sequence >>> ");
  __isoc99_scanf("%x %x %x",&local_5c,&local_60,&local_64);
  iVar1 = FUN_001012ce(local_5c,local_60,local_64);
  if (iVar1 != 0xa4c570) {
    printf("<<< Authorization sequence not valid.");
                    /* WARNING: Subroutine does not return */
    exit(0);
  }
  if ((local_58._4_4_ < 0x11) || (0x11 < local_58._4_4_)) {
    puts("<<< You failed. Try Another Time.");
  }
  else {
    FUN_0010125c("flag.txt");
  }
  return 0;
}

Although the psuedo code is already pretty clear, we can still improve it with some manual inspection of the code.

// Function prototype for helper functions
int validateAuthorization(unsigned int seq1, unsigned int seq2, unsigned int seq3);
void displayFlag(const char *filename);
void setupIoBuffers(void);

int main(void) {
   // Local variables
   struct tm *timeInfo;
   unsigned int authSeq1, authSeq2, authSeq3;
   time_t currentTime;
   
   // disable stderr 
   setupIoBuffers();
   
   // Get current time
   currentTime = time(NULL);
   timeInfo = localtime(&currentTime);
   
   // Display initial message
   puts("<<< Space Travel require precision.");
   printf("<<< Current Time Is: %02d:%02d:%02d", timeInfo->tm_hour, timeInfo->tm_min, timeInfo->tm_sec);
   
   // Request authorization input
   printf("Enter authorization sequence >>> ");
   scanf("%x %x %x", &authSeq1, &authSeq2, &authSeq3);
   
   // Validate authorization
   int validationResult = validateAuthorization(authSeq1, authSeq2, authSeq3);
   if (validationResult != 0xa4c570) {
       printf("<<< Authorization sequence not valid.");
       exit(0);
   }
   
   // Check if the current minute is 17 (0x11)
   if (timeInfo->tm_min != 0x11) {
       puts("<<< You failed. Try Another Time.");
   } else {
       displayFlag("flag.txt");
   }
   
   return 0;
}

For those of you unfamiliar with CTFs, to actually solve the challenge, you have to nc to the remote server 0.cloud.chals.io:26020 and solve the challenge there as the flag is stored in text file only on the server. This is to prevent people from debugging the challenge locally. This is a common tactic used by CTF authors to force a static solve, hence we're only provided with the binary and it attempts to open a file called flag.txt that only exists on the server.

Cracking the Code: Our Objective in Plain Sight

The first thing that jumped out to me was that the user had to input the solution on the 17th minute of the hour. Seems simple enough. Secondly the scanf is expecting three hex numbers that are passed to (what I renamed) the validateAuthorization function. This is where things get interesting... because up until this point, the challenge was pretty simple. This is what the decompiled code for the function looks like:

int validateAuthorization(int param_1,int param_2,int param_3)
{
  return (param_1 + param_2 + param_3 << ((byte)(param_1 % param_2) & 0x1f)) /
         (int)((2 << ((byte)param_1 & 0x1f) ^ 3U) * param_3);
}

If the function's output is not equal to 0xa4c570 or 10,798,448 in decimal format, the binary will exit, and we won't get the flag.

It was pretty clear to me that I wouldn't be able to solve this with mental math or like a standard equation. It was late, I was tired, so I immediately went to Google, looking for a "multi-variate bitwise equation solver," to no avail.

Discovering Z3

As I continued looking for an online equation solver that could handle bitwise shifts and xor operations, I kept seeing occasional references to the "Z3 Theorem Solver" and decided to check it out.

I quickly realized that Z3 existed to solve these problems, and it supported all the bit operators. I promptly dove into the python bindings for Z3 and spent about fifteen minutes learning the lay of the land.

I quickly scrapped together this code after taking another ten minutes to figure out that I had to represent my numerical inputs as bit vectors rather than the int type in Z3.

The Solution Code:

# pip install z3-solver
from z3 import BitVec, Solver

a = BitVec("a", 32)
b = BitVec("b", 32)
c = BitVec("c", 32)

num = (a + b + c) << ((a % b) & 0x1F)
denom = c * ((2 << (a & 0x1F)) ^ 3)
equation = num / denom

s = Solver()
s.add(equation == 0xA4C570)
s.check()

m = s.model()

print(hex(s.model()[a].as_long()))
print(hex(s.model()[b].as_long()))
print(hex(s.model()[c].as_long()))

Based off the error message being <<< You failed. Try Another Time. rather than <<< Authorization sequence not valid. we know that the magical numbers we generated were correct.

And Voila! We had our working magic numbers, and were the first team to solve the challenge.

Conclusion

And just like that, we had our solution to a seemingly tricky problem; Z3 had generated three perfect numbers instantaneously that had satisfied our conditions.

There was only one more check to pass, submitting our three numbers at the seventeenth minute of the hour, which just required patience.