I have reversed the code of this simple crackme(more like reverseme :)) but I don't understand how to create valid password for the algorithm.Here's the reversed code:#include <stdlib.h>#include <stdio.h>#include <string.h>int main(int argc, char* argv[]) {    if(argc<2)        return -1;    char *original = argv[1];     char *password = strdup(original);    int success = 0xFD0970E7;    int i, j;    for (i = random() & 0xFF; i > 0; i--) {        for (j = 0; j < (int)strlen(original); j++) {            password[j] = password[j] ^ random();        }    }    i = 0x1337;    for (j = strlen(original)-1; j >= 0; j--) {        i = i * password[j] + 0x31337;    }    if (i == success) {        printf(SUCCESS\n);        return 0;    }    printf(WRONG\n);    return -1;}I understand that since random() isn't seeded I can control the input that gets to the later stages of the program, but I don't get how can I use it to solve it :(
How to break this reversing exercise
crackme
We can define recursive functions in SMT language (e.g. with define-fun-rec), but some popular solvers (e.g. z3) currently cannot handle them yet (I do not know any can support); so it is not direct to encode loops in such a solver. But we can use a trick, that is to just unroll the loop (then it is still obliged to test several lengths of the password) by generating automatically SMT formulae. For example, the following program generate a SMT formula for each length of password:#include <stdlib.h>#include <stdio.h>#define PRE_VAL_NUM 0xfffint ran_vals[PRE_VAL_NUM];void gen_pre_vals(){  for (unsigned int i = 0; i < PRE_VAL_NUM; ++i) {    ran_vals[i] = random();  }  return;}int main(int argc, char* argv[]){  if (argc != 2) {    printf(please run as keygen length_of_password\n);    return 0;  }  gen_pre_vals();  FILE* smt_file = fopen(reverseme.smt2, w+);  fprintf(smt_file, (set-logic QF_BV)\n);  fprintf(smt_file, (set-info :smt-lib-version 2.0)\n);  int passwd_len = strtol(argv[1], NULL, 0);  fprintf(smt_file, \n);  for (int i = 0; i < passwd_len; ++i) {    fprintf(smt_file, (declare-fun pw%d () (_ BitVec 8))\n, i);  }  fprintf(smt_file, \n);  fprintf(smt_file, (define-fun prev_i ((i (_ BitVec 32)) (pw_i (_ BitVec 8))) (_ BitVec 32)\n);  fprintf(smt_file, (let ((pw_i_ext ((_ sign_extend 24) pw_i)))\n);  fprintf(smt_file, (bvadd (bvmul i pw_i_ext) #x00031337)))\n);  fprintf(smt_file, \n);  for (int i = 0; i < passwd_len; ++i) {    fprintf(smt_file, (assert (and (bvuge pw%d #x21) (bvule pw%d #x7e)))\n, i, i);  }  fprintf(smt_file, \n);  fprintf(smt_file, (assert\n);  fprintf(smt_file, (let (\n);  unsigned int acc_ran;  for (int i = 0; i < passwd_len; ++i) {    acc_ran = 0x00;    for (int j = ran_vals[0] & 0xff; j > 0; j--) {      acc_ran ^= ran_vals[1 + i + (j - 1) * passwd_len];    }    fprintf(smt_file, (pwn%d (bvxor pw%d #x%x))\n, i, i, (acc_ran & 0xff));  }  fprintf(smt_file, )\n);  fprintf(smt_file, (let ((i%d (prev_i #x1337 pwn%d)))\n, passwd_len - 2, passwd_len - 1);  for (int i = passwd_len - 2; i >= 1; --i) {    fprintf(smt_file, (let ((i%d (prev_i i%d pwn%d)))\n, i - 1, i, i);  }  fprintf(smt_file, (let ((i (prev_i i0 pwn0)))\n);  fprintf(smt_file, (= i #xfd0970e7))\n);  for (int i = 0; i < passwd_len; ++i) fprintf(smt_file, ));  fprintf(smt_file, )\n);  fprintf(smt_file, \n);  fprintf(smt_file, (check-sat)\n);  fprintf(smt_file, (get-value (\n);  for (int i = 0; i < passwd_len; ++i) fprintf(smt_file, pw%d\n, i);  fprintf(smt_file, ))\n);  fclose(smt_file);  printf(output smt file: reverseme.smt2\n);  return 1;}It generates a SMT file, named reverseme.smt2 for each length of password (e.g. the generated SMT file for the length 6 is here), then we can type: z3 reverseme.smt2 to get a valid password. I have tested for lengths of 2, 3, 4, 5 (the length 1 is obviously impossible). On my machine, z3 takes about 1-5 seconds for each test, and gives UNSAT for each of them; the first SAT result 6`SHQe (ASCII codes: 0x36, 0x60, 0x53, 0x48, 0x51, 0x65 is found for length of 6. I do not check whether there exists some valid passwords for lengths larger than 6 though.