maplectf 2023
This commit is contained in:
parent
d98befe85a
commit
c797501c70
|
|
@ -0,0 +1 @@
|
|||
/build
|
||||
|
|
@ -0,0 +1,38 @@
|
|||
# mapleCTF 2023
|
||||
|
||||
what IS UP chat we're back at it again with another writeup post
|
||||
|
||||
last weekend i played [MapleCTF 2023](https://ctf2023.maplebacon.org) with my team
|
||||
[BLÅHAJ](https://blahaj.awoo.systems) (raised from the dead, i don't remember when the last time i
|
||||
played as/with BLÅHAJ was but it's been like. a hot second)
|
||||
|
||||
there were a couple of interesting challenges in this CTF. BLÅHAJ ended up placing 5th, with a team
|
||||
of like just a handful of people, which i thought was actually pretty impressive
|
||||
|
||||
the challenges we solved that were valued the most points at the end of the CTF were
|
||||
|
||||
- flakey ci (misc, 489 points). this was surprising! flakey ci was literally trivial, so i'm
|
||||
surprised more people didn't solve it. maybe they were scared of nix. perhaps i had an unfair
|
||||
advantage being a nix user.....
|
||||
- merkle (crypto, 472 points). also surprising! i'm not sure i would classify merkle as a crypto
|
||||
challenge, it was more just implementing state recovery of internal data structures using
|
||||
probabalistic output. it was not the most time consuming ever to solve, by far
|
||||
- lost-in-space (pwn, 456 points). still surprising,,, like this was a fairly straightforward
|
||||
challenge that required you to implement a graph search algorithm in shellcode with a limited
|
||||
amount of program memory/stack. it was interesting, but it wasn't *hard* imo
|
||||
- AaaS (misc, 436 points). i wasn't involved in solving this one, but it was basically just python
|
||||
trivia. a writeup on this wouldn't be very involved
|
||||
- **coinflip** (misc, 425 points). this one was actually really interesting imo. the discussion on
|
||||
this challenge goes into some depth
|
||||
|
||||
so basically here's a writeup on coinflip. the writeup is structured in a way to guide you through
|
||||
the background information required to develop a solution and the thought process involved, so if
|
||||
you don't rly care about that you can skip to the end with the actual solution script
|
||||
|
||||
enjoy~
|
||||
|
||||
<!--
|
||||
writeup index:
|
||||
|
||||
- [misc: coinflip](#manipulating-python-rng-using-the-seed-coinflip)
|
||||
-->
|
||||
|
|
@ -0,0 +1,452 @@
|
|||
## manipulating python RNG using the seed: `coinflip`
|
||||
|
||||
>Your fate lies in a coin flip. Will you take control of your destiny?
|
||||
>
|
||||
>Author: nneonneo
|
||||
>
|
||||
>`nc coinflip.ctf.maplebacon.org 1337`
|
||||
|
||||
Files:
|
||||
[server.py](https://git.lain.faith/haskal/writeups/raw/branch/main/2023/maple/coinflip/server.py)
|
||||
|
||||
|
||||
### summary
|
||||
|
||||
python `Random` is used to generate random coin flips as `1` or `0` bits, where if you get `1` then
|
||||
you lose money, and if you get `0` you win money. user input directly seeds the RNG, which can be
|
||||
constructed in a way that forces most of the coin flips to go in the `0` direction. using this
|
||||
computed seed, we can trick the server into giving us lots of money and winning the game
|
||||
|
||||
### challenge source
|
||||
|
||||
we are given the source code, in python for the challenge. it's not very long, so reviewing it is
|
||||
straightforward
|
||||
|
||||
|
||||
#### the `Coin` class
|
||||
|
||||
```python
|
||||
class Coin:
|
||||
def __init__(self, coin_id):
|
||||
self.random = Random(coin_id)
|
||||
self.flips_left = 0
|
||||
self.buffer = None
|
||||
|
||||
def flip(self):
|
||||
if self.flips_left == 0:
|
||||
self.buffer = self.random.getrandbits(32)
|
||||
self.flips_left = 32
|
||||
res = self.buffer & 1
|
||||
self.buffer >>= 1
|
||||
self.flips_left -= 1
|
||||
return res
|
||||
```
|
||||
|
||||
this is an implementation of random coin flips, which uses python's builtin `Random` class with a
|
||||
given seed `coin_id`. every time a coin flip is needed, it is taken as the next bit of 32-bit output
|
||||
from the `Random` instance, and when all bits are used a new 32-bit value is requested from `Random`
|
||||
|
||||
this is an interesting implementation because you might expect something more typical like
|
||||
`random.randint(0, 1)` or `random.choice([True, False])` which might be more idiomatic
|
||||
|
||||
#### the "main function"
|
||||
|
||||
```python
|
||||
if __name__ == "__main__":
|
||||
signal.alarm(60)
|
||||
print("Welcome to Maple Betting!")
|
||||
print("We'll be betting on the outcome of a fair coin flip.")
|
||||
print("You'll start with $1 - try to make lots of money and you'll get flags!")
|
||||
|
||||
game_id = input("Which coin would you like to use? ")
|
||||
num_rounds = input("How many rounds do you want to go for? ")
|
||||
num_rounds = int(num_rounds)
|
||||
if num_rounds > 20_000_000:
|
||||
print("Can't play that long, I'm afraid.")
|
||||
exit(1)
|
||||
```
|
||||
|
||||
there is a time limit of 60 seconds to interact with the server, and we are asked for a "game id"
|
||||
and a number of rounds to play. this is the only user input to the program
|
||||
|
||||
```python
|
||||
print("Alright, let's go!")
|
||||
coin = Coin(int(game_id, 0))
|
||||
money = 1
|
||||
for nr in range(num_rounds):
|
||||
money += [1, -1][coin.flip()]
|
||||
if money <= 0:
|
||||
print(f"Oops, you went broke at round {nr+1}!")
|
||||
exit(1)
|
||||
|
||||
```
|
||||
|
||||
the "game id" is used to construct `Coin` (and becomes the seed for the RNG). then, the server plays
|
||||
the rounds you requested. on each round, a `1` or `0` bit is generated, and if the result is `0`,
|
||||
you win `$1`, and if the result is `1` then you lose `$1`
|
||||
|
||||
```python
|
||||
print(f"You finished with ${money} in the pot.")
|
||||
if money < 18_000:
|
||||
print("At least you didn't go broke!")
|
||||
elif money < 7_000_000:
|
||||
print(f"Pretty good!")
|
||||
else:
|
||||
print(f"What the hell?! You bankrupted the casino! Take your spoils: {FLAG}")
|
||||
```
|
||||
|
||||
so in order to win the game and get the flag, we need to make an amount of money over `$7000000`
|
||||
|
||||
|
||||
### naive approach
|
||||
|
||||
since we can control the seed, one approach is to try seed values until one wins the necessary
|
||||
amount of games
|
||||
|
||||
something like this
|
||||
|
||||
```python
|
||||
seed = 0
|
||||
best_seed = 0
|
||||
best_money = 0
|
||||
while True:
|
||||
coin = Coin(seed)
|
||||
money = 0
|
||||
for _ in range(20_000_000):
|
||||
money += [1, -1][coin.flip()]
|
||||
if money > best_money:
|
||||
best_money = money
|
||||
best_seed = seed
|
||||
|
||||
if money <= 0:
|
||||
break
|
||||
|
||||
seed += 1
|
||||
```
|
||||
|
||||
running this for a while might get you money up to like, `$15000` or so depending on how long you run
|
||||
it, but ultimately it's nowhere near the needed `$7000000` and the improvements rapidly diminish with
|
||||
further running time. clearly this approach is not going to work
|
||||
|
||||
### background: python RNG (Mersenne twister)
|
||||
|
||||
to find out how we can manipulate the python RNG, let's take a closer look at the implementation
|
||||
|
||||
the RNG in python is a [Mersenne Twister](https://en.wikipedia.org/wiki/Mersenne_Twister). a quick
|
||||
summary of how the Mersenne twister works
|
||||
|
||||
- a state array `MT` of 32-bit integers is initialized using a given seed value
|
||||
- index `index` set to `n`
|
||||
- to generate a value, pick the next `MT[index]` and increment `index`. additionally the output
|
||||
value is "tempered" with some bitwise operations
|
||||
- if `index >= n`, run the `twist` operation (notice `twist` is also run the first time a random
|
||||
value is generated)
|
||||
- `twist` scrambles `MT` using some more bitwise operations
|
||||
|
||||
we can find the full implementation of the Mersenne twister in CPython in
|
||||
[Modules/_randommodule.c](https://github.com/python/cpython/blob/main/Modules/_randommodule.c)
|
||||
|
||||
here's the implementation of generating a 32 bit number, if you do some tracing through calls in
|
||||
CPython, you can find that this is the underlying C function that gets called by the
|
||||
`getrandbits(32)` call of `Coin.flip`. i've added comments to explain the main parts of the function
|
||||
|
||||
```c
|
||||
static uint32_t
|
||||
genrand_uint32(RandomObject *self)
|
||||
{
|
||||
uint32_t y;
|
||||
static const uint32_t mag01[2] = {0x0U, MATRIX_A};
|
||||
/* mag01[x] = x * MATRIX_A for x=0,1 */
|
||||
uint32_t *mt;
|
||||
|
||||
mt = self->state;
|
||||
|
||||
// XXX: the contents of this block are the "twist" operation
|
||||
|
||||
if (self->index >= N) { /* generate N words at one time */
|
||||
int kk;
|
||||
|
||||
for (kk=0;kk<N-M;kk++) {
|
||||
y = (mt[kk]&UPPER_MASK)|(mt[kk+1]&LOWER_MASK);
|
||||
mt[kk] = mt[kk+M] ^ (y >> 1) ^ mag01[y & 0x1U];
|
||||
}
|
||||
for (;kk<N-1;kk++) {
|
||||
y = (mt[kk]&UPPER_MASK)|(mt[kk+1]&LOWER_MASK);
|
||||
mt[kk] = mt[kk+(M-N)] ^ (y >> 1) ^ mag01[y & 0x1U];
|
||||
}
|
||||
y = (mt[N-1]&UPPER_MASK)|(mt[0]&LOWER_MASK);
|
||||
mt[N-1] = mt[M-1] ^ (y >> 1) ^ mag01[y & 0x1U];
|
||||
|
||||
self->index = 0;
|
||||
}
|
||||
|
||||
// XXX: the following extracts the MT array value and applies the "temper" operation
|
||||
|
||||
y = mt[self->index++];
|
||||
y ^= (y >> 11);
|
||||
y ^= (y << 7) & 0x9d2c5680U;
|
||||
y ^= (y << 15) & 0xefc60000U;
|
||||
y ^= (y >> 18);
|
||||
return y;
|
||||
}
|
||||
```
|
||||
|
||||
to recap, in order to win the coinflip game, we need a lot of coin flips to be a `0` bit; which
|
||||
means we need a lot of the output values to have mostly `0` bits in them
|
||||
|
||||
looking at the "temper" operation above, we can see that if the value `y` is `0x00000000` before
|
||||
tempering, it will still be `0x00000000` after tempering. this means that we need the state array
|
||||
elements themselves to be `0x00000000` to get what we want
|
||||
|
||||
additionally, during the "twist" operation we also find that having `MT` values of mostly
|
||||
`0x00000000` results in "twist" producing an output `MT` which still contains mostly `0x00000000`
|
||||
|
||||
it's starting to look pretty convenient that `0` is the bit needed to win money!
|
||||
|
||||
### `init_by_array`: how to get known values into `MT`
|
||||
|
||||
the last step of background information is to understand how python generates the `MT` array using a
|
||||
given seed
|
||||
|
||||
this is the C function that seeds the RNG using a given Python argument
|
||||
|
||||
```c
|
||||
static int
|
||||
random_seed(RandomObject *self, PyObject *arg)
|
||||
{
|
||||
int result = -1; /* guilty until proved innocent */
|
||||
PyObject *n = NULL;
|
||||
uint32_t *key = NULL;
|
||||
size_t bits, keyused;
|
||||
int res;
|
||||
|
||||
if (arg == NULL || arg == Py_None) {
|
||||
// ... seed from /dev/urandom ...
|
||||
return 0;
|
||||
}
|
||||
|
||||
// ...
|
||||
n = /* coerce argument into PyLong */;
|
||||
// ...
|
||||
|
||||
/* Now split n into 32-bit chunks, from the right. */
|
||||
bits = _PyLong_NumBits(n);
|
||||
if (bits == (size_t)-1 && PyErr_Occurred())
|
||||
goto Done;
|
||||
|
||||
/* Figure out how many 32-bit chunks this gives us. */
|
||||
keyused = bits == 0 ? 1 : (bits - 1) / 32 + 1;
|
||||
|
||||
/* Convert seed to byte sequence. */
|
||||
key = (uint32_t *)PyMem_Malloc((size_t)4 * keyused);
|
||||
if (key == NULL) {
|
||||
PyErr_NoMemory();
|
||||
goto Done;
|
||||
}
|
||||
res = _PyLong_AsByteArray((PyLongObject *)n,
|
||||
(unsigned char *)key, keyused * 4,
|
||||
PY_LITTLE_ENDIAN,
|
||||
0); /* unsigned */
|
||||
if (res == -1) {
|
||||
goto Done;
|
||||
}
|
||||
|
||||
// ...
|
||||
/* XXX: call init_by_array using uint32_t[] from the PyLong value */
|
||||
init_by_array(self, key, keyused);
|
||||
// ...
|
||||
}
|
||||
```
|
||||
|
||||
to summarize, the way seeding works is
|
||||
|
||||
- given a `PyLong` value (ie, any integer in python), an array of `uint32_t` is produced consisting
|
||||
of 32-bit chunks of the given value
|
||||
- `init_by_array` is called with the given array
|
||||
|
||||
next, let's look at `init_by_array` and its helper function `init_genrand`
|
||||
|
||||
```c
|
||||
/* initializes mt[N] with a seed */
|
||||
static void
|
||||
init_genrand(RandomObject *self, uint32_t s)
|
||||
{
|
||||
int mti;
|
||||
uint32_t *mt;
|
||||
|
||||
mt = self->state;
|
||||
mt[0]= s;
|
||||
for (mti=1; mti<N; mti++) {
|
||||
mt[mti] =
|
||||
(1812433253U * (mt[mti-1] ^ (mt[mti-1] >> 30)) + mti);
|
||||
/* See Knuth TAOCP Vol2. 3rd Ed. P.106 for multiplier. */
|
||||
/* In the previous versions, MSBs of the seed affect */
|
||||
/* only MSBs of the array mt[]. */
|
||||
/* 2002/01/09 modified by Makoto Matsumoto */
|
||||
}
|
||||
self->index = mti;
|
||||
return;
|
||||
}
|
||||
|
||||
/* initialize by an array with array-length */
|
||||
/* init_key is the array for initializing keys */
|
||||
/* key_length is its length */
|
||||
static void
|
||||
init_by_array(RandomObject *self, uint32_t init_key[], size_t key_length)
|
||||
{
|
||||
size_t i, j, k; /* was signed in the original code. RDH 12/16/2002 */
|
||||
uint32_t *mt;
|
||||
|
||||
mt = self->state;
|
||||
init_genrand(self, 19650218U);
|
||||
i=1; j=0;
|
||||
k = (N>key_length ? N : key_length);
|
||||
for (; k; k--) {
|
||||
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * 1664525U))
|
||||
+ init_key[j] + (uint32_t)j; /* non linear */
|
||||
i++; j++;
|
||||
if (i>=N) { mt[0] = mt[N-1]; i=1; }
|
||||
if (j>=key_length) j=0;
|
||||
}
|
||||
for (k=N-1; k; k--) {
|
||||
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * 1566083941U))
|
||||
- (uint32_t)i; /* non linear */
|
||||
i++;
|
||||
if (i>=N) { mt[0] = mt[N-1]; i=1; }
|
||||
}
|
||||
|
||||
mt[0] = 0x80000000U; /* MSB is 1; assuring non-zero initial array */
|
||||
}
|
||||
```
|
||||
|
||||
this departs from the traditional method of seeding a Mersenne twister. the original method is
|
||||
`init_genrand`, which implements the canonical seeding function. the procedure here is:
|
||||
|
||||
- call `init_genrand` with a *static seed*
|
||||
- combine the resulting `MT` array with the `init_key` (recall this is 32-bit chunks of the seed
|
||||
value from python) using some bitwise operations and arithmetic
|
||||
|
||||
this is useful for us, because this means it is actually possible to control almost all values in
|
||||
`MT` (except for the first one, which is hardcoded to `0x80000000`). this would not be possible with
|
||||
just the canonical seeding implementation
|
||||
|
||||
### cracking the Mersenne twister (actually)
|
||||
|
||||
[z3](https://github.com/Z3Prover/z3) can be used to reverse the `init_by_array` function and produce
|
||||
an input that causes `MT` to contain the desired values. this is particularly made possible by the
|
||||
operations being all deterministic arithmetic on 32-bit integers, and all loops being a fixed number
|
||||
of iterations
|
||||
|
||||
first, we set up `init_state.txt` which contains the output of `init_genrand(19650218)` since that
|
||||
is static
|
||||
|
||||
then, the following script implements the reversing
|
||||
|
||||
```python
|
||||
N = 624
|
||||
L = N
|
||||
|
||||
with open("init_state.txt", "r") as f:
|
||||
init_mt = [int(x.strip()) for x in f]
|
||||
|
||||
def crack():
|
||||
s = z3.Solver()
|
||||
|
||||
init_key = [z3.BitVec(f"init_key_{i}", 32) for i in range(L)]
|
||||
mt = [z3.BitVecVal(x, 32) for x in init_mt]
|
||||
|
||||
```
|
||||
|
||||
we initialize a `init_key` of all symbolic values, and a `MT` (which in the real code would have
|
||||
just been generated by `init_genrand`) to the required concrete values
|
||||
|
||||
next, we simulate the same operations as `init_by_array`, implemented in python
|
||||
|
||||
```python
|
||||
i = 1
|
||||
j = 0
|
||||
k = N
|
||||
while k > 0:
|
||||
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * z3.BitVecVal(1664525, 32))) + init_key[j] + z3.BitVecVal(j, 32)
|
||||
i += 1
|
||||
j += 1
|
||||
if i >= N:
|
||||
mt[0] = mt[N-1]
|
||||
i = 1
|
||||
if j >= L:
|
||||
j = 0
|
||||
|
||||
k -= 1
|
||||
|
||||
k = N - 1
|
||||
while k > 0:
|
||||
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * z3.BitVecVal(1566083941, 32))) - z3.BitVecVal(i, 32)
|
||||
i += 1
|
||||
if i >= N:
|
||||
mt[0] = mt[N-1]
|
||||
i = 1
|
||||
|
||||
k -= 1
|
||||
```
|
||||
|
||||
finally, we add constraints on the output values `1..N` so that they are all zero
|
||||
|
||||
```python
|
||||
for idx in range(1, N):
|
||||
s.add(mt[idx] == 0)
|
||||
```
|
||||
|
||||
now, we are ready to solve with z3 and output the result as an integer literal which would be passed
|
||||
to the `Random` constructor, which we concatenate from the 32-bit chunks
|
||||
|
||||
```python
|
||||
s.check()
|
||||
m = s.model()
|
||||
|
||||
x = bytearray()
|
||||
for ik in init_key:
|
||||
ikv = m[ik].as_long()
|
||||
x += struct.pack("<I", ikv)
|
||||
|
||||
print(hex(int.from_bytes(x, byteorder='little')))
|
||||
|
||||
if __name__ == "__main__":
|
||||
crack()
|
||||
```
|
||||
|
||||
running this produces a solution value fairly quickly. the full script can be found at
|
||||
[coinflip_crack.py](https://git.lain.faith/haskal/writeups/raw/branch/main/2023/maple/coinflip_crack.py)
|
||||
and
|
||||
[init_state.txt](https://git.lain.faith/haskal/writeups/raw/branch/main/2023/maple/init_state.txt)
|
||||
|
||||
next, we need to find out how many rounds to run with this seed
|
||||
|
||||
```python
|
||||
from server import Coin
|
||||
with open("computed_seed.txt", "r") as f:
|
||||
seed = int(f.read().strip(), 0)
|
||||
coin = Coin(seed)
|
||||
money = 0
|
||||
for i in range(20_000_000):
|
||||
money += [1, -1][coin.flip()]
|
||||
if money > 7_000_000:
|
||||
print(i)
|
||||
break
|
||||
```
|
||||
|
||||
with this we get `14819684`
|
||||
|
||||
### jackpot!!!
|
||||
|
||||
running the server with the computed seed and number of rounds results in the flag! (reproduced here
|
||||
only locally, i don't remember what the server flag was)
|
||||
|
||||
```text
|
||||
$ (sleep 2; cat seed.txt; sleep 2; echo 14819684) | python3 server.py
|
||||
Welcome to Maple Betting!
|
||||
We'll be betting on the outcome of a fair coin flip.
|
||||
You'll start with $1 - try to make lots of money and you'll get flags!
|
||||
Which coin would you like to use? How many rounds do you want to go for? Alright, let's go!
|
||||
You finished with $7000001 in the pot.
|
||||
What the hell?! You bankrupted the casino! Take your spoils: ctf{test_flag_test_flag}
|
||||
```
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
## the end
|
||||
|
||||
```hex
|
||||
6a 3c 58 0f 05
|
||||
```
|
||||
|
|
@ -0,0 +1,16 @@
|
|||
builddir = build
|
||||
|
||||
pandocflags = --filter writefreely-validate --wrap=none --strip-comments
|
||||
|
||||
postid = 7tlde1rgiq
|
||||
|
||||
rule pandoc
|
||||
command = pandoc $pandocflags -o $out $in
|
||||
description = pandoc $out
|
||||
|
||||
rule upload
|
||||
command = writefreely-cli $postid $in
|
||||
description = upload $postid
|
||||
|
||||
build $builddir/post-full.md: pandoc 00-intro.md 01-misc-coinflip.md 02-end.md
|
||||
build upload: upload $builddir/post-full.md
|
||||
|
|
@ -0,0 +1,48 @@
|
|||
from random import Random
|
||||
from secret import FLAG
|
||||
import signal
|
||||
|
||||
class Coin:
|
||||
def __init__(self, coin_id):
|
||||
self.random = Random(coin_id)
|
||||
self.flips_left = 0
|
||||
self.buffer = None
|
||||
|
||||
def flip(self):
|
||||
if self.flips_left == 0:
|
||||
self.buffer = self.random.getrandbits(32)
|
||||
self.flips_left = 32
|
||||
res = self.buffer & 1
|
||||
self.buffer >>= 1
|
||||
self.flips_left -= 1
|
||||
return res
|
||||
|
||||
if __name__ == "__main__":
|
||||
signal.alarm(60)
|
||||
print("Welcome to Maple Betting!")
|
||||
print("We'll be betting on the outcome of a fair coin flip.")
|
||||
print("You'll start with $1 - try to make lots of money and you'll get flags!")
|
||||
|
||||
game_id = input("Which coin would you like to use? ")
|
||||
num_rounds = input("How many rounds do you want to go for? ")
|
||||
num_rounds = int(num_rounds)
|
||||
if num_rounds > 20_000_000:
|
||||
print("Can't play that long, I'm afraid.")
|
||||
exit(1)
|
||||
|
||||
print("Alright, let's go!")
|
||||
coin = Coin(int(game_id, 0))
|
||||
money = 1
|
||||
for nr in range(num_rounds):
|
||||
money += [1, -1][coin.flip()]
|
||||
if money <= 0:
|
||||
print(f"Oops, you went broke at round {nr+1}!")
|
||||
exit(1)
|
||||
|
||||
print(f"You finished with ${money} in the pot.")
|
||||
if money < 18_000:
|
||||
print("At least you didn't go broke!")
|
||||
elif money < 7_000_000:
|
||||
print(f"Pretty good!")
|
||||
else:
|
||||
print(f"What the hell?! You bankrupted the casino! Take your spoils: {FLAG}")
|
||||
|
|
@ -0,0 +1,55 @@
|
|||
import z3
|
||||
import struct
|
||||
|
||||
N = 624
|
||||
L = N
|
||||
|
||||
with open("init_state.txt", "r") as f:
|
||||
init_mt = [int(x.strip()) for x in f]
|
||||
|
||||
def crack():
|
||||
s = z3.Solver()
|
||||
|
||||
init_key = [z3.BitVec(f"init_key_{i}", 32) for i in range(L)]
|
||||
mt = [z3.BitVecVal(x, 32) for x in init_mt]
|
||||
|
||||
i = 1
|
||||
j = 0
|
||||
k = N
|
||||
while k > 0:
|
||||
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * z3.BitVecVal(1664525, 32))) + init_key[j] + z3.BitVecVal(j, 32)
|
||||
i += 1
|
||||
j += 1
|
||||
if i >= N:
|
||||
mt[0] = mt[N-1]
|
||||
i = 1
|
||||
if j >= L:
|
||||
j = 0
|
||||
|
||||
k -= 1
|
||||
|
||||
k = N - 1
|
||||
while k > 0:
|
||||
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 30)) * z3.BitVecVal(1566083941, 32))) - z3.BitVecVal(i, 32)
|
||||
i += 1
|
||||
if i >= N:
|
||||
mt[0] = mt[N-1]
|
||||
i = 1
|
||||
|
||||
k -= 1
|
||||
|
||||
for idx in range(1, N):
|
||||
s.add(mt[idx] == 0)
|
||||
|
||||
s.check()
|
||||
m = s.model()
|
||||
|
||||
x = bytearray()
|
||||
for ik in init_key:
|
||||
ikv = m[ik].as_long()
|
||||
x += struct.pack("<I", ikv)
|
||||
|
||||
print(hex(int.from_bytes(x, byteorder='little')))
|
||||
|
||||
if __name__ == "__main__":
|
||||
crack()
|
||||
|
|
@ -0,0 +1,624 @@
|
|||
19650218
|
||||
2194844435
|
||||
874550967
|
||||
1417962806
|
||||
719805879
|
||||
2188372024
|
||||
721660136
|
||||
1814940559
|
||||
2833403150
|
||||
3889680837
|
||||
1003665704
|
||||
1330738387
|
||||
2892331238
|
||||
3489052161
|
||||
3855278296
|
||||
3311200630
|
||||
1422571577
|
||||
2585306665
|
||||
2882769417
|
||||
2783805802
|
||||
4207719964
|
||||
2400416080
|
||||
2341377904
|
||||
2590753297
|
||||
3924081815
|
||||
1211472509
|
||||
3057012486
|
||||
3436335279
|
||||
551149560
|
||||
1318655221
|
||||
1900533858
|
||||
3537525294
|
||||
2107812065
|
||||
3148644481
|
||||
594136785
|
||||
1814262168
|
||||
1224061569
|
||||
653651109
|
||||
254650943
|
||||
2832785922
|
||||
3699583528
|
||||
2088609312
|
||||
3529585711
|
||||
41492871
|
||||
2876012911
|
||||
4240588078
|
||||
1402615791
|
||||
1934126869
|
||||
3096545044
|
||||
2890863071
|
||||
80499043
|
||||
970921794
|
||||
3007610686
|
||||
750866145
|
||||
799115259
|
||||
3629971774
|
||||
2864380489
|
||||
3888374480
|
||||
2087741561
|
||||
3146346387
|
||||
3269762417
|
||||
2727485495
|
||||
2488668711
|
||||
2964190680
|
||||
2116659522
|
||||
4141458096
|
||||
3537107937
|
||||
3667677805
|
||||
2429248426
|
||||
2452306317
|
||||
3015982257
|
||||
499957222
|
||||
2360410630
|
||||
4194693085
|
||||
147288288
|
||||
3359074475
|
||||
1635136148
|
||||
4073107990
|
||||
3628367767
|
||||
3898116531
|
||||
275612352
|
||||
2842514961
|
||||
3115851985
|
||||
3103448722
|
||||
302309156
|
||||
22171017
|
||||
2075519075
|
||||
3671007489
|
||||
3949991970
|
||||
1963601502
|
||||
4167967445
|
||||
804406473
|
||||
1055110313
|
||||
3894654986
|
||||
2278780139
|
||||
34711884
|
||||
4121261916
|
||||
3468881884
|
||||
2287991389
|
||||
393453278
|
||||
548699130
|
||||
1499706375
|
||||
332872900
|
||||
1556864443
|
||||
1043137738
|
||||
4174970395
|
||||
1614747618
|
||||
669116410
|
||||
1897615374
|
||||
3255278936
|
||||
1370736725
|
||||
1550777747
|
||||
1685794058
|
||||
1862314184
|
||||
2400528575
|
||||
2672900100
|
||||
1647333586
|
||||
3524644532
|
||||
1765506473
|
||||
2857335743
|
||||
3636393737
|
||||
2932986219
|
||||
1203228647
|
||||
1628511289
|
||||
3647085204
|
||||
2987412752
|
||||
2905279128
|
||||
2631768385
|
||||
4014428911
|
||||
1727529885
|
||||
1124854030
|
||||
2262104686
|
||||
2499713312
|
||||
2421398767
|
||||
4134715143
|
||||
2358935835
|
||||
1002066021
|
||||
340444514
|
||||
3268366900
|
||||
1112268606
|
||||
1897974631
|
||||
3331577291
|
||||
2922602614
|
||||
3423543891
|
||||
1267030560
|
||||
2344564886
|
||||
1942259446
|
||||
3179572998
|
||||
1573187880
|
||||
1205933762
|
||||
3025229445
|
||||
4246102746
|
||||
346693941
|
||||
2002220930
|
||||
1829519945
|
||||
3309743875
|
||||
1904872348
|
||||
955816590
|
||||
2796353700
|
||||
668528669
|
||||
2648785169
|
||||
2704726048
|
||||
893089804
|
||||
738773343
|
||||
2832484895
|
||||
2050343702
|
||||
104744889
|
||||
3439545764
|
||||
980222603
|
||||
422274176
|
||||
3865519914
|
||||
2026267864
|
||||
539814729
|
||||
4137805178
|
||||
1140607595
|
||||
2537690753
|
||||
3971218783
|
||||
1931293181
|
||||
3089667358
|
||||
1133695167
|
||||
399772074
|
||||
3682192071
|
||||
4293649418
|
||||
1029228868
|
||||
3902327948
|
||||
1974090788
|
||||
3344730195
|
||||
2795804747
|
||||
3396216457
|
||||
366677807
|
||||
416687433
|
||||
930072460
|
||||
901228284
|
||||
1521860141
|
||||
3484259358
|
||||
478803252
|
||||
3138556488
|
||||
4137898487
|
||||
3807832586
|
||||
3773310804
|
||||
3221624091
|
||||
3076008769
|
||||
4156878137
|
||||
406561453
|
||||
3897607181
|
||||
623564883
|
||||
2247148685
|
||||
1696011322
|
||||
2911604503
|
||||
3979653402
|
||||
742342831
|
||||
3881512158
|
||||
2282092805
|
||||
2681274264
|
||||
3681829528
|
||||
46152446
|
||||
3126539534
|
||||
3635632789
|
||||
1012335624
|
||||
3686064131
|
||||
2587648220
|
||||
2008745587
|
||||
2556071384
|
||||
1788453345
|
||||
861781568
|
||||
2727104545
|
||||
758340017
|
||||
1880693944
|
||||
2136364769
|
||||
1370367813
|
||||
798286522
|
||||
506003017
|
||||
2520802485
|
||||
2991500316
|
||||
3489134272
|
||||
3275208410
|
||||
1640252809
|
||||
3797759893
|
||||
4271912220
|
||||
3111882026
|
||||
140581304
|
||||
2568658569
|
||||
2686841033
|
||||
3059852298
|
||||
293994524
|
||||
1890650113
|
||||
1797269750
|
||||
3428669802
|
||||
1401714789
|
||||
2643788909
|
||||
3727894469
|
||||
2833360921
|
||||
1622853283
|
||||
3832221927
|
||||
277065458
|
||||
3711010937
|
||||
4192871202
|
||||
3356722694
|
||||
680496635
|
||||
2574997514
|
||||
1476265004
|
||||
3232676806
|
||||
3318710975
|
||||
4210635059
|
||||
4159903992
|
||||
2116300560
|
||||
2532158399
|
||||
718792604
|
||||
2539969944
|
||||
3164133583
|
||||
2649636591
|
||||
2200349072
|
||||
2851998122
|
||||
670873689
|
||||
2613796143
|
||||
3562264788
|
||||
1174445287
|
||||
1149173203
|
||||
2225964784
|
||||
4266377361
|
||||
3119455410
|
||||
1518371465
|
||||
1816545474
|
||||
2516586762
|
||||
240910660
|
||||
2681595121
|
||||
1301176317
|
||||
3127753611
|
||||
862342957
|
||||
771183330
|
||||
438085196
|
||||
1046497567
|
||||
922186079
|
||||
1222939296
|
||||
51184555
|
||||
1757804190
|
||||
426665187
|
||||
2730510776
|
||||
2573705612
|
||||
1312406577
|
||||
667742236
|
||||
3239950393
|
||||
2582034960
|
||||
3759737929
|
||||
1601926242
|
||||
2947737408
|
||||
975540284
|
||||
1285948639
|
||||
3761027786
|
||||
1226457986
|
||||
34782949
|
||||
2916146832
|
||||
142734034
|
||||
569716755
|
||||
4042990521
|
||||
3947471773
|
||||
1575951506
|
||||
3517313596
|
||||
3100986137
|
||||
2199197158
|
||||
3376719924
|
||||
4087139828
|
||||
3705107125
|
||||
1482533137
|
||||
1541227668
|
||||
1678953742
|
||||
2056318769
|
||||
3045003063
|
||||
1622629937
|
||||
487578169
|
||||
4137196231
|
||||
3764647071
|
||||
2241527512
|
||||
2558474063
|
||||
1038354351
|
||||
2094837850
|
||||
2481932343
|
||||
3229539130
|
||||
3756851151
|
||||
1006180559
|
||||
4181103103
|
||||
3565909441
|
||||
2371373280
|
||||
1493415041
|
||||
160348120
|
||||
1285104017
|
||||
3595587370
|
||||
4264242568
|
||||
1161124915
|
||||
2042766103
|
||||
737713932
|
||||
3481808155
|
||||
478389208
|
||||
1300643225
|
||||
1007986266
|
||||
1168231653
|
||||
3652705112
|
||||
2909421388
|
||||
3924670764
|
||||
1731016690
|
||||
4084014919
|
||||
4205099837
|
||||
1373900512
|
||||
2937538864
|
||||
2730075174
|
||||
957417377
|
||||
3258199283
|
||||
87174175
|
||||
792789163
|
||||
2527971304
|
||||
2716998340
|
||||
3091367825
|
||||
97659251
|
||||
1782441684
|
||||
919015551
|
||||
735476370
|
||||
87326482
|
||||
926205331
|
||||
1888657273
|
||||
3715638227
|
||||
1715499660
|
||||
1922410526
|
||||
4175228089
|
||||
1525608673
|
||||
3578587616
|
||||
2042086160
|
||||
3730509879
|
||||
3607443975
|
||||
3879209240
|
||||
3652717612
|
||||
2372597521
|
||||
3471943430
|
||||
2765853569
|
||||
3643232056
|
||||
3297105617
|
||||
2692883557
|
||||
1805942063
|
||||
1394934451
|
||||
3337180104
|
||||
1181922214
|
||||
2331394419
|
||||
306465830
|
||||
3736887952
|
||||
1729663122
|
||||
3390355091
|
||||
2379159653
|
||||
3851731257
|
||||
4021176185
|
||||
1079541434
|
||||
433656928
|
||||
1831627642
|
||||
2892512290
|
||||
4063025724
|
||||
406246264
|
||||
1293199350
|
||||
1120564498
|
||||
3926678815
|
||||
1350089133
|
||||
4273098366
|
||||
3385122292
|
||||
993379095
|
||||
725502136
|
||||
25504318
|
||||
752278045
|
||||
3729298457
|
||||
2392480235
|
||||
2657233815
|
||||
320925812
|
||||
2950230896
|
||||
989728679
|
||||
506301841
|
||||
1404204260
|
||||
1413065993
|
||||
865242585
|
||||
866785615
|
||||
1859142878
|
||||
589268143
|
||||
775553472
|
||||
1410495094
|
||||
1607063978
|
||||
3888932143
|
||||
704411669
|
||||
3513884419
|
||||
3370826939
|
||||
2896358996
|
||||
439226283
|
||||
2352722741
|
||||
1626809714
|
||||
246502175
|
||||
189424636
|
||||
1337937966
|
||||
3719088974
|
||||
4178799653
|
||||
2794717891
|
||||
1831166187
|
||||
1862432793
|
||||
2263235392
|
||||
3847861459
|
||||
802662362
|
||||
3621709005
|
||||
2634319122
|
||||
3245216029
|
||||
1466421412
|
||||
1528864744
|
||||
349292989
|
||||
3152395874
|
||||
3374677426
|
||||
2279952808
|
||||
1238578150
|
||||
107682552
|
||||
913857966
|
||||
3747681661
|
||||
3560958606
|
||||
3617063034
|
||||
1988620951
|
||||
1854864649
|
||||
1862999556
|
||||
2962654934
|
||||
1498851202
|
||||
2003448718
|
||||
2942754891
|
||||
798789550
|
||||
3882536840
|
||||
3338815162
|
||||
3066948065
|
||||
2057094004
|
||||
4171611151
|
||||
4284063395
|
||||
2325690120
|
||||
2659914459
|
||||
165909127
|
||||
2783186990
|
||||
2161504072
|
||||
343671839
|
||||
2751150377
|
||||
3621950182
|
||||
222528329
|
||||
3219381950
|
||||
238911006
|
||||
2710753737
|
||||
2982111755
|
||||
1115859074
|
||||
156211365
|
||||
228231184
|
||||
2302165064
|
||||
933165355
|
||||
4181545713
|
||||
2201173365
|
||||
291303663
|
||||
19134280
|
||||
3581811046
|
||||
68817880
|
||||
1037069880
|
||||
2445243929
|
||||
2507869609
|
||||
1468655994
|
||||
2646143627
|
||||
2709652242
|
||||
559859542
|
||||
2657856757
|
||||
248278651
|
||||
656698256
|
||||
2682159578
|
||||
3542996035
|
||||
2775252812
|
||||
1761180115
|
||||
3646714856
|
||||
2330951878
|
||||
834843492
|
||||
3951905925
|
||||
744286448
|
||||
3621804227
|
||||
2822882772
|
||||
1168938371
|
||||
3349647456
|
||||
672527398
|
||||
1163635478
|
||||
3445281068
|
||||
722448549
|
||||
3543924788
|
||||
2823456463
|
||||
1931863550
|
||||
2483173049
|
||||
4148604134
|
||||
3081487737
|
||||
2916138664
|
||||
940193076
|
||||
4142650279
|
||||
2563327448
|
||||
3737140007
|
||||
2407111514
|
||||
243557343
|
||||
1657192483
|
||||
3995730323
|
||||
1012445178
|
||||
2365602253
|
||||
2830079959
|
||||
2287658550
|
||||
2893719730
|
||||
2373631903
|
||||
4215513121
|
||||
189686171
|
||||
2003138393
|
||||
3410898923
|
||||
1020530876
|
||||
1103312993
|
||||
1976606742
|
||||
899447370
|
||||
1949555562
|
||||
3167671920
|
||||
595304244
|
||||
1919198655
|
||||
2929333298
|
||||
619161901
|
||||
623498751
|
||||
2063591130
|
||||
763251111
|
||||
4291719204
|
||||
3951567013
|
||||
2998385089
|
||||
758818611
|
||||
1375945828
|
||||
2510752543
|
||||
4188334520
|
||||
121785359
|
||||
3225750324
|
||||
1354685949
|
||||
1643999927
|
||||
911976986
|
||||
518523023
|
||||
3993561529
|
||||
2326708913
|
||||
336174575
|
||||
853096604
|
||||
2873283550
|
||||
4022490143
|
||||
3010604384
|
||||
2080594943
|
||||
1702902668
|
||||
3360749048
|
||||
4184957279
|
||||
2421794725
|
||||
4155016765
|
||||
3104188113
|
||||
1576615579
|
||||
604774175
|
||||
2739462297
|
||||
4096823942
|
||||
1932918233
|
||||
1779286169
|
||||
2544260698
|
||||
1430072091
|
||||
2196303270
|
||||
4237199385
|
||||
2613550760
|
||||
1481676153
|
||||
2920297152
|
||||
2463881971
|
||||
1098865791
|
||||
2939219489
|
||||
2494804283
|
||||
3108728554
|
||||
1635052534
|
||||
2905164258
|
||||
Loading…
Reference in New Issue