1

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 :(

  • We still cannot yet define recursive function in SMT solvers (so we cannot yet define directly the loop), but we can "unroll" the loop to get a valid password, for example: 6`SHQe. – Ta Thanh Dinh Nov 13 '15 at 1:32
  • In case of the sequence of generated pseudo random numbers in yours machine is different from mine, you can always find a new password using z3 reverseme.smt2 (this file is given here). – Ta Thanh Dinh Nov 13 '15 at 2:47
3

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 0xfff
int 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.

  • Hey thanks for your answer! Maybe it wasn't clear from my first post, but I tried to better explain myself in the comments. I knew that I could brute force, or unroll the loop in a SMT but since another exercise from the same series had a flaw in the algorithm that allowed through a xor property to simply compute the password I thought that maybe I wasn't seeing something. But since everyone here is proposing to "brute force" then I'm happy to do it :D – Jack Taylor Nov 13 '15 at 16:24
  • I never used Z3 so I'll take a look at the documentation and write something down, wanted to learn using it from long time. I'll keep your answer as a reference if I fail during the process XD Again, thank your for you help, it's really appreciated! – Jack Taylor Nov 13 '15 at 16:25
1

In C/C++, rand() has a default seed of 1.

Consider the following:

#include <stdlib.h>
#include <stdio.h>

int main(int argc, char const* argv[])
{
  srand(1);
  int foo = rand();
  printf("%d\n", foo);
  return 0;
}

This will always give you same results as

#include <stdlib.h>
#include <stdio.h>

int main(int argc, char const* argv[])
{
  int foo = rand();
  printf("%d\n", foo);
  return 0;
}

If you change the value in srand() to something different, you will see that you will get a different number.

Therefore, in the solution to your crackme, you can simply use rand() without using srand(), or you could use srand(1) before rand() since an unseeded rand() (or a rand() preceded by a call to srand(1)) will always yield the same results.

  • As per my comment after the code snippet, I already knew that. The problem is I don't know what to do with that. What I'm asking is how to solve the "equation" of the crackme, since it doesn't seem to have a solution for me, without trying a brute force. – Jack Taylor Nov 11 '15 at 9:39
  • If you don't want to bruteforce it, you can always feed it to a SMT solver. – Dillinur Nov 11 '15 at 11:54
  • @Dillinur I've already looked into that, but I'm not sure how to do it. Because the equation in this case seems to be recursive a I don't know any solver that supports that :/ – Jack Taylor Nov 11 '15 at 12:42
  • @JackTaylor: the natural approach is what you said: defining recursive functions (for each of two loops in your crackme) in SMT languages. But current SMT solvers do not handle such a function, so we can "unroll the loop" by trying with several concrete lengths of password. It is not really beauty, but it does work. – Ta Thanh Dinh Nov 13 '15 at 8:31
0

As with all equations, solve it starting from the end. You might need to have several iterations based on the length of the original password string.

Start with hypothesizing the length equals 1, solve the last cycle (what the password would need to be to hit the right answer?) then solve the first cycle based on you knowledge of rand(). If the result looks plausible (e.g. it has exactly the length of 1 as you hypothesized), check it and stop. If not - assume length equals 2 and do the same. Etc, up to the length of string fitting into an int. I would just go up to 8, why bother calculating that length.

P.S. There is no recursion in the code you posted, not sure what you mean.

  • Thank you for your advice. Then I have to brute force my way to the solution :D I thought that maybe there was something wrong in the math and it was solvable in other ways that were obvious to others! By recursion I mean the iteration to compute "i", where we use "i" as input for the next iteration. As far as I know there no way to input such thing in a SMT solver, without knowing the length at least. – Jack Taylor Nov 11 '15 at 20:45
  • @JackTaylor: in principle, we can define recursive functions in SMT languages, but such a function is not handled yet. – Ta Thanh Dinh Nov 13 '15 at 2:43
  • I don't see your problem, you can solve it on paper by iterating over length. Start at 8 and count down to 1 if that's easier :) Or do 8 solver equations if you want to use an SMT solver as in one answer above - someone did all the work for your exercise already. – Vitaly Osipov Nov 13 '15 at 5:18
  • @VitalyOsipov: your approach is absolutely correct, I think that the author asks for a more general solution (which do not need to try each length). Since we cannot yet define recursive function in SMT language, I do not know whether we can get directly a general solution. – Ta Thanh Dinh Nov 13 '15 at 8:55
  • @JackTaylor: strictly speaking, my solution is brute-force but with help of a SMT solver (which is z3 here). In your case, the solution is not heavy, it takes several seconds to get a correct password. Of course, in general case, the running time depends on the length of password. – Ta Thanh Dinh Nov 13 '15 at 9:03

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.