The binary accepts text, and checks if it's the flag. We get "nuh uh" for an invalid flag. The decompiled main code is as follows:
undefined8 main(void){char cVar1;long lVar2; undefined8 len;long buf;long local_20;long local_18; buf =0; len =0;print("whats the flag: ");/* buf becomes the address of the buffer, local_18 is no. of bytes read incl terminating byte */ local_18 =getline(&buf,&len,_stdin);*(undefined *)(local_18 +-1+ buf)=0; local_20 = buf;FUN_00101ad4(buf);FUN_00101346(local_20);FUN_00100c8c(local_20);FUN_00100786(local_20); lVar2 =FUN_00100690(buf);if((lVar2 ==0x20)&&(cVar1 =check(local_20), cVar1 =='\x01')){puts("good job!");return0;}puts("nuh uh");return0;}
The program accepts a line from stdin, and sets the last byte to be a null byte. FUN_00101ad4, FUN_00101346, FUN_00100c8c and FUN_00100786 are all functions which perform a combination of addition and XOR operations on the input buffer, which is treated as a long arr[4]. For example, FUN_00101ad4 contains the following code snippet:
FUN_00100690 then checks that the input is 32 bytes long. The check function contains the following code:
We want to fulfil all conditions in order to enter the if block, and have 1 returned. This will cause "good job" to be printed by main.
We can use the following Z3 script to perform the addition and XOR operations, and impose the 4 restrictions upon the arithmetic results.