I found this challenge from: https://safiire.github.io/blog/2019/01/07/integer-overflow-puzzle/

Most Int overflow challenges I found don't give you a binary, and instead just have you connect to a server. So the sources for these might be a bit different.

Let's take a look at the binary here:

$    file puzzle
puzzle: ELF 64-bit LSB shared object, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, BuildID[sha1]=4e7bd9eb9ab969b8ba61f3b6283f846934c74009, for GNU/Linux 3.2.0, not stripped
$    ./puzzle
Segmentation fault (core dumped)
$    ./puzzle 15935728

So we can see that we are dealing with a 64 bit binary, that appears to take in input via arguments.


When we take a look at the main function in Ghidra, we see this:

undefined8 main(undefined8 argc,long argv)

  if (**(long **)(argv + 8) * 0x1064deadbeef4601 == -0x2efc72d1f84bda97) {
  return 0;

So we can see that it is taking our first argument, multiplying it by 0x1064deadbeef4601, then checking to see if it is equal to 0xD1038D2E07B42569. If it is, then it will run system("/bin/sh"). The reason why the offset is 8 from argv for our first argument, is realistically it's the second argument. The first is the process's name. Also the reason why it displays -0x2efc72d1f84bda97 instead of 0xD1038D2E07B42569 is because that is the signed representation of the unsigned value. Looking at the disassembly shows us the unsigned value:

        00101155 48 b8 01        MOV        RAX,0x1064deadbeef4601
                 46 ef be
                 ad de 64 10
        0010115f 48 0f af c2     IMUL       RAX,RDX
        00101163 48 ba 69        MOV        RDX,0xD1038D2E07B42569
                 25 b4 07
                 2e 8d 03 d1
        0010116d 48 39 d0        CMP        RAX,RDX


So we need to set the product of our input and 0x1064deadbeef4601 equal to 0xD1038D2E07B42569. We will do this using an Integer Overflow. First off let's talk a bit about how an Integer Overflow works.

Data types can only contain so much data. For x64 bit integers, they contain 8 bytes worth of data. So what happens if we try to store a value larger than 8 bytes in an integer? For instance:

0x1064deadbeef4601 * 0xD1038D2E07B42569 = 0xd629404f62e95bf5b815e3124f5db69

Thing is, in instances like this, it will only store the lower 8 bytes. So here, the result would be 0x5b815e3124f5db69. So realistically, the actual "equation" we need to solve is this:

(((argv[1] * 0x1064deadbeef4601) & 0xffffffffffffffff) == 0xD1038D2E07B42569)

We can write a simple z3 script to solve this for us:

from z3 import *

foREVer = Solver()

x = BitVec("0", 64)

foREVer.add(((x * 0x1064deadbeef4601) & 0xffffffffffffffff) == 0xd1038d2e07b42569)

if foREVer.check() == sat:
    solution = foREVer.model()
    solution = hex(int(str(solution[x])))
    solution = solution[2:]

    # We have to reverse the value because the binary is least endian
    value = ""
    i = len(solution) / 2
    while i > 0:
        i -= 1
        y = solution[(i*2):(i*2) + 2]
        value += chr(int("0x" + y, 16))

    print "Now I think, I understand: " + value
    print "Not solvable, I would recommend crying, a lot"

When we run it:

$    python rev.py
Now I think, I understand: io64pass
$    ./puzzle io64pass
$ w
 11:01:12 up  1:31,  1 user,  load average: 1.62, 1.51, 1.27
USER     TTY      FROM             LOGIN@   IDLE   JCPU   PCPU WHAT
guyinatu :0       :0               09:29   ?xdm?   3:58   0.00s /usr/lib/gdm3/g
$ ls
puzzle    readme.md  rev.py

Just like that, we solved the challenge!