You should definitely check AdrenSys writeup as it covers details about the challenge and the binary, I don't want to repeat what is already done. (Thank you for a great writeup!)
What I would like to add is how I solved this challenge, in a slightly different way, without involving Z3(although it's a great tool, and you should
try it :) ).
The key idea is that all 4 parts of the license key must not be equal to 0, but we know that (email_checksum ^ license_checksum ^ 0xaecbcc2) == 0.
The email checksum is 0xaed12f1, so the license_checksum should be 0x01ae33. Keeping in mind that all 4 parts of the license key
should not be equal to 0, we can create a license key with 3 parts having value 1 and the 4th part having value 0x42b0.
Here's a short program(written in C) to test our license. (If you find any mistake or issue or have a better idea, please contact me on twitter @0xcpu). Thanks!
#include <stdio.h>
#include <stdlib.h>
#include <inttypes.h>
#include <stdbool.h>
#include <string.h>
int main(void)
{
int32_t email_chksum = 0x0AED0DEA;
char const * const email = "[email protected]";
bool chk_switch = false;
for (size_t i = 0; i < strlen(email); i++) {
if (email[i] == '@')
chk_switch = true;
if (chk_switch) {
email_chksum ^= email[i];
} else {
email_chksum += email[i];
}
}
printf("Email checksum: %#08x\n", email_chksum);
char const * const license = "00010001000142b0";
char dword[5] = {0};
char *endstr;
int32_t lic_chksum = 0;
for (size_t i = 0; i < 4; i++) {
strncpy(dword, license + 4 * i, 4);
printf("checksum: %#08lx\n", strtol(dword, &endstr, 0x1e));
lic_chksum ^= (int32_t)strtol(dword, &endstr, 0x1e);
}
printf("License checksum: %#08x\n", lic_chksum);
if ((lic_chksum ^ email_chksum ^ 0xaecbcc2) == 0) {
puts("correct");
} else {
puts("incorrect");
}
}