# Aero CTF 2020 - Magic II (Crypto, 496pts)
Good and difficult crypto challenge. Should be an entry exercise for getting into Lattice-based cryptoanalysis and Symbolic Execution.
## challenge details
We got Python script (excerpted):
```pythondef create_potion(ingredients: List[int], amounts: List[int]) -> int:    magic_constant = 1046961993706256953070441    effect = sum(starmap(mul, zip(ingredients, amounts)))    side_effect = getrandbits(13) ^ getrandbits(37)    return (effect + side_effect) % magic_constant
def main():    from secret import FLAG    security_level = 64    ingredients_count = 12    random = Random.create(security_level)    potions_count = int.from_bytes(FLAG, 'big') ^ random.randint(512)    print(f'There are {potions_count} famous potions in the world. We are trying to create something new!')    ingredients = [random.randint(security_level) for _ in range(ingredients_count)]    while True:        amounts = [getrandbits(41) for _ in range(len(ingredients))]        effect = create_potion(ingredients, amounts)        print(f'A potion with {amounts} amounts of ingregients has {effect} value of effect.')        choice = input('Would you like to create another potion? (y/n): ')        if not choice.lower().startswith('y'):            break    return```
and its output for 100 rounds:
```There are 6649072325173565167790166618241744001772629470276152191212306811403978598551946952005874796389850254324206273014469019894959347241157412707755498754629152 famous potions in the world. We are trying to create something new!A potion with [432963764937, 1734018663110, 341889949567, 1898982667391, 2077151719276, 1407002783602, 1284167537027, 1834426568578, 285492081118, 2058066808411, 682725745551, 212794466530] amounts of ingregients has 675829748828112222653599 value of effect.Would you like to create another potion? (y/n): yA potion with [1520127565791, 1613928435234, 1481625614519, 513222175065, 1825760063135, 849601240471, 2028256612679, 884310262235, 240010057040, 992839358285, 923505774812, 383090205845] amounts of ingregients has 19282755083699178123269 value of effect.Would you like to create another potion? (y/n): y(...194 lines omitted)A potion with [353615797819, 779510410363, 634337418618, 112328801072, 1308573457212, 1018471322967, 2191760622378, 1641311358023, 126717015375, 790498704391, 2029952294067, 1080095433537] amounts of ingregients has 64147717148582160182619 value of effect.Would you like to create another potion? (y/n): n```
## Recovering ingredients by solving CVP
`Random` is the original RNG implementation of this challenge. We should analyse it later, but at first we should guess what the `ingredients` is.
The calculation of creating potion above can be treated as manipulation of matrix. If we define
$$\begin{align}\boldsymbol{A} =&\;\texttt{amounts[]}\\\boldsymbol{s} =&\;\texttt{ingredients}\\n =&\;\texttt{ingredients_count}\\\boldsymbol{e} =&\;\texttt{side_effect[]}\\\boldsymbol{b} =&\;\texttt{effect[]}\\q =&\;\texttt{magic_constant}\end{align}$$
the calculation can be described as:
$$\begin{align}\boldsymbol{A}\boldsymbol{s}+\boldsymbol{e}=\boldsymbol{b}\bmodq\end{align}$$
And we know $\boldsymbol{A}$, $\boldsymbol{b}$, and $q$... well, that is what exactly [LWE cryptosystem](http://cryptowiki.net/index.php?title=LWE-based_cryptographic_protocols#LWE-based_cryptosystems) is!
Using a [lattice](https://ctf-wiki.github.io/ctf-wiki/crypto/asymmetric/lattice/overview/) for attacking LWE is very common. In this case, there are too many bits in $q$ and the error $\boldsymbol{e}$ is relatively small. It is very likely to break this cipher by lattice attack.
Solving LWE is reducted into [CVP](https://ctf-wiki.github.io/ctf-wiki/crypto/asymmetric/lattice/cvp/) in the lattice theory. First break the equation into rows:
\[\begin{cases}\boldsymbol{a}_{1}\boldsymbol{s}+e_{1}=b_{1}\bmod q\\\boldsymbol{a}_{2}\boldsymbol{s}+e_{2}=b_{2}\bmod q\\\vdots\\\boldsymbol{a}_{m}\boldsymbol{s}+e_{m}=b_{m}\bmod q\end{cases}\]
and erase the modulo by introducing coefficient $k_1, \dots, k_n\in\mathbb{Z}$:
$$\begin{cases}\boldsymbol{a}_{1}\boldsymbol{s}+k_{1}q=b_{1}-e_{1}\\\boldsymbol{a}_{2}\boldsymbol{s}+k_{2}q=b_{2}-e_{2}\\\vdots\\\boldsymbol{a}_{m}\boldsymbol{s}+k_{m}q=b_{m}-e_{m}\end{cases}$$
This can be translated into matrix operation:
$$\left[\begin{array}{cccccccc}a_{11} & a_{12} & \cdots & a_{1n} & q & 0 & \cdots & 0\\a_{21} & \ddots &  & \vdots & 0 & q &  & \vdots\\\vdots &  & \ddots & \vdots & \vdots &  & \ddots & \vdots\\a_{m1} & \cdots & \cdots & a_{mn} & 0 & \cdots & \cdots & q\end{array}\right]\left[\begin{array}{c}s_{1}\\\vdots\\s_{n}\\k_{1}\\\vdots\\k_{m}\end{array}\right]=\boldsymbol{b}-\boldsymbol{e}$$
and also can be written as following:
$$s_{1}\left[\begin{array}{c}a_{11}\\a_{21}\\\vdots\\a_{m1}\end{array}\right]+\cdots+s_{n}\left[\begin{array}{c}a_{1n}\\a_{2}\\\vdots\\a_{mn}\end{array}\right]+k_{1}\left[\begin{array}{c}q\\0\\\vdots\\0\end{array}\right]+k_{2}\left[\begin{array}{c}0\\q\\\vdots\\0\end{array}\right]+\cdots+k_{m}\left[\begin{array}{c}0\\0\\\vdots\\q\end{array}\right]=\boldsymbol{b}-\boldsymbol{e}$$
This is considered as a lattice, with $n+m$ base vectors and targetting $\boldsymbol{b}$ with a (relatively) small error $\boldsymbol{e}$. In the other words, we should adjust parameters $s_1, \dots, s_n, k_1, \dots, k_m$ and find the closest vector into $\boldsymbol{b}$.
This is called CVP (Closest Vector Problem) in the lattice theory. It is known that this is NP-hard, but, by using LLL and [Babai's nearest plane algorithm](https://ctf-wiki.github.io/ctf-wiki/crypto/asymmetric/lattice/cvp/#babais-nearest-plane-algorithm), a good approximate solution can be found in the polynomial time (w/o knowing actual parameters $s_1, \dots, s_n, k_1, \dots, k_m$). This is enough for this case.
We did implement solver with SageMath:
{%gist hakatashi/2266a5df35cc79de50b86d2419b33a6f %}
Note that SageMath implements [closest_vector()](http://doc.sagemath.org/html/en/reference/modules/sage/modules/free_module_integer.html#sage.modules.free_module_integer.FreeModule_submodule_with_basis_integer.closest_vector) but it is a definitive solution and (thus) very very slow.
And we recovered `ingredients` as:
```[15947635162630781022, 13358685451704549741, 16125368066162772035, 15826229117247968913, 2646399917048428358, 4885066420149917790, 5030034390407155536, 14428761327704365060, 12909357566263158604, 8293230205600583029, 14383462958218167109, 15636563551321853965]```
## Recover the Initial State of RNG by Z3
Now we know the last $64\times12$ bits of RNG output. Let's move into RNG.
The generation of bits can be seen here in the given code:
```python    def _getbit(self) -> int:        buffer = 2 * self._state | self._state >> (self._size - 1) | self._state << (self._size + 1)        self._state = reduce(ior, ((buffer >> i & 7 in [1, 2, 3, 4]) << i for i in range(self._size)))        return self._state & 1```
The state parameter is 64bits unsigned integer. This code is a bit tricky, but actually this is just getting `i-1..i+1`-th bits of previous state for each `i`-th bits and checking if it is 1, 2, 3, or 4.
Solving the puzzle by hand is an option, but this check can be translated into a simple logical expression, `(state[i-1] | state[i]) ^ state[i+1]` (Write your own truth table!). It is very likely that this can be automatically analyzed by SAT-solver. Let's try with Z3Py!
{%gist hakatashi/c7826a6b6ff64e97a934d2485099af45 %}
Execute and wait for a few minites... and yes, SAT!
```$ python2 solve.pySolving...('SAT', [state__13 = True, state__2 = True, state__46 = True, state__42 = True, state__49 = False, state__50 = False, state__54 = False, state__63 = True, state__25 = False, state__39 = False, state__30 = True, state__19 = True, state__47 = True, state__41 = False, state__38 = False, state__20 = False, state__23 = True, state__52 = False, state__11 = True, state__18 = False, state__21 = True, state__55 = False, state__62 = False, state__1 = True, state__40 = True, state__51 = False, state__0 = False, state__3 = False, state__14 = False, state__57 = True, state__28 = False, state__9 = True, state__45 = False, state__22 = False, state__44 = True, state__35 = True, state__5 = False, state__6 = True, state__27 = True, state__32 = False, state__60 = False, state__61 = True, state__53 = True, state__4 = False, state__16 = False, state__29 = False, state__34 = False, state__37 = False, state__7 = True, state__15 = False, state__26 = True, state__12 = True, state__43 = False, state__10 = True, state__59 = False, state__17 = True, state__56 = False, state__48 = True, state__31 = True, state__36 = False, state__8 = True, state__58 = True, state__24 = True, state__33 = False])```
This is the initial state (=seed) of the RNG. We can recover the following 512bits of outputs by simply modifying the original code, resulting:
```6649072325173565167790166607303544343236044285056890707110072554988785350596422550050892070579043919783725646730179370397111189029461357122780521673335594```
Now xor it with the given number (`potions_count`) and successfully get flag:
`Aero{b3_c4r3ful_n0t_4ll_p0t10ns_4r3_g00d_f0r_h34lth}`
Great!