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

def 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): y
A 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 the actual value of ingredients.

The calculation of creating potion above can be treated as manipulation of matrix. If we define

$$\begin{array}{rl}\text{boldsymbol}A=& \mathtt{\text{amounts[]}}\\ \text{boldsymbol}s=& \mathtt{\text{ingredients}}\\ n=& \mathtt{\text{ingredients\_count}}\\ \text{boldsymbol}e=& \mathtt{\text{side\_effect[]}}\\ \text{boldsymbol}b=& \mathtt{\text{effect[]}}\\ q=& \mathtt{\text{magic\_constant}}\end{array}$$

the calculation can be described as:

$$\begin{array}{r}\text{boldsymbol}A\text{boldsymbol}s+\text{boldsymbol}e=\text{boldsymbol}bmodq\end{array}$$

And we know

$\text{boldsymbol}A$,

$\text{boldsymbol}b$, and

$q$… well, that is what exactly LWE cryptosystem is!

Using a lattice for attacking LWE is very common. In this case, there are too many bits in

$q$ and the error

$\text{boldsymbol}e$ is relatively small. It is very likely to break this cipher by lattice attack.

Solving LWE is reducted into CVP in the lattice theory. First break the equation into rows:

$$\{\begin{array}{l}\text{boldsymbol}{a}_1\text{boldsymbol}s+e_1=b_{1}modq\\ \text{boldsymbol}{a}_2\text{boldsymbol}s+e_2=b_{2}modq\\ ⋮\\ \text{boldsymbol}{a}_m\text{boldsymbol}s+e_m=b_{m}modq\end{array}$$

and erase the modulo by introducing coefficient

$k_1,\dots ,k_n\in \mathbb{Z}$:

$$\{\begin{array}{l}\text{boldsymbol}{a}_1\text{boldsymbol}s+k_{1}q=b_1-e_1\\ \text{boldsymbol}{a}_2\text{boldsymbol}s+k_{2}q=b_2-e_2\\ ⋮\\ \text{boldsymbol}{a}_m\text{boldsymbol}s+k_{m}q=b_m-e_m\end{array}$$

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 & & ⋮& 0& q& & ⋮\\ ⋮& & \ddots & ⋮& ⋮& & \ddots & ⋮\\ a_{m1}& \cdots & \cdots & a_{mn}& 0& \cdots & \cdots & q\end{array}\right]\left[\begin{array}{c}{s}_1\\ ⋮\\ s_n\\ k_1\\ ⋮\\ k_m\end{array}\right]=\text{boldsymbol}b-\text{boldsymbol}e$$

and also can be written as following:

$$s_1\left[\begin{array}{c}{a}_{11}\\ a_{21}\\ ⋮\\ a_{m1}\end{array}\right]+\cdots +s_n\left[\begin{array}{c}{a}_{1n}\\ a_2\\ ⋮\\ a_{mn}\end{array}\right]+k_1\left[\begin{array}{c}q\\ 0\\ ⋮\\ 0\end{array}\right]+k_2\left[\begin{array}{c}0\\ q\\ ⋮\\ 0\end{array}\right]+\cdots +k_m\left[\begin{array}{c}0\\ 0\\ ⋮\\ q\end{array}\right]=\text{boldsymbol}b-\text{boldsymbol}e$$

This is considered as a lattice, with

$n+m$ base vectors and targetting

$\text{boldsymbol}b$ with a (relatively) small error

$\text{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

$\text{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, 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:

	from sage.modules.free_module_integer import IntegerLattice
	from random import randint
	import sys
	from itertools import starmap
	from operator import mul
	# Babai's Nearest Plane algorithm
	# from: http://mslc.ctf.su/wp/plaidctf-2016-sexec-crypto-300/
	def Babai_closest_vector(M, G, target):
	small = target
	for _ in range(1):
	for i in reversed(range(M.nrows())):
	c = ((small * G[i]) / (G[i] * G[i])).round()
	small -= M[i] * c
	return target - small
	m = 100
	n = 12
	q = 1046961993706256953070441
	A_values = [[432963764937, 1734018663110, 341889949567, 1898982667391, 2077151719276, 1407002783602, 1284167537027, 1834426568578, 285492081118, 2058066808411, 682725745551, 212794466530], [1520127565791, 1613928435234, 1481625614519, 513222175065, 1825760063135, 849601240471, 2028256612679, 884310262235, 240010057040, 992839358285, 923505774812, 383090205845], [1101701826759, 579755276606, 1679688888621, 2024518241198, 860054720347, 1116564024705, 589730482574, 360441751468, 1509110655549, 209728670419, 590101198773, 1132857579083], [2145865348334, 712881695579, 493900571678, 709094726199, 2012239934926, 1944402267362, 258292513751, 1764614293744, 941798668247, 426748444686, 798829055999, 1160730795921], [1492160858733, 1872863223836, 1889796062683, 659100703920, 1030657263164, 1833284936792, 827632716760, 219330876235, 248421700730, 346448737264, 1525349461858, 636639435527], [83082894249, 1039988014970, 102695237946, 2196528981766, 624386218452, 1543152008022, 1067281074437, 850757382016, 1833741786624, 369488342620, 697998875223, 659137791743], [304520368939, 104480385531, 365287988347, 574917543522, 215751596410, 7223892660, 1811846445016, 1502401485396, 1282574831827, 269041740296, 553385674063, 475354002884], [768225213922, 706735949631, 397048789995, 1175370153621, 1910090604414, 887353264455, 671406086293, 929826775368, 1204510817878, 1355027160116, 78304839001, 842053988515], [255538486847, 1401698734253, 1016906021885, 1704027715257, 583469046368, 358750586451, 1150682319699, 344044372511, 1032015901696, 1730015612177, 2162220214971, 1767839652202], [2006632728344, 790112749938, 508031558919, 2082337317375, 448968929655, 1414214282719, 1808366562208, 912319915699, 664114766901, 974817491833, 695174243589, 1609563926059], [1436900477897, 1553753235857, 463841158006, 1429068640922, 2061793340457, 580802599865, 770526736438, 1495205419904, 1206233235214, 1578352580616, 1095625556503, 1713252862559], [2017099004045, 588353446526, 276827969167, 169158325763, 468281087107, 1388845242155, 416588879006, 177935453008, 714541282422, 2172913200038, 1172115088612, 1411651166958], [324647923094, 852008352168, 725751570359, 74065035635, 1833306350775, 620711450603, 234219120008, 1615744416211, 905646085524, 312834222210, 132839454018, 198391294212], [540310357001, 1766144475897, 1556038226294, 1517139133878, 1032291339775, 1794869363811, 269209045714, 1401433580873, 203908104379, 190401172763, 192404742203, 762821431026], [1952465088096, 1156764636228, 852363417918, 2024229075808, 1307131596082, 449524583076, 144051635633, 904764909263, 2189675861584, 1730307560460, 983193442820, 212951533209], [939213248732, 555904720940, 77063493291, 995590579117, 1731667289603, 672614440876, 547117018940, 858230432384, 1004131275605, 1676733631604, 1131734760708, 1878878683398], [2138457657906, 323850555627, 1618155536662, 1908602807577, 112536517813, 1696964821127, 293853804532, 1625195444231, 171670571595, 1081421822332, 320147811844, 2136897794687], [513789068967, 1986087503122, 838788863642, 2003559382825, 1154492790279, 1541607381370, 1990637932216, 328266880457, 2096371668433, 1444749890102, 11959808384, 2001291608528], [2102856442550, 246117336196, 68265455204, 712396035652, 2138787150391, 1660150245418, 725621653667, 1771135066051, 1390785760702, 254586570730, 1972941929061, 1818436030393], [946898181952, 194835610752, 554405107434, 1405864441581, 1077244632928, 327633704746, 2115620731515, 1659533451153, 1632246692744, 1749601689332, 984765787230, 1124646752081], [192638840363, 2150984058206, 709550700840, 709644630842, 340874667445, 2084678206436, 1506137040057, 1747657555598, 1935416502789, 473980548572, 1364080414649, 904895351825], [318849992562, 135532151794, 1178552370715, 889895840268, 1710609279109, 183944613870, 1852301174538, 1482760559085, 1310303719885, 2024110977244, 811396907891, 1365892519997], [2123981818418, 1813543068137, 1983952993316, 2120271504889, 1146537229407, 271771651686, 899686738135, 1447661086127, 1986127027593, 1002665964725, 1515729034443, 2172382968118], [1431847048607, 24909262854, 1697635646427, 13269365739, 1067173491601, 847437155603, 473039016297, 1550957910085, 513201023795, 837819065335, 1162364208517, 1750591891158], [1220182156386, 748313297340, 661332736481, 808694401129, 1609743643332, 512262620132, 1334278181282, 1570597195131, 1307318080094, 1916955371412, 1655615027244, 1017354487337], [1722924411338, 272078573623, 1394385504892, 231931156296, 2052634184898, 908365826089, 1609322857312, 1596762940527, 1327278892833, 1961843330699, 419575058660, 2195594233280], [698132527097, 161324065065, 1812097147496, 2107426444111, 1313982144764, 1348406752518, 1185050744002, 1263248810398, 329460928358, 1181234659427, 1964689802402, 357401502374], [1770546936051, 239617374674, 1318158898745, 427396641853, 792641039792, 1600696035608, 1650780073767, 2146517453475, 1901932646084, 126174601112, 2033844414420, 283855370876], [1341300400490, 1207587747904, 1734700266562, 974590528235, 161746207184, 888456689044, 1903333588403, 1923789349118, 1286981833891, 448766381320, 164708697227, 1866046383352], [680662624262, 1338318250232, 894017793915, 591707383914, 2127062006626, 1306517284501, 197745464952, 238895620568, 2102650005387, 1823313005404, 242428862428, 1845204226713], [225616533526, 313662551208, 1219584406147, 1340787036501, 1384932485272, 895196474595, 508087746747, 422049801253, 1202562145656, 1478989337614, 1197194141890, 25127506722], [25492662659, 857700490650, 331963441694, 1126095551268, 623963369838, 1980465976406, 278616527948, 379352399514, 148835829984, 595159418762, 1600209555693, 116327937147], [906029460590, 118917519326, 190199086540, 897613816795, 788678863872, 763408103325, 912155124470, 987264773268, 1688806660323, 665238624095, 850363001694, 1387675666041], [726847082429, 1969388660863, 184553855230, 1614251782147, 178131106232, 929387893014, 867986891433, 864031240021, 1988356913623, 1702817061757, 1248822320972, 50884893771], [867494301330, 2031724930426, 532010386612, 1865166424267, 1583237668662, 1194843262711, 166581105474, 2189061537364, 448586344920, 1811921095843, 233005856659, 2013918907931], [705601486204, 1339099093597, 247493990424, 408472092982, 570509580900, 134824965243, 926558262323, 1958229422211, 1444958290598, 1488325512562, 850053512156, 1219227074064], [1224478400636, 47506840312, 1072984906736, 1167068703110, 291103161887, 255557655960, 1961107248667, 1530149533528, 1817513759859, 2196582216962, 574338822773, 650534991954], [1983886537607, 313569227439, 528747318547, 688950032209, 1144022765153, 348460180862, 1837399075996, 867426169054, 910799972889, 506420829121, 1195323847023, 1096556513687], [1123843439946, 1978622056610, 898329859402, 619974041301, 674350841482, 302342173115, 376785379908, 2120311421239, 1920305936172, 2189094204418, 887318664061, 69141677091], [1762165864775, 155697089518, 1041021281936, 7050624368, 162196181677, 1450398755971, 2184914349389, 458421582192, 2001982411315, 1980377793129, 2002672777287, 1564659515550], [958194851625, 871302015911, 1348835789167, 1217944526699, 1350666801102, 2060774779507, 871640578553, 793362863179, 254184801385, 259923048251, 10195792282, 1775517849231], [187830969359, 1975535798361, 1422188056398, 1946258358500, 52610682675, 88186964706, 1383951729962, 1055188935046, 2061589029644, 1762195755151, 1935655115315, 769388259157], [310671430548, 10192525439, 149501417590, 334553928670, 178170960669, 1006996935940, 503450426314, 1424634857238, 1165419692225, 503866990024, 1868351370876, 723604273856], [386449512727, 864610785780, 1908939655877, 981806227105, 80601572510, 2120728253209, 1003367415212, 1108057611121, 1592644583389, 447904219610, 1831487891681, 19942657477], [868512077227, 584469863509, 1258537721027, 803887713352, 1402135147548, 734046633886, 1142022075114, 2019086220606, 2196164989345, 1877298161139, 885208648086, 807498890573], [1096841381658, 42413214294, 1637751294735, 2147686265901, 1824053771283, 1110536376526, 1591300455858, 242777179180, 1677919947707, 900312552591, 2028603841603, 705944605831], [1872458416134, 2110697558147, 179051131604, 2146965920658, 1332497302934, 1831637583695, 2154260471976, 1659285390154, 387211752086, 1820158158934, 221322606596, 701602414375], [804694390644, 1024469912939, 1698132347597, 1086405318771, 681813856593, 2045390619322, 815354871709, 870256607381, 1736243846338, 1887576725780, 770791973591, 1183513879976], [1742433564211, 346089653963, 139257622471, 404279839448, 2049985723921, 279038879734, 1917897411363, 1468861220004, 723827140572, 323437675717, 162098541700, 1842705216173], [283035063923, 1122652112143, 1080489653082, 1315416465002, 1273387377124, 829269159070, 929939964243, 739849026778, 2162408817145, 1407488336099, 1069236872238, 1334472596697], [1414192047488, 1872825081442, 2087876032222, 381329687491, 123187086445, 2092186308801, 2055981456717, 1085495354668, 1663039123402, 1646114602366, 1424125098382, 1038520717598], [1526725029446, 1881784143027, 1494803611891, 1476579095707, 2196162861245, 1272074898735, 694991641272, 1701720997992, 523353198407, 1810771185699, 1215663276734, 1709461292581], [1393601514454, 709617954599, 368076627373, 424227657365, 1561163971516, 1686019594175, 487075200483, 416870166379, 186371433798, 2162605641077, 2162636048958, 1272841954561], [527235380195, 1087926535162, 406985228690, 1436183960381, 988090894778, 625466453498, 1885000375775, 1264476387796, 400965893857, 1682634935680, 982498733473, 1866340126756], [1569415239675, 1157273998315, 448369590564, 1221334676793, 1941203630728, 246353371564, 489935690331, 1526064886380, 54866020731, 248333682713, 1316076795409, 2077645304649], [2108979609195, 1535683503317, 895466147424, 1523450994399, 1401616699223, 401554733839, 1793269160716, 1339667982766, 1552703333696, 1040882283279, 566867873903, 1159307549009], [1070725633820, 1198109464256, 1855472728887, 1971828326245, 532830217404, 957538001586, 498304046467, 992449184246, 1900407767249, 1949307817271, 2175465566301, 2022232536982], [1320407041050, 766590197207, 483230384242, 10580232237, 274132617994, 665628457690, 1733587315909, 1742992316672, 2110253868174, 1075404304192, 1563092738671, 403681306019], [1473903582526, 1799656243954, 1152863199111, 1209694104077, 1272671798386, 2057303261066, 1497728087670, 588728085682, 1301038925651, 1199700311075, 1298847314044, 1105494246692], [1448745552514, 1110403418523, 1343653779281, 1306765546946, 1019183938317, 2045701018330, 1813713977445, 1854649736141, 1150591662809, 1757629249244, 24020807950, 1085418658633], [1338405967834, 159074548809, 316847415555, 1229294597770, 856783868894, 1881694135156, 1801080701256, 354969823359, 1904052866782, 639206211981, 502495777241, 1740674829829], [234843293193, 2172976613395, 363810146037, 2135890559636, 1955022781427, 537489566065, 1909903655826, 1033976414978, 862992455469, 1499399803984, 1746689918603, 145588625054], [1321718504575, 431077882674, 287933796173, 1692551127307, 16838677375, 786189494657, 1321093229328, 1117944689034, 1686199636844, 1172569015295, 177723651287, 1022902953082], [839257147587, 1349408177884, 1490786440342, 1780444822281, 770922270267, 57444920438, 339935823897, 1368240118293, 992397904354, 1364572586218, 2102252236905, 2095582589789], [978715088154, 1048544175534, 291060708784, 5863503630, 1873842929654, 308644285867, 273098180858, 857586934540, 1426598075439, 261563639741, 2130397064193, 1247760076795], [1365072331427, 46506043735, 1151508919349, 1642506447335, 714743477587, 969967150887, 2191637417567, 1132673653739, 552479970293, 1558924380782, 242149852471, 877763638426], [1078613869205, 879864455938, 2173553117405, 198446896627, 1641932685273, 2160600816356, 89525032555, 879078189040, 1122930896798, 1637061856577, 2082115649793, 402810311913], [402996550924, 409803970167, 2127813643661, 285812197785, 125293814620, 2153421361756, 261662560366, 1193986400277, 702330919610, 630202837275, 1428220822604, 1554797110283], [1489691244439, 1297380208397, 340520443770, 934302783224, 1252452506863, 199553519898, 869253654784, 668499388793, 600399829043, 1314983901913, 1195050056972, 1075550034136], [1126594473121, 265617845632, 2025552399661, 762605633921, 483315738986, 67782378028, 1772856291452, 1692964110326, 887683695934, 1299756122515, 1981107956107, 506711419504], [4223574474, 465364775279, 562009862398, 1662625485270, 1141564839160, 756472182433, 506043264194, 2072816956678, 1092553403871, 408988046569, 1071227977372, 1994699797711], [444060346445, 742236636817, 1322409961810, 905619584812, 1911408742356, 1567395770398, 1475158838622, 1731225282472, 1945257421443, 1232014590628, 1959897722177, 296847366475], [1709440139157, 1898990022154, 1609556562931, 276507916971, 1988459960636, 309465213787, 1219434802449, 1404153976093, 62639299214, 180576455586, 49668058127, 747279552071], [519450752904, 256819941888, 203145514018, 1050932838011, 673819000126, 2015860038863, 433001966396, 790239986699, 1835676479154, 1089422338767, 1862395149515, 2143512112340], [674011832957, 450311176408, 1780642673265, 1410678015618, 601178529849, 272039056177, 1541290003173, 1665504099391, 1880786686649, 1723844866707, 1241174092109, 417883303700], [1572890691585, 1775490699529, 845880597864, 2101513798141, 143578800592, 930571452607, 1867377376479, 788249932996, 2044789813310, 1566494953684, 872999219649, 1046481060090], [698553375707, 349023568780, 521507019831, 2055725466871, 633857398045, 1552963937073, 1983235506952, 684680710708, 1935067029261, 2042496456370, 1343327511293, 502249801280], [811984645062, 1913147798332, 509709462212, 1652756887641, 568071922671, 2077704727270, 1369427198734, 1261796613078, 733297338581, 1993945663238, 780896942345, 16927824545], [396761731732, 1206462513633, 207769258517, 2103715610607, 104308403919, 1966642225985, 1094396111312, 695586770790, 564881525352, 1768864943490, 336499889733, 1566608925457], [394166158736, 729538767612, 1031032920885, 1419849594482, 1549283861, 1090526010208, 86911491880, 668441851366, 1885781785483, 27639599884, 1598767823761, 1435776963385], [1606897077261, 720626698747, 1939728425044, 1772333556270, 240840363289, 32654435220, 2117662622147, 745001138084, 222381515792, 652181069051, 1463399211440, 1788587710957], [628259722543, 1370623731829, 82779109840, 165543161944, 842033900344, 1934122243966, 1902724696802, 46620185757, 5352415413, 1176159889314, 1255856070417, 1414117976988], [693641865293, 2102657704795, 1495028714457, 1007772528991, 983667631061, 293952079058, 1611080249147, 857846707148, 1971854341825, 657090731765, 683454491654, 1665562379837], [109316211612, 219947786273, 894911062987, 1141647477379, 49426089161, 1583841729106, 1657205293524, 854099910144, 781812578836, 224298673767, 367051650470, 714609088720], [633136053195, 1338722323837, 1372342208746, 1651205104710, 1416362076763, 1103837113439, 1408648739554, 1520547994306, 2104782012343, 476790088093, 909456154336, 568460191082], [519973542327, 145604485152, 18768521765, 1024195486720, 637927553625, 1430002338433, 1745896929716, 1447204118632, 858736551795, 1586771694107, 730137115219, 1374838749132], [63793189525, 509021968267, 1907797173081, 1884997733962, 1383438087533, 1844311745326, 294336997177, 1227853944928, 2066199655124, 2048296071749, 1739673474035, 408509787879], [204407141413, 938619978971, 268200026, 1989105747620, 510934826195, 660770854496, 1804536457689, 1210293605248, 1733411734103, 413798343442, 117286015489, 1795063667797], [2083710927791, 407241634435, 1526426389500, 1055534551365, 1950278161919, 1515186934934, 1963872669936, 1315063569167, 1036817807730, 231890272788, 862040193565, 983291467909], [1040849323826, 811095857401, 1115914170627, 1439938719419, 1725881545271, 1158231852721, 977478507531, 2164813836004, 816771963, 1108565884826, 549566110849, 1491408126609], [1381102387066, 1944592442409, 2163109986571, 532996523162, 1553161957437, 942585778026, 1864580734394, 931387226893, 1173929002538, 1113716705487, 526932453035, 866298089888], [2043769639521, 1999476644619, 888836326727, 1422669479271, 208107969391, 1346029359607, 30221108547, 61668310026, 463873157294, 120948802983, 659496306454, 343644788018], [463680149953, 2105859784056, 830399407482, 1783033835531, 1156686780193, 882046095924, 1659371129740, 1345748101900, 769205989803, 791883253207, 1543332569698, 1392300421109], [19268805341, 1015114584468, 513288336070, 1746853021453, 1939691417413, 1612923167297, 326405095650, 40284887467, 847100335636, 1055593542167, 666007907442, 607125503802], [1297426677140, 194887835535, 5190446265, 347855990489, 702524426734, 1288079657345, 555521610494, 1724617460649, 1050813948199, 1530073607904, 568470586704, 334651647716], [1111519163737, 1121476861742, 1416073504486, 1765100568383, 1517550317492, 943142697678, 1081416817754, 543813133086, 2000412985748, 2131215090411, 1735948320131, 1312077631731], [469249776404, 1948681416932, 1835375642933, 351662168941, 1224308685384, 1116260533979, 533327044869, 745337036301, 509237346034, 1783675555750, 1349234987790, 1870711697625], [2159802029821, 1303032673713, 1320265915444, 513641365466, 1529456786666, 1251079585810, 1264500013849, 1213212049679, 1668414036912, 2167270068960, 318217697168, 576374695912], [1065288411375, 1509971579806, 187223695446, 909018564656, 1424625899384, 1526643143984, 180730542103, 334603945082, 953019698611, 1319780720675, 568009221802, 1376837427812], [353615797819, 779510410363, 634337418618, 112328801072, 1308573457212, 1018471322967, 2191760622378, 1641311358023, 126717015375, 790498704391, 2029952294067, 1080095433537]]
	b_values = [675829748828112222653599, 19282755083699178123269, 678436649010458903205058, 369269068465810324168668, 985003784677656180129985, 302550934486352707090601, 293615522846897487129032, 786500908938082399700302, 579706331608910031828558, 136215398670659802777453, 480694562908917705162021, 560232039771932380765016, 503842457537242219123462, 371022864302057124577014, 995285726293200902651498, 511135488573285172390781, 406332541907748912445623, 64976747594853792180181, 622088533358028260372893, 923282752273883420665599, 723189980097309723092905, 113205315310498546359277, 559924175990752214286619, 500361794215386623766971, 264975606806442217831414, 695260697358296089495727, 530523315113556155844756, 15426800229550499851233, 161464190402734389224389, 139775511063366648308276, 763807623777555762201967, 534935672775949337618714, 193929369787602620599758, 232176016150290974119526, 606257022204867681176247, 91123464738298399809703, 266148568273413451208142, 307278389042046740655819, 175512006840496943188244, 32878792885747499102364, 513454468429895818957677, 33616424149677969819928, 666519009106137978956330, 479090649272470836287360, 931246929391630904786202, 346355675573292324651293, 1045965942572852285465083, 874368247779367833092211, 480309596987681169470644, 398745054387905745112887, 727745975262204938625645, 536282696957881149366607, 917050812288442286476258, 968536396900054739602969, 444102502920870237780302, 1011964345526846015789017, 1007394247360164670481117, 459018927985707788897502, 293672351248683895502981, 986867295499561561109289, 475667518424628957098510, 491959295744872690366329, 132559354447319837553255, 6944124517931759676428, 306726499609833273410776, 56554457195691332306508, 202635171894963165665452, 893027655184230968252975, 787826479075320420759597, 109845597928983197937244, 668720532113201200503211, 749454109912280740519613, 276061528480480768464309, 630745096301664257786157, 186492444390810706243944, 398519478006565020789631, 759696068142013706377021, 332796614703267448013263, 45225156157674211763302, 790985220117110070340583, 340497774827772526781788, 481286424371542803000452, 883919316594213134808588, 642424796020883205219500, 610501796024842413891191, 348411348661058428992391, 734763041221733532976266, 37601381899664267311776, 348363023551208062306412, 581292279862020141335330, 209426765857030314592639, 627530597965534112514516, 264830541125932321199169, 270304137586581183193738, 944893386016454335831219, 825285026655290918345294, 465745201543131679294819, 401163253661371827564326, 822082026461895291797295, 64147717148582160182619]
	A = matrix(ZZ, m + n, m)
	for i in range(m):
	A[i, i] = q
	for x in range(m):
	for y in range(n):
	A[m + y, x] = A_values[x][y]
	lattice = IntegerLattice(A, lll_reduce=True)
	print("LLL done")
	gram = lattice.reduced_basis.gram_schmidt()[0]
	target = vector(ZZ, b_values)
	res = Babai_closest_vector(lattice.reduced_basis, gram, target)
	print("Closest Vector: {}".format(res))
	R = IntegerModRing(q)
	M = Matrix(R, A_values)
	ingredients = M.solve_right(res)
	print("Ingredients: {}".format(ingredients))
	for row, b in zip(A_values, b_values):
	effect = sum(starmap(mul, zip(map(int, ingredients), row))) % q
	assert(abs(b - effect) < 2 ** 37)
	print("ok")

view raw solve.sage hosted with ❤ by GitHub

Note that SageMath implements 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\times 12$ bits of RNG output. Let's move into RNG.

The generation of bits can be seen here in the given code:

    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!

	from z3 import *
	outputs = '011110100001111101000100001101011111010110000110100010101011101110110110100000101110000011101000001001011010100111000110100111011100001000010010111100000000000001001011000010110001001111111011100010010110101001000001110111111110000111110000010001011101101101100010111011101101001010110000001011010110011110011101001001000111101000011001100111001010011101100000011111001101001111000010000010101111000111101100000111010000010110100010011100111010001000100000000110100110110101110000110111111000001010111100000100110011001011100111101110011111001011110010000000101110010011001101101011101011001100111010101111010111011100011110111010001100111010100010110000101010100100010001010110101100101000111001111000111011000000001000001110100000110000101101110111000000000010011011'
	initial_state = BoolVector('state', 64)
	solver = Solver()
	state = initial_state
	for _ in range(512):
	new_state = [None] * 64
	for i in range(64):
	a = state[(i - 1) % 64]
	b = state[i % 64]
	c = state[(i + 1) % 64]
	new_state[i] = Xor(Or(a, b), c)
	state = new_state
	for output in outputs:
	new_state = [None] * 64
	for i in range(64):
	a = state[(i - 1) % 64]
	b = state[i % 64]
	c = state[(i + 1) % 64]
	new_state[i] = Xor(Or(a, b), c)
	state = new_state
	solver.add(state[0] == (output == '1'))
	print('Solving...')
	assert(solver.check() == sat)
	model = solver.model()
	print('SAT', model)

view raw solve.py hosted with ❤ by GitHub

Execute and wait for a few minites… and yes, SAT!

$ python2 solve.py
Solving...
('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!