对称之美
题目
Vernam 密码
import random
import string
import itertools
from secret import FLAG
key = ''.join(random.choices(string.ascii_letters + string.digits, k=16))
cipher = bytes([ord(m)^ord(k) for m, k in zip(FLAG, itertools.cycle(key))])
print(cipher)
思路
由于给了大量的密文，完全可以对密钥空间进行范围上的缩小。
由于进行的是异或操作，且明文与密钥均为可见字符，只需要对相同位置的密文与所有可能的密钥字符进行异或计算，结果不在可见字符范围内的均可以排除掉。
经过初步筛选后密钥空间会小很多，进行爆破或者根据上下文手动选择即可。
代码
import string
import itertools
key = string.ascii_letters + string.digits
# first = [94, 116, 57, 32, 54, 49, 33, 32, 54, 38, 116, 59, 37, 32, 32, 116, 60, 32, 57, 59, 51, 34, 38, 39, 116, 59, 116, 38, 60, 61, 35, 58, 39, 55, 59, 116, 49, 32, 48, 39, 55, 94, 59, 116, 38, 39, 116, 50, 59, 53, 48, 122, 60, 94, 116, 61, 54, 38, 38, 32, 39, 116, 56, 59, 53, 97, 1]
# first = [35, 25, 21, 25, 17, 2, 28, 3, 5, 21, 17, 3, 5, 80, 80, 18, 25, 31, 21, 31, 94, 21, 80, 4, 24, 31, 17, 3, 17, 4, 80, 80, 25, 17, 3, 0, 9, 24, 9, 25, 24, 17, 30, 3, 9, 80, 17, 17, 2, 80, 31, 80, 80, 22, 3, 3, 25, 9, 21, 24, 80, 17, 21, 80, 23, 93, 62]
# first = [78, 68, 89, 89, 91, 23, 83, 23, 67, 91, 89, 94, 82, 69, 78, 66, 89, 23, 67, 92, 23, 69, 67, 23, 86, 92, 89, 23, 83, 27, 67, 85, 84, 91, 82, 69, 25, 94, 23, 89, 94, 65, 23, 89, 23, 88, 23, 84, 23, 91, 64, 110, 68, 86, 78, 23, 91, 23, 23, 82, 61, 71, 68, 95, 13, 86, 89]
# first = [43, 102, 50, 33, 39, 76, 102, 50, 102, 39, 34, 50, 53, 35, 41, 53, 34, 53, 52, 102, 76, 39, 46, 47, 52, 102, 37, 43, 102, 102, 46, 41, 39, 106, 102, 35, 102, 53, 49, 33, 40, 41, 50, 39, 54, 52, 42, 35, 76, 47, 40, 41, 47, 37, 43, 47, 39, 39, 36, 52, 34, 54, 53, 35, 102, 25, 63]
# first = [3, 25, 29, 78, 0, 1, 12, 6, 7, 26, 78, 7, 64, 15, 27, 23, 78, 11, 23, 15, 58, 2, 7, 29, 10, 8, 7, 15, 100, 12, 15, 10, 2, 78, 1, 10, 100, 78, 6, 78, 9, 7, 6, 28, 15, 78, 1, 78, 15, 0, 78, 27, 10, 11, 3, 29, 26, 0, 1, 78, 7, 11, 78, 28, 100, 27, 49]
# first = [31, 18, 90, 21, 25, 15, 31, 31, 14, 31, 112, 21, 112, 22, 8, 90, 14, 31, 90, 14, 18, 90, 9, 90, 87, 21, 31, 3, 27, 15, 14, 19, 22, 27, 28, 27, 46, 25, 31, 27, 90, 30, 31, 22, 25, 24, 21, 19, 20, 31, 14, 93, 31, 90, 31, 90, 31, 30, 14, 9, 12, 27, 14, 31, 18, 41, 57]
# first = [69, 84, 94, 67, 84, 69, 17, 92, 17, 17, 94, 95, 104, 88, 17, 70, 89, 90, 70, 17, 84, 67, 31, 69, 70, 67, 95, 17, 17, 69, 17, 84, 72, 66, 17, 69, 89, 80, 69, 17, 85, 88, 17, 88, 90, 84, 90, 95, 85, 17, 89, 93, 66, 80, 69, 59, 67, 17, 89, 88, 88, 67, 89, 17, 86, 2, 0]
# first = [65, 93, 85, 19, 19, 29, 71, 64, 80, 71, 71, 82, 92, 73, 81, 92, 86, 19, 91, 82, 65, 86, 19, 91, 90, 19, 71, 93, 93, 19, 71, 64, 19, 19, 67, 92, 86, 94, 91, 94, 90, 93, 94, 93, 19, 82, 19, 19, 19, 64, 86, 95, 19, 65, 65, 88, 82, 90, 19, 87, 87, 19, 86, 90, 82, 85, 67]
# first = [49, 104, 104, 44, 45, 104, 32, 45, 41, 39, 32, 36, 61, 45, 58, 58, 104, 66, 45, 104, 45, 41, 28, 41, 58, 66, 104, 39, 41, 60, 32, 104, 59, 66, 39, 58, 58, 45, 45, 41, 38, 47, 45, 47, 39, 58, 41, 60, 33, 60, 104, 104, 39, 45, 33, 38, 36, 60, 59, 45, 33, 37, 104, 59, 37, 29, 0]
# first = [119, 35, 93, 37, 54, 3, 50, 59, 57, 119, 50, 119, 119, 119, 54, 60, 36, 56, 57, 39, 119, 36, 63, 35, 50, 62, 54, 35, 58, 63, 50, 32, 46, 32, 35, 36, 50, 119, 37, 35, 57, 119, 57, 123, 49, 36, 35, 63, 58, 37, 93, 36, 49, 119, 52, 56, 119, 112, 62, 119, 57, 56, 36, 119, 50, 102, 100]
# first = [57, 56, 49, 49, 51, 56, 112, 38, 112, 51, 34, 36, 61, 57, 57, 57, 51, 37, 112, 49, 49, 63, 53, 112, 52, 36, 62, 112, 53, 53, 57, 53, 61, 53, 53, 112, 54, 57, 112, 53, 53, 50, 37, 112, 112, 113, 112, 53, 49, 49, 61, 53, 112, 32, 49, 39, 35, 35, 52, 63, 55, 34, 49, 36, 43, 123, 34]
# first = [87, 92, 25, 78, 81, 80, 86, 92, 88, 86, 25, 92, 88, 77, 87, 87, 92, 77, 64, 80, 75, 87, 25, 78, 25, 23, 90, 81, 25, 64, 75, 75, 84, 75, 87, 86, 86, 87, 51, 21, 75, 92, 25, 51, 78, 51, 64, 25, 94, 80, 80, 92, 64, 75, 85, 87, 64, 25, 92, 95, 25, 92, 84, 81, 97, 13, 68]
# first = [65, 65, 17, 8, 65, 18, 3, 18, 13, 13, 2, 2, 24, 77, 65, 6, 15, 65, 14, 15, 4, 18, 107, 4, 21, 65, 4, 0, 7, 65, 65, 4, 4, 4, 21, 19, 19, 65, 2, 65, 65, 8, 14, 9, 14, 53, 14, 12, 8, 6, 5, 65, 14, 4, 79, 65, 12, 107, 18, 65, 13, 65, 4, 4, 81, 15, 107]
# first = [57, 61, 57, 54, 55, 120, 50, 116, 43, 55, 55, 48, 120, 120, 82, 120, 61, 43, 45, 44, 120, 120, 62, 127, 55, 23, 43, 46, 55, 51, 82, 120, 44, 120, 49, 120, 61, 48, 48, 59, 55, 54, 62, 45, 52, 57, 45, 49, 54, 48, 60, 58, 45, 44, 120, 57, 53, 47, 120, 44, 49, 55, 118, 120, 42, 60]
# first = [5, 27, 30, 16, 3, 20, 18, 87, 24, 5, 26, 25, 25, 21, 30, 21, 4, 14, 87, 30, 4, 17, 30, 5, 87, 2, 3, 18, 5, 25, 24, 21, 5, 3, 22, 7, 91, 22, 24, 22, 5, 16, 87, 25, 1, 28, 5, 5, 18, 3, 27, 24, 5, 3, 35, 4, 18, 31, 18, 31, 25, 5, 125, 17, 40, 83]
# first = [38, 55, 60, 114, 58, 61, 49, 88, 114, 33, 34, 59, 61, 39, 33, 55, 114, 63, 62, 60, 55, 61, 32, 55, 62, 32, 61, 114, 114, 55, 37, 51, 59, 58, 62, 32, 114, 60, 61, 38, 114, 114, 51, 53, 55, 55, 114, 32, 114, 114, 55, 38, 114, 43, 58, 114, 38, 55, 59, 59, 55, 114, 1, 62, 59, 52]
def test(char):
for c in first:
num = ord(char) ^ c
if (num < 0x20 or 0x7f <= num) and num != 0x0a: # 可能出现换行符
return False
return True
for c in key:
if (test(c)):
print (c, end = ' ')
print()
# T
# b d e k l o p q r s t u w x y final: p
# 7
# F
# n
# z
# b 1
# a c d e f g h i j k m n o p q r s t u v w x y z 0 1 2 3 4 5 7 9 final: 3
# H
# W
# C D E O P Q R S U V W final: P
# k 9
# a
# X
# w
# x R
将密文每十六个分一组，每一组相同位置对应的密钥应该是同一个，因此将这些密文字符组成一个 list，这里命名为 first。
对每一个位置进行密钥的初筛，最终可以得到代码块下面的注释所示的密钥空间
随便选择一组密钥进行解密运算
key = 'Tp7Fnz13HWP9aXwR'
a = (bytes([m ^ ord(k) for m, k in zip(cipher, itertools.cycle(key))]))
print (a)
对这些密钥进行手动筛查并更新密钥即可，过程如下。
b'\nLymmet y zn Art vs whe< t{e Elemznts o4 \nr pAintvng orrdrrwiNg b~lancereaph Othem \nout| T{is\x00cousd be &he3obJectl them!elees\x0c \nbjt it 1an3alSo rzlate &o polOrs ~nd \no&hea cOmpolition3l gecHniqjes.\nY=u ~ay\x00not?reali(e zt,\x00but?your 0razn *is }usy w=rkzng\x00behvnd th7 spenEs tp seekr\noft Symmztry w:en3yoU lopk at 3 prinTing1 \nThe e rre\x00sevzral r7as|ns\x00for?this.rThv \nFirsk is t:at3we\x07re ward-w;rew tO lopk forr\nig. our ~ncien& a}ceStorl may <ot3haVe h~d \na <amv fOr ik, butrthvy Knew?that &hezr *own?bodie! wvre\x00basvcallyrsy~meTric~l, asr\nwvre\x00thole of "otvntIal oredat=rs3or\x00pref. \nTh7reuorE, twis ca?e zn Handf whet:er3\ncHoosvng a ?atv, Catcwing d;nnvr Or \n~voidi<g qeiNg oq the ?enf oF a lnarli<g,3\nhUngrf packrof3woLves?or be3rs2\nTAke ~ lookrat3yoUr f~ce inrthv mIrrom \nandrimrgiNe a?line !trrigHt dpwn th7 \n~idDle.?You\'l> sve Both?sidesrof3yoUr \nyace a e creTty lymmet icrl.\x00Thil is \n9nodn As bvlater3l `ymMetrf and ;t\'` \nWherz bothrsiwes\x00eitwer si6e |f This?\ndivi6int lIne ~ppearrmoae Or lzss th7 srme\x0e\nSo?here ;s ghe\x00flax: \nhg3mehX0R_i52a_uS34U184nD$fUQny_C1"H3a}\n'
ubuntu@DESKTOP:/mnt/d/HGAME/cipher$ python3
Python 3.8.5 (default, Jul 28 2020, 12:59:40)
[GCC 9.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> ord('x') ^ ord('o') ^ ord('g')
112
>>> chr(112)
'p'
>>>
ubuntu@DESKTOP:/mnt/d/HGAME/cipher$ python3 solve.py
1069
b'\nSymmet y zn Art is whe< t{e Elements o4 \nr pAinting orrdrrwiNg balancereaph Other \nout| T{is\x00could be &he3obJects them!elees\x0c \nbut it 1an3alSo relate &o polOrs and \no&hea cOmposition3l gecHniques.\nY=u ~ay\x00not reali(e zt,\x00but your 0razn *is busy w=rkzng\x00behind th7 spenEs to seekr\noft Symmetry w:en3yoU look at 3 prinTing. \nThe e rre\x00several r7as|ns\x00for this.rThv \nFirst is t:at3we\x07re hard-w;rew tO look forr\nig. our ancien& a}ceStors may <ot3haVe had \na <amv fOr it, butrthvy Knew that &hezr *own bodie! wvre\x00basicallyrsy~meTrical, asr\nwvre\x00those of "otvntIal predat=rs3or\x00prey. \nTh7reuorE, this ca?e zn Handy whet:er3\ncHoosing a ?atv, Catching d;nnvr Or \navoidi<g qeiNg on the ?enf oF a snarli<g,3\nhUngry packrof3woLves or be3rs2\nTAke a lookrat3yoUr face inrthv mIrror \nandrimrgiNe a line !trrigHt down th7 \n~idDle. You\'l> sve Both sidesrof3yoUr \nface a e creTty symmet icrl.\x00This is \n9nodn As bilater3l `ymMetry and ;t\'` \nWhere bothrsiwes\x00either si6e |f This \ndivi6int lIne appearrmoae Or less th7 srme\x0e\nSo here ;s ghe\x00flag: \nhg3mehX0R_i5-a_uS34U184nD$fUNny_C1"H3a}\n'
ubuntu@DESKTOP:/mnt/d/HGAME/cipher$ python3
Python 3.8.5 (default, Jul 28 2020, 12:59:40)
[GCC 9.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> ord(';') ^ ord('a') ^ ord('i')
51
>>> chr(51)
'3'
>>>
ubuntu@DESKTOP:/mnt/d/HGAME/cipher$ python3 solve.py
1069
b"\nSymmetry zn Art is when t{e Elements of \nr pAinting or drrwiNg balance eaph Other \nout. T{is\x00could be the3obJects themselees\x0c \nbut it can3alSo relate to polOrs and \nothea cOmpositional gecHniques.\nYou ~ay\x00not realize zt,\x00but your brazn *is busy workzng\x00behind the spenEs to seek \noft Symmetry when3yoU look at a prinTing. \nThere rre\x00several reas|ns\x00for this. Thv \nFirst is that3we\x07re hard-wirew tO look for \nig. our ancient a}ceStors may not3haVe had \na namv fOr it, but thvy Knew that thezr *own bodies wvre\x00basically sy~meTrical, as \nwvre\x00those of potvntIal predators3or\x00prey. \nThereuorE, this came zn Handy whether3\ncHoosing a matv, Catching dinnvr Or \navoiding qeiNg on the menf oF a snarling,3\nhUngry pack of3woLves or bears2\nTAke a look at3yoUr face in thv mIrror \nand imrgiNe a line strrigHt down the \n~idDle. You'll sve Both sides of3yoUr \nface are creTty symmetricrl.\x00This is \nknodn As bilateral `ymMetry and it'` \nWhere both siwes\x00either side |f This \ndividint lIne appear moae Or less the srme\x0e\nSo here is ghe\x00flag: \nhgamehX0R_i5-a_uS3fU184nD$fUNny_C1pH3a}\n"
ubuntu@DESKTOP:/mnt/d/HGAME/cipher$ python3
Python 3.8.5 (default, Jul 28 2020, 12:59:40)
[GCC 9.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> ord('x') ^ ord(' ')
88
>>> chr(88)
'X'
>>>
ubuntu@DESKTOP:/mnt/d/HGAME/cipher$ python3 solve.py
1069
b"\nSymmetry zn art is when t{e elements of \nr painting or drrwing balance eaph other \nout. T{is could be the3objects themselees, \nbut it can3also relate to polors and \nothea compositional gechniques.\nYou ~ay not realize zt, but your brazn \nis busy workzng behind the spenes to seek \noft symmetry when3you look at a printing. \nThere rre several reas|ns for this. Thv \nfirst is that3we're hard-wirew to look for \nig. Our ancient a}cestors may not3have had \na namv for it, but thvy knew that thezr \nown bodies wvre basically sy~metrical, as \nwvre those of potvntial predators3or prey. \nThereuore, this came zn handy whether3\nchoosing a matv, catching dinnvr or \navoiding qeing on the menf of a snarling,3\nhungry pack of3wolves or bears2\nTake a look at3your face in thv mirror \nand imrgine a line strright down the \n~iddle. You'll sve both sides of3your \nface are cretty symmetricrl. This is \nknodn as bilateral `ymmetry and it'` \nwhere both siwes either side |f this \ndividint line appear moae or less the srme.\nSo here is ghe flag: \nhgamehX0r_i5-a_uS3fU184nd$fUNny_C1pH3a}\n"
ubuntu@DESKTOP:/mnt/d/HGAME/cipher$ python3
Python 3.8.5 (default, Jul 28 2020, 12:59:40)
[GCC 9.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> ord('g') ^ ord('C') ^ ord('t')
80
>>> chr(80)
'P'
>>>
ubuntu@DESKTOP:/mnt/d/HGAME/cipher$ python3 solve.py
1069
b"\nSymmetry in art is when the elements of \na painting or drawing balance each other \nout. This could be the objects themselves, \nbut it can also relate to colors and \nother compositional techniques.\nYou may not realize it, but your brain \nis busy working behind the scenes to seek \nout symmetry when you look at a painting. \nThere are several reasons for this. The \nfirst is that we're hard-wired to look for \nit. Our ancient ancestors may not have had \na name for it, but they knew that their \nown bodies were basically symmetrical, as \nwere those of potential predators or prey. \nTherefore, this came in handy whether \nchoosing a mate, catching dinner or \navoiding being on the menu of a snarling, \nhungry pack of wolves or bears!\nTake a look at your face in the mirror \nand imagine a line straight down the \nmiddle. You'll see both sides of your \nface are pretty symmetrical. This is \nknown as bilateral symmetry and it's \nwhere both sides either side of this \ndividing line appear more or less the same.\nSo here is the flag: \nhgame{X0r_i5-a_uS3fU1+4nd$fUNny_C1pH3r}\n"
FAKE
第一次做 SMC
step 0：错误的做法
拖入ida
进入主函数
__int64 __usercall main@<rax>(char **a1@<rsi>, char **a2@<rdx>, __int64 a3@<rbp>)
{
__int64 v3; // rdx
__int64 v4; // rdx
__int64 v6; // [rsp-D8h] [rbp-D8h]
__int64 flag; // [rsp-48h] [rbp-48h]
signed int i; // [rsp-Ch] [rbp-Ch]
__int64 v9; // [rsp-8h] [rbp-8h]
__asm { endbr64 }
v9 = a3;
print("Give me your true flag:", a1, a2);
scan("%50s", &flag);
if ( length(&flag) != 36 )
{
print("Wrong length.", &flag, v3);
sub_401120();
}
for ( i = 0; i <= 35; ++i )
*((_DWORD *)&v9 + i - 52) = *((char *)&v9 + i - 64);// v9 - 64 = flag, flag往前偏移12个字节
if ( (unsigned int)sub_401216((__int64)&v6) == 1 )// 动态调试结果显示，v6就是输入的flag
print("Ohhhhhhhhhh!", &flag, v4);
else
print("Wrong flag. Keep looking!", &flag, v4);
return 0LL;
}
发现对于输入的flag，进行一个函数的判断
进入函数，发现一串如下的代码
v2 = -37 * *(_DWORD *)(*(v1 - 3) + 4)
+ -58 * *(_DWORD *)(*(v1 - 3) + 132)
+ 17 * *(_DWORD *)(*(v1 - 3) + 28)
+ 26 * *(_DWORD *)(*(v1 - 3) + 124)
+ -20 * *(_DWORD *)(*(v1 - 3) + 48)
+ -56 * *(_DWORD *)(*(v1 - 3) + 104)
+ 70 * *(_DWORD *)(*(v1 - 3) + 76)
+ 29 * *(_DWORD *)*(v1 - 3)
+ -42 * *(_DWORD *)(*(v1 - 3) + 68)
+ 67 * *(_DWORD *)(*(v1 - 3) + 140)
+ 11 * *(_DWORD *)(*(v1 - 3) + 24)
+ 66 * *(_DWORD *)(*(v1 - 3) + 60)
+ 53 * *(_DWORD *)(*(v1 - 3) + 44)
- 53 * *(_DWORD *)(*(v1 - 3) + 12)
+ 63 * *(_DWORD *)(*(v1 - 3) + 128)
- 65 * *(_DWORD *)(*(v1 - 3) + 84)
+ 9 * *(_DWORD *)(*(v1 - 3) + 36)
- 50 * *(_DWORD *)(*(v1 - 3) + 112)
- 48 * *(_DWORD *)(*(v1 - 3) + 32)
- 70 * *(_DWORD *)(*(v1 - 3) + 88)
+ 48 * *(_DWORD *)(*(v1 - 3) + 52);
if ( -35 * *(_DWORD *)(*(v1 - 3) + 8)
+ 89 * *(_DWORD *)(*(v1 - 3) + 96)
+ -49 * *(_DWORD *)(*(v1 - 3) + 64)
+ -19 * *(_DWORD *)(*(v1 - 3) + 16)
+ 88 * *(_DWORD *)(*(v1 - 3) + 100)
+ -7 * *(_DWORD *)(*(v1 - 3) + 120)
+ *(_DWORD *)(*(v1 - 3) + 108)
+ -33 * *(_DWORD *)(*(v1 - 3) + 80)
+ -23 * *(_DWORD *)(*(v1 - 3) + 92)
+ 90 * *(_DWORD *)(*(v1 - 3) + 56)
+ -99 * *(_DWORD *)(*(v1 - 3) + 40)
+ 30 * *(_DWORD *)(*(v1 - 3) + 116)
+ v2
- 68 * *(_DWORD *)(*(v1 - 3) + 136)
- 14 * *(_DWORD *)(*(v1 - 3) + 20)
- 67 * *(_DWORD *)(*(v1 - 3) + 72) != -874 )
goto LABEL_42;
用gdb调试看了一下，发现 *(v1 - 3) + 4 * i 就对应 input[i]
总共有36个方程，使用z3求解
from z3 import *
s = Solver()
f = [ Int('f%d' % i) for i in range(36) ]
for i in range(36):
s.add(f[i] > 0x20)
s.add(f[i] < 0x7f)
s.add(f[ 0] == ord('h'))
s.add(f[ 1] == ord('g'))
s.add(f[ 2] == ord('a'))
s.add(f[ 3] == ord('m'))
s.add(f[ 4] == ord('e'))
s.add(f[ 5] == ord('{'))
s.add(f[35] == ord('}'))
s.add(-37 * f[1] + -58 * f[33] + 17 * f[7] + 26 * f[31] + -20 * f[12] + -56 * f[26] + 70 * f[19] + 29 * f[0] + -42 * f[17] + 67 * f[35] + 11 * f[6] + 66 * f[15] + 53 * f[11] - 53 * f[3] + 63 * f[32] - 65 * f[21] + 9 * f[9] - 50 * f[28] - 48 * f[8] - 70 * f[22] + 48 * f[13] -35 * f[2] + 89 * f[24] + -49 * f[16] + -19 * f[4] + 88 * f[25] + -7 * f[30] + f[27] + -33 * f[20] + -23 * f[23] + 90 * f[14] + -99 * f[10] + 30 * f[29] - 68 * f[34] - 14 * f[5] - 67 * f[18] == -874)
s.add(64 * f[18] + -57 * f[15] + 90 * f[21] + 57 * f[4] + -63 * f[13] + 13 * f[2] + 10 * f[35] + -56 * f[8] + 56 * f[31] + -40 * f[0] + -91 * f[27] + 57 * f[23] + 62 * f[10] + 90 * f[9] + -92 * f[17] + -5 * f[29] + 60 * f[22] - 13 * f[12] + 5 * f[28] - 63 * f[32] + 5 * f[26] -41 * f[25] + -47 * f[16] + f[14] + 67 * f[34] + -20 * f[1] + 47 * f[33] + -79 * f[19] + -17 * f[6] + 30 * f[5] + 70 * f[3] + 41 * f[7] + 71 * f[24] + 15 * f[11] + 42 * f[20] == 21163)
s.add(28 * f[13] + 77 * f[19] + 2 * f[7] + -53 * f[10] + -61 * f[4] + 12 * f[17] + 93 * f[11] + -13 * f[32] + 53 * f[9] + 29 * f[16] + -77 * f[14] + 77 * f[33] + 74 * f[34] + -100 * f[30] - 99 * f[27] - 87 * f[25] + 36 * f[6] + 59 * f[3] + 81 * f[21] + 28 * f[28] + 7 * f[0] + 73 * f[26] + 50 * f[20] + 88 * f[35] + 49 * f[1] + 34 * f[23] + 58 * f[29] + 69 * f[24] + 54 * f[22] - 5 * f[31] - 41 * f[2] + 5 * f[18] - 93 * f[15] + 10 * f[12] - 27 * f[8] + 24 * f[5] == 45615)
s.add(-46 * f[20] + -61 * f[6] + -46 * f[19] + 51 * f[4] + -76 * f[34] + -17 * f[31] + 8 * f[28] + 94 * f[30] + 23 * f[8] + -61 * f[29] + -52 * f[35] + 81 * f[33] + -44 * f[1] + 75 * f[32] + -9 * f[24] - 96 * f[12] + 5 * f[26] + 2 * f[25] + 31 * f[22] + 43 * f[15] - 2 * f[0] - 17 * f[23] + 53 * f[21] + 51 * f[13] + 58 * f[17] + -52 * f[10] + -77 * f[7] + 86 * f[11] + -77 * f[16] + -100 * f[18] + -61 * f[2] - 92 * f[14] + 13 * f[5] - 99 * f[3] + 63 * f[27] + 8 * f[9] == -37017)
s.add(9 * f[16] + 59 * f[3] + -29 * f[14] + 32 * f[18] + -69 * f[26] + -81 * f[33] + -69 * f[9] + 60 * f[19] + -35 * f[21] + 40 * f[11] + -44 * f[7] + 78 * f[22] + 68 * f[28] + 70 * f[29] + 3 * f[2] + 61 * f[6] + 37 * f[35] - 36 * f[27] + 40 * f[34] + 23 * f[17] + 81 * f[12] - 25 * f[4] + 91 * f[0] + -43 * f[32] + 17 * f[13] + 9 * f[15] + f[1] * 64 + 69 * f[30] - 9 * f[23] - 75 * f[25] - 62 * f[20] + 56 * f[31] + 96 * f[5] + 69 * f[8] + 80 * f[10] + 99 * f[24] == 72092)
s.add(-79 * f[26] + -20 * f[8] + 90 * f[6] + 6 * f[30] + 47 * f[16] + 50 * f[20] + 51 * f[23] + -13 * f[33] + -86 * f[13] + 32 * f[31] + -89 * f[2] + 79 * f[11] + -41 * f[7] + -56 * f[14] + 54 * f[19] - 96 * f[34] - 34 * f[25] - 64 * f[4] - 36 * f[35] + 48 * f[10] - 39 * f[5] + 51 * f[32] + -63 * f[21] + 78 * f[24] + -76 * f[28] + 48 * f[18] + 93 * f[1] + 66 * f[29] + -86 * f[27] + -3 * f[0] + 20 * f[3] + 61 * f[17] - 56 * f[15] - 97 * f[22] + 96 * f[9] - 61 * f[12] == -27809)
s.add(-74 * f[28] + 76 * f[33] + 91 * f[5] + 83 * f[19] + 99 * f[32] + 98 * f[7] + 22 * f[34] + 83 * f[13] + -13 * f[0] + -66 * f[11] + -25 * f[2] + -9 * f[31] + 35 * f[25] + 31 * f[18] - 95 * f[21] + 37 * f[22] - 74 * f[16] + 17 * f[12] - 27 * f[24] + 11 * f[3] + 83 * f[9] + -44 * f[35] + -26 * f[30] + -36 * f[4] + 64 * f[6] + -65 * f[26] + -46 * f[8] + -33 * f[14] + -45 * f[1] + -32 * f[23] - 60 * f[27] + 77 * f[20] + 96 * f[15] - 23 * f[10] - 5 * f[29] - 73 * f[17] == 9604)
s.add(-57 * f[31] + 32 * f[25] + 55 * f[16] + 42 * f[24] + -93 * f[26] + 69 * f[17] + 84 * f[12] + 9 * f[23] + -34 * f[32] + -84 * f[2] + -18 * f[7] + 60 * f[29] - 99 * f[30] - f[0] + 24 * f[21] - 36 * f[4] + 9 * f[35] + 89 * f[15] + 72 * f[19] + 86 * f[13] - 8 * f[28] + -79 * f[10] + 82 * f[8] + -88 * f[3] + -26 * f[11] + 76 * f[1] + 69 * f[27] + -51 * f[14] + 78 * f[33] + -11 * f[18] + -83 * f[5] + 70 * f[20] + -36 * f[22] + 64 * f[6] + 19 * f[9] + 71 * f[34] == 25498)
s.add(-80 * f[15] + -54 * f[2] + 75 * f[6] + -31 * f[17] + 29 * f[12] + 28 * f[28] + 57 * f[14] + -68 * f[4] + 86 * f[0] + 82 * f[13] + -20 * f[11] + -18 * f[23] + 88 * f[18] + -57 * f[25] + 94 * f[9] - 51 * f[5] - 58 * f[7] - 2 * f[3] + 94 * f[31] - 6 * f[21] - 59 * f[19] + -70 * f[8] + 50 * f[30] + 26 * f[16] + 65 * f[32] + -62 * f[34] + 79 * f[10] + -82 * f[27] + -16 * f[29] + -60 * f[1] + 25 * f[20] - 66 * f[35] - 62 * f[24] + 89 * f[26] + 12 * f[22] - 86 * f[33] == -10472)
s.add(-91 * f[20] + -11 * f[17] + 38 * f[3] + 53 * f[35] + 31 * f[5] + -75 * f[22] + 14 * f[26] + -7 * f[24] + -7 * f[31] + 77 * f[23] + -46 * f[6] + 47 * f[19] + 48 * f[33] + 74 * f[ 1] - 24 * f[30] + 87 * f[9] + 33 * f[11] + 86 * f[28] + 37 * f[21] - 97 * f[27] - 30 * f[13] + 31 * f[14] + -11 * f[2] + 30 * f[10] + 72 * f[8] + 72 * f[29] + -49 * f[34] + 83 * f[18] + -63 * f[0] + -88 * f[4] - 59 * f[16] + 5 * f[7] - 3 * f[15] + 13 * f[12] - 73 * f[32] - 56 * f[25] == 6560)
s.add(-74 * f[20] + -97 * f[6] + 14 * f[15] + 77 * f[30] + -66 * f[28] + -89 * f[12] + -95 * f[13] + -70 * f[10] + -27 * f[1] + -85 * f[22] + -66 * f[34] + -91 * f[4] - 5 * f[19] - 94 * f[29] - 24 * f[35] - 7 * f[32] + 63 * f[5] - 49 * f[14] - 96 * f[18] - 100 * f[7] + 81 * f[16] + 59 * f[23] + -81 * f[8] + 49 * f[0] + -52 * f[3] + 84 * f[2] + 26 * f[25] + 70 * f[11] + 3 * f[21] + 28 * f[24] - 14 * f[9] + 59 * f[17] + 24 * f[31] - 25 * f[27] + 20 * f[33] - 77 * f[26] == -69431)
s.add(-69 * f[25] + 33 * f[20] + 55 * f[24] + 69 * f[18] + 83 * f[15] + -19 * f[13] + 22 * f[21] + f[16] + -53 * f[22] + -58 * f[4] + -63 * f[29] - 91 * f[26] + 28 * f[34] + 5 * f[3] + 35 * f[8] + 27 * f[ 1] - 31 * f[27] + 10 * f[12] + 84 * f[33] + 24 * f[14] + 42 * f[11] + 98 * f[28] + 2 * f[7] + 70 * f[19] + 53 * f[35] + 34 * f[6] + 30 * f[5] + 55 * f[23] + 69 * f[10] + 60 * f[2] - 2 * f[17] + 68 * f[32] + 21 * f[0] - f[9] + 60 * f[31] - 60 * f[30] == 54106)
s.add(15 * f[31] + -96 * f[21] + 38 * f[19] + -81 * f[9] + -68 * f[12] + 89 * f[20] + 33 * f[2] + 70 * f[34] + 79 * f[28] + -80 * f[35] + 76 * f[10] - 38 * f[5] + 5 * f[6] + 60 * f[11] - 8 * f[26] - 59 * f[23] + 9 * f[24] + 34 * f[17] - 60 * f[1] + 98 * f[25] + 48 * f[16] + -88 * f[22] + -96 * f[3] + f[18] * 64 + -61 * f[15] + -92 * f[13] + 50 * f[8] + 90 * f[29] + 32 * f[4] + -97 * f[27] + 14 * f[14] + f[30] + 97 * f[7] - 17 * f[32] - 96 * f[0] + 54 * f[33] == -8292)
s.add(-7 * f[3] + 49 * f[17] + 60 * f[25] + -45 * f[16] + -50 * f[0] + -98 * f[28] + -92 * f[12] + -22 * f[23] + 33 * f[13] + 57 * f[31] - 15 * f[5] + 36 * f[29] - 88 * f[15] + 12 * f[21] + 71 * f[14] - 48 * f[35] + 79 * f[34] - 5 * f[19] + 68 * f[33] - 2 * f[4] - 82 * f[10] + -58 * f[32] + 53 * f[8] + -57 * f[30] + -29 * f[24] + -28 * f[26] - 16 * f[18] - 98 * f[22] - f[27] * 64 + 32 * f[11] + 73 * f[2] - 38 * f[20] + 27 * f[9] - 7 * f[7] - 30 * f[ 1] - 35 * f[6] == -44677)
s.add(4 * f[31] + -43 * f[18] + -36 * f[29] + 60 * f[14] + 29 * f[20] + -85 * f[19] + 71 * f[27] + -22 * f[11] + 95 * f[9] + 19 * f[12] + -20 * f[30] + 6 * f[34] + 49 * f[6] + 13 * f[10] - 23 * f[13] + 17 * f[7] - 79 * f[22] + 12 * f[3] - 7 * f[4] - 12 * f[2] - 78 * f[17] + -86 * f[28] + -69 * f[33] + -31 * f[21] + 91 * f[15] + 91 * f[8] + 58 * f[16] + -91 * f[23] - 56 * f[5] + 59 * f[26] + 18 * f[32] - 87 * f[35] - 30 * f[24] + 54 * f[25] - 5 * f[ 1] - 94 * f[0] == -17772)
s.add(-17 * f[9] + -93 * f[12] + -85 * f[20] + -73 * f[35] + -87 * f[24] + -80 * f[25] + -87 * f[4] + 56 * f[27] + -89 * f[21] + 52 * f[15] + 97 * f[0] + -11 * f[19] + -94 * f[10] + -92 * f[29] + -20 * f[17] - 95 * f[5] - 13 * f[8] + 80 * f[31] - f[33] + 37 * f[30] + 64 * f[32] + -18 * f[18] + -76 * f[34] + 65 * f[3] + -78 * f[13] + -71 * f[26] + -44 * f[23] + 61 * f[7] + 63 * f[1] + 9 * f[16] + 11 * f[22] - 39 * f[14] + 80 * f[6] - 33 * f[11] - 62 * f[2] - 74 * f[28] == -77151)
s.add(54 * f[20] + 65 * f[22] + -9 * f[9] + -61 * f[24] + -45 * f[25] + 47 * f[4] + 31 * f[5] + 36 * f[23] + 20 * f[13] - 40 * f[2] - 64 * f[12] - 40 * f[14] + 81 * f[10] - 35 * f[0] - 12 * f[27] + 35 * f[30] + 63 * f[15] - 65 * f[19] + 31 * f[18] - 42 * f[35] + 33 * f[11] + 43 * f[33] + 76 * f[32] + -4 * f[26] + 59 * f[6] + -85 * f[34] + 69 * f[29] + 77 * f[31] + -95 * f[8] + 75 * f[16] - 19 * f[3] + 65 * f[21] - 78 * f[7] - 48 * f[28] - 77 * f[17] == 11531)
s.add(-12 * f[0] + 55 * f[17] + 35 * f[20] + 76 * f[13] + -73 * f[15] + 84 * f[12] + -72 * f[3] + 71 * f[24] + -41 * f[7] + 28 * f[8] + -93 * f[34] + -63 * f[30] + 35 * f[6] - 38 * f[10] - 4 * f[16] + 99 * f[11] + 10 * f[4] - 98 * f[35] - 9 * f[18] + 22 * f[21] - 6 * f[26] + 67 * f[23] + 95 * f[5] + -37 * f[9] + -71 * f[25] + 33 * f[32] + 96 * f[14] + 47 * f[31] + -92 * f[27] + -51 * f[1] + -25 * f[28] + 82 * f[2] - 6 * f[33] - 13 * f[29] + 25 * f[22] - 35 * f[19] == 4538)
s.add(79 * f[27] + 87 * f[24] + -52 * f[29] + -72 * f[13] + -17 * f[23] + 54 * f[0] + 45 * f[10] + -17 * f[33] + -49 * f[4] + -34 * f[17] + 87 * f[7] + -41 * f[18] + 2 * f[30] + -81 * f[11] + 37 * f[35] - 46 * f[9] + 25 * f[32] - 45 * f[14] - 30 * f[12] + 83 * f[19] + 24 * f[1] + 98 * f[16] + 64 * f[21] + 93 * f[8] + 78 * f[2] + 56 * f[15] + -51 * f[6] + -17 * f[26] + -50 * f[25] + -76 * f[3] + -65 * f[28] + -36 * f[31] + 88 * f[34] + 77 * f[20] - 62 * f[5] + 67 * f[22] == 33735)
s.add(37 * f[17] + -21 * f[19] + 55 * f[21] + -70 * f[26] + 92 * f[6] + 75 * f[31] + -35 * f[29] + -50 * f[25] + 8 * f[33] + -74 * f[13] + 34 * f[35] + 29 * f[24] + -10 * f[15] + -75 * f[16] + 24 * f[18] + 98 * f[0] + 41 * f[20] - 54 * f[28] - 5 * f[23] - 66 * f[9] + 3 * f[5] + 30 * f[1] + -29 * f[7] + -71 * f[30] + 61 * f[10] + -25 * f[4] + 82 * f[32] + 62 * f[22] + -40 * f[34] + 90 * f[3] + -36 * f[14] - 66 * f[2] + 15 * f[12] - 74 * f[27] + 31 * f[8] - 68 * f[11] == -7107)
s.add(-34 * f[13] + -13 * f[15] + -11 * f[19] + 28 * f[17] + 98 * f[9] + -69 * f[3] + 64 * f[25] + -66 * f[7] + -71 * f[6] + 75 * f[34] + 19 * f[32] + -94 * f[33] - 72 * f[18] + 35 * f[26] - 32 * f[27] + 76 * f[1] + 80 * f[28] + 66 * f[10] + 3 * f[12] - 99 * f[14] + 17 * f[30] + -79 * f[24] + -83 * f[29] + 55 * f[35] + -75 * f[8] + 77 * f[31] + 84 * f[22] - 94 * f[0] + 12 * f[2] + 61 * f[20] - 24 * f[23] + 62 * f[11] + 37 * f[16] - 65 * f[21] - 2 * f[4] - 90 * f[5] == -17028)
s.add(24 * f[3] + -76 * f[2] + -94 * f[16] + -37 * f[4] + -31 * f[7] + -65 * f[0] + -23 * f[22] + 80 * f[24] + -48 * f[20] + -42 * f[32] + 47 * f[9] - 95 * f[6] - 10 * f[35] - 30 * f[34] - 67 * f[12] + 81 * f[14] - 21 * f[27] + 65 * f[18] + 60 * f[25] + 31 * f[17] - 20 * f[31] + -17 * f[21] + -34 * f[26] + 64 * f[15] + 43 * f[11] + 39 * f[23] + 68 * f[33] + -58 * f[13] + 21 * f[1] + 19 * f[19] + 96 * f[8] - 32 * f[30] - 83 * f[28] + 20 * f[5] - 3 * f[29] + 7 * f[10] == -21641)
s.add(-76 * f[0] + -82 * f[22] + -92 * f[24] + 53 * f[20] + -90 * f[5] + 3 * f[34] + 93 * f[2] + 77 * f[25] + -40 * f[16] + -59 * f[26] + -91 * f[15] + 55 * f[9] + -84 * f[35] + -46 * f[12] + -41 * f[31] + -55 * f[8] + 97 * f[32] + 56 * f[19] - 15 * f[13] - 93 * f[4] + 37 * f[33] + -52 * f[7] + -82 * f[23] + 14 * f[27] + 52 * f[6] + 67 * f[11] + f[3] + -37 * f[30] - 88 * f[18] - 16 * f[10] + f[14] + 48 * f[17] - 80 * f[21] + 17 * f[29] - 94 * f[28] - 12 * f[ 1] == -71317)
s.add(-71 * f[21] + -55 * f[5] + -76 * f[4] + -94 * f[10] + -79 * f[26] + 95 * f[28] + 58 * f[3] + -85 * f[13] + -74 * f[27] + -35 * f[16] + 68 * f[2] + 84 * f[11] + -25 * f[23] + -91 * f[33] + -87 * f[14] + -65 * f[34] + 23 * f[20] + -91 * f[15] + 34 * f[12] + 53 * f[ 1] - 16 * f[24] + 46 * f[9] + -26 * f[0] + 42 * f[30] + 22 * f[25] + -89 * f[19] + 34 * f[32] + -12 * f[29] + -16 * f[7] + 22 * f[18] + -52 * f[31] + 83 * f[22] + 5 * f[17] - 71 * f[6] + 41 * f[35] + 68 * f[8] == -41387)
s.add(-97 * f[12] + -19 * f[19] + -87 * f[3] + 89 * f[27] + 54 * f[5] + 59 * f[22] + 95 * f[17] + 62 * f[26] + 6 * f[20] + 64 * f[14] + -50 * f[13] + -95 * f[30] + -68 * f[16] + 10 * f[0] - f[2] - f[28] + 17 * f[18] - 76 * f[6] - 24 * f[23] - 76 * f[11] + 33 * f[34] - 98 * f[31] + -59 * f[10] + 35 * f[4] + -53 * f[8] + -18 * f[1] + 9 * f[32] + -45 * f[9] - 60 * f[29] - 74 * f[35] + 31 * f[7] + 50 * f[24] + 25 * f[21] - 83 * f[33] + 25 * f[25] + 52 * f[15] == -30463)
s.add(-27 * f[25] + 84 * f[34] + -73 * f[14] + -54 * f[7] + -45 * f[26] + -97 * f[18] + 40 * f[10] + 73 * f[27] + -55 * f[11] + 52 * f[29] + -29 * f[13] + 32 * f[24] + -80 * f[0] + -79 * f[17] + -39 * f[6] + 88 * f[1] + 44 * f[2] - 50 * f[3] - 2 * f[22] - 44 * f[31] - 62 * f[8] + -68 * f[5] + 77 * f[21] + -34 * f[15] + -42 * f[35] + 30 * f[28] + -54 * f[30] + -53 * f[20] + 98 * f[33] + 70 * f[32] + 99 * f[19] - 51 * f[4] + 12 * f[16] - 55 * f[9] + 40 * f[12] + 76 * f[23] == -14435)
s.add(86 * f[20] + 70 * f[13] + -76 * f[19] + -31 * f[28] + 77 * f[14] + 48 * f[15] + -78 * f[31] + -82 * f[26] + 69 * f[3] + 70 * f[5] + 95 * f[6] - 60 * f[4] + 30 * f[27] + 3 * f[29] - 29 * f[32] + 5 * f[24] + 55 * f[0] + 36 * f[23] - 90 * f[22] + 37 * f[35] + 78 * f[34] + 20 * f[11] + -64 * f[1] + 74 * f[30] + 16 * f[16] + -83 * f[33] + 16 * f[2] + -17 * f[17] + -28 * f[8] + 9 * f[7] - 62 * f[10] + 46 * f[9] + 63 * f[21] - 39 * f[12] - 64 * f[18] - 27 * f[25] == 23472)
s.add(7 * f[0] + 92 * f[6] + -57 * f[24] + -89 * f[11] + -47 * f[5] + -39 * f[30] + 64 * f[8] + -63 * f[12] + -46 * f[9] + -82 * f[17] + 39 * f[23] + 58 * f[13] - 81 * f[1] + 33 * f[29] + 89 * f[7] - 14 * f[20] + 97 * f[33] + 10 * f[35] - 46 * f[14] + 81 * f[4] + 89 * f[15] + 97 * f[21] + -71 * f[2] + -7 * f[19] + -55 * f[3] + 85 * f[16] + -97 * f[34] + -29 * f[27] + -79 * f[32] + 50 * f[28] + 81 * f[22] - 44 * f[31] - 60 * f[10] - 20 * f[26] + 18 * f[18] + 91 * f[25] == 7913)
s.add(49 * f[17] + 52 * f[18] + -89 * f[25] + -93 * f[35] + -70 * f[11] + -45 * f[24] + 88 * f[30] + 92 * f[31] + 44 * f[26] + -5 * f[1] + -48 * f[6] + -16 * f[22] + 88 * f[32] + 91 * f[33] + 82 * f[28] + 98 * f[8] - 63 * f[13] - 8 * f[9] - f[16] - 4 * f[27] - 47 * f[4] + -41 * f[10] + 67 * f[29] + -22 * f[15] + -79 * f[12] + -18 * f[2] + 23 * f[20] + -20 * f[14] + 64 * f[19] + 91 * f[5] - 6 * f[7] + 84 * f[3] - 6 * f[34] + 69 * f[21] - 4 * f[23] - 80 * f[0] == 23824)
s.add(89 * f[11] + 61 * f[7] + -92 * f[31] + 99 * f[21] + 27 * f[16] + -48 * f[24] + -51 * f[4] + -39 * f[25] + 84 * f[30] + 34 * f[14] + -73 * f[17] + -92 * f[18] + 72 * f[2] - 14 * f[13] - f[19] + 2 * f[9] + 3 * f[29] - 61 * f[33] - 6 * f[26] - 57 * f[15] - 8 * f[27] + -28 * f[35] + -72 * f[6] + -46 * f[32] + 99 * f[20] + -69 * f[22] + -94 * f[12] + -35 * f[8] + -29 * f[0] - 29 * f[10] - 2 * f[23] - 23 * f[34] + 41 * f[3] + 42 * f[28] == -13865)
s.add(62 * f[25] + 85 * f[8] + -66 * f[32] + 43 * f[10] + 32 * f[33] + 75 * f[34] + 44 * f[1] + 49 * f[28] + -21 * f[26] + 60 * f[4] + -40 * f[0] + -98 * f[15] + -37 * f[9] + 78 * f[16] + 96 * f[35] - 84 * f[18] - 2 * f[7] + 43 * f[2] - 28 * f[6] - 77 * f[3] - 30 * f[17] + 90 * f[19] + 58 * f[30] + 74 * f[12] + 22 * f[29] + -29 * f[20] + -49 * f[22] + 88 * f[14] + -51 * f[24] + 44 * f[21] + 28 * f[13] - 95 * f[5] + 5 * f[23] + 85 * f[31] + 5 * f[27] + 47 * f[11] == 50179)
s.add(-100 * f[25] + -88 * f[18] + 46 * f[33] + 50 * f[31] + -85 * f[4] + -92 * f[6] + -54 * f[7] + 83 * f[23] + -25 * f[24] + -91 * f[5] + 85 * f[10] + -15 * f[16] - 59 * f[27] - 91 * f[8] + 73 * f[32] + 44 * f[19] + 5 * f[34] + 68 * f[14] - 32 * f[21] - 26 * f[30] - 56 * f[17] + 30 * f[1] + -92 * f[26] + 4 * f[29] + -89 * f[20] + 57 * f[15] + -66 * f[0] + -85 * f[12] + 91 * f[35] + -68 * f[2] - 95 * f[3] - 16 * f[13] - 76 * f[11] - 48 * f[9] - 88 * f[22] + 65 * f[28] == -75429)
s.add(-49 * f[20] + -71 * f[13] + -23 * f[23] + -19 * f[21] + 62 * f[2] + -41 * f[19] + 46 * f[15] + 5 * f[1] + -2 * f[5] + 88 * f[9] + 84 * f[16] + 77 * f[6] - 6 * f[26] + 51 * f[33] - 96 * f[31] + 59 * f[14] - 62 * f[8] - 55 * f[25] - 32 * f[34] + 69 * f[32] - 48 * f[28] + 85 * f[30] + -35 * f[24] + -58 * f[18] + 16 * f[12] + -45 * f[7] + 49 * f[35] + 8 * f[11] + 54 * f[22] + -33 * f[4] + 4 * f[17] - 21 * f[27] + 31 * f[0] - 98 * f[10] - 96 * f[29] - 71 * f[3] == -18764)
s.add(74 * f[20] + -50 * f[2] + -46 * f[21] + 28 * f[15] + -100 * f[5] + 53 * f[28] + -93 * f[9] + -69 * f[1] + -61 * f[0] + 26 * f[8] + -66 * f[6] + -66 * f[27] - 42 * f[4] + 89 * f[33] - 30 * f[31] - 45 * f[22] + 13 * f[14] - 29 * f[3] + 33 * f[10] + 54 * f[23] + 18 * f[30] + 88 * f[12] + 84 * f[34] + 66 * f[24] + 99 * f[16] + -78 * f[32] + -88 * f[11] + -21 * f[35] + 25 * f[18] + -81 * f[19] - 39 * f[29] + 15 * f[13] + 83 * f[26] - 28 * f[7] + 2 * f[25] == -20428)
s.add(-97 * f[22] + 14 * f[33] + -43 * f[11] + 40 * f[20] + 31 * f[13] + 44 * f[29] + -68 * f[3] + -36 * f[1] + -38 * f[9] + -7 * f[12] + f[26] + -50 * f[6] + 59 * f[8] + 88 * f[30] + 46 * f[0] - 34 * f[15] + 10 * f[4] + 84 * f[18] + 13 * f[7] + 14 * f[25] - 5 * f[16] + 10 * f[31] + 64 * f[28] + 97 * f[5] + -7 * f[27] + 62 * f[14] + 60 * f[24] + 27 * f[34] + -11 * f[10] - 31 * f[32] - 48 * f[19] - 55 * f[35] - 96 * f[2] - 83 * f[23] == 11973)
s.add(-99 * f[4] + -57 * f[8] + 2 * f[7] + 57 * f[24] + -54 * f[25] + 39 * f[29] + -91 * f[1] + -32 * f[20] + -30 * f[11] + 16 * f[12] + 45 * f[17] + 90 * f[32] + 26 * f[5] - 59 * f[28] + 7 * f[2] - 88 * f[3] + 36 * f[15] - 73 * f[6] - 6 * f[27] + 99 * f[13] - 96 * f[0] + -45 * f[26] + -10 * f[35] + -40 * f[9] + 97 * f[10] + 6 * f[22] + 58 * f[34] + 4 * f[31] + 55 * f[21] - 72 * f[16] + 27 * f[19] + 79 * f[23] - 28 * f[18] - 90 * f[30] - 6 * f[33] + 58 * f[14] == -23186)
if s.check() == sat:
model = s.model()
for i in range(36):
print (chr(model[f[i]].as_long().real), end='')
print ('\nfinish')
得到结果
hgame{@_FAKE_flag!_do_Y0u_know_SMC?}
提交一下发现不正确，说明这是一个假flag，提示我们这道题使用了SMC（self-modifying code）
step 1：找到SMC位置和加密方法
既然对某一个片段进行了加密，说明程序中肯定有一部分乱码（或者逻辑混乱的汇编代码）
在0x409080处找到一大段数字
交叉引用一下，定位到负责加密代码40699B
发现是一个简单异或，用刚才找到的一长串方程的那个函数与这段乱码进行逐位异或
step 2：破解SMC
接下来手动patch一下
在二进制文件中找到两段代码的位置，进行异或，上网找个二进制文件修改的代码
file_path = "FAKE"
fr = open(file_path, "rb")
fw = open('modify_'+file_path, "wb")
data = fr.read()
fw.write(data)
fw.seek(0x1216)
fw.write(b'\xf3\x0f\x1e\xfa\x55\x48\x89\xe5\x48\x81\xec\x60\x01\x00\x00\x48' )
fw.write(b'\x89\xbd\x28\xfe\xff\xff\x48\x8d\x95\x50\xff\xff\xff\xb8\x00\x00' )
fw.write(b'\x00\x00\xb9\x12\x00\x00\x00\x48\x89\xd7\xf3\x48\xab\xc7\x85\xc0' )
fw.write(b'\xfe\xff\xff\xf6\xd6\x00\x00\xc7\x85\xc4\xfe\xff\xff\xa7\xee\x00' )
fw.write(b'\x00\xc7\x85\xc8\xfe\xff\xff\xf7\xea\x00\x00\xc7\x85\xcc\xfe\xff' )
fw.write(b'\xff\x9f\xdf\x00\x00\xc7\x85\xd0\xfe\xff\xff\xcc\xdd\x00\x00\xc7' )
fw.write(b'\x85\xd4\xfe\xff\xff\xae\xd9\x00\x00\xc7\x85\xd8\xfe\xff\xff\x32' )
fw.write(b'\xb6\x00\x00\xc7\x85\xdc\xfe\xff\xff\xc3\xce\x00\x00\xc7\x85\xe0' )
fw.write(b'\xfe\xff\xff\x4c\xd1\x00\x00\xc7\x85\xe4\xfe\xff\xff\x05\xc5\x00' )
fw.write(b'\x00\xc7\x85\xe8\xfe\xff\xff\x8e\xc3\x00\x00\xc7\x85\xec\xfe\xff' )
fw.write(b'\xff\x9a\xac\x00\x00\xc7\x85\xf0\xfe\xff\xff\x6d\xaf\x00\x00\xc7' )
fw.write(b'\x85\xf4\xfe\xff\xff\x9a\xb5\x00\x00\xc7\x85\xf8\xfe\xff\xff\xc8' )
fw.write(b'\xb3\x00\x00\xc7\x85\xfc\xfe\xff\xff\x3b\xad\x00\x00\xc7\x85\x00' )
fw.write(b'\xff\xff\xff\x4a\xab\x00\x00\xc7\x85\x04\xff\xff\xff\x50\xad\x00' )
fw.write(b'\x00\xc7\x85\x08\xff\xff\xff\xce\xd6\x00\x00\xc7\x85\x0c\xff\xff' )
fw.write(b'\xff\xbc\xf1\x00\x00\xc7\x85\x10\xff\xff\xff\x12\xef\x00\x00\xc7' )
fw.write(b'\x85\x14\xff\xff\xff\x1b\xe3\x00\x00\xc7\x85\x18\xff\xff\xff\x82' )
fw.write(b'\xe1\x00\x00\xc7\x85\x1c\xff\xff\xff\xb4\xd6\x00\x00\xc7\x85\x20' )
fw.write(b'\xff\xff\xff\xd1\xbe\x00\x00\xc7\x85\x24\xff\xff\xff\x52\xc7\x00' )
fw.write(b'\x00\xc7\x85\x28\xff\xff\xff\xdd\xc1\x00\x00\xc7\x85\x2c\xff\xff' )
fw.write(b'\xff\x5b\xbc\x00\x00\xc7\x85\x30\xff\xff\xff\x20\xbb\x00\x00\xc7' )
fw.write(b'\x85\x34\xff\xff\xff\x87\xc6\x00\x00\xc7\x85\x38\xff\xff\xff\x04' )
fw.write(b'\xb6\x00\x00\xc7\x85\x3c\xff\xff\xff\x55\xc5\x00\x00\xc7\x85\x40' )
fw.write(b'\xff\xff\xff\x25\xbd\x00\x00\xc7\x85\x44\xff\xff\xff\x3f\xb4\x00' )
fw.write(b'\x00\xc7\x85\x48\xff\xff\xff\x16\xb4\x00\x00\xc7\x85\x4c\xff\xff' )
fw.write(b'\xff\x98\xb6\x00\x00\xc7\x85\x30\xfe\xff\xff\x68\x00\x00\x00\xc7' )
fw.write(b'\x85\x34\xfe\xff\xff\x67\x00\x00\x00\xc7\x85\x38\xfe\xff\xff\x61' )
fw.write(b'\x00\x00\x00\xc7\x85\x3c\xfe\xff\xff\x6d\x00\x00\x00\xc7\x85\x40' )
fw.write(b'\xfe\xff\xff\x65\x00\x00\x00\xc7\x85\x44\xfe\xff\xff\x7b\x00\x00' )
fw.write(b'\x00\xc7\x85\x48\xfe\xff\xff\x40\x00\x00\x00\xc7\x85\x4c\xfe\xff' )
fw.write(b'\xff\x5f\x00\x00\x00\xc7\x85\x50\xfe\xff\xff\x46\x00\x00\x00\xc7' )
fw.write(b'\x85\x54\xfe\xff\xff\x41\x00\x00\x00\xc7\x85\x58\xfe\xff\xff\x4b' )
fw.write(b'\x00\x00\x00\xc7\x85\x5c\xfe\xff\xff\x45\x00\x00\x00\xc7\x85\x60' )
fw.write(b'\xfe\xff\xff\x5f\x00\x00\x00\xc7\x85\x64\xfe\xff\xff\x66\x00\x00' )
fw.write(b'\x00\xc7\x85\x68\xfe\xff\xff\x6c\x00\x00\x00\xc7\x85\x6c\xfe\xff' )
fw.write(b'\xff\x61\x00\x00\x00\xc7\x85\x70\xfe\xff\xff\x67\x00\x00\x00\xc7' )
fw.write(b'\x85\x74\xfe\xff\xff\x21\x00\x00\x00\xc7\x85\x78\xfe\xff\xff\x2d' )
fw.write(b'\x00\x00\x00\xc7\x85\x7c\xfe\xff\xff\x64\x00\x00\x00\xc7\x85\x80' )
fw.write(b'\xfe\xff\xff\x6f\x00\x00\x00\xc7\x85\x84\xfe\xff\xff\x5f\x00\x00' )
fw.write(b'\x00\xc7\x85\x88\xfe\xff\xff\x59\x00\x00\x00\xc7\x85\x8c\xfe\xff' )
fw.write(b'\xff\x30\x00\x00\x00\xc7\x85\x90\xfe\xff\xff\x75\x00\x00\x00\xc7' )
fw.write(b'\x85\x94\xfe\xff\xff\x5f\x00\x00\x00\xc7\x85\x98\xfe\xff\xff\x6b' )
fw.write(b'\x00\x00\x00\xc7\x85\x9c\xfe\xff\xff\x6f\x00\x00\x00\xc7\x85\xa0' )
fw.write(b'\xfe\xff\xff\x6e\x00\x00\x00\xc7\x85\xa4\xfe\xff\xff\x77\x00\x00' )
fw.write(b'\x00\xc7\x85\xa8\xfe\xff\xff\x5f\x00\x00\x00\xc7\x85\xac\xfe\xff' )
fw.write(b'\xff\x53\x00\x00\x00\xc7\x85\xb0\xfe\xff\xff\x4d\x00\x00\x00\xc7' )
fw.write(b'\x85\xb4\xfe\xff\xff\x43\x00\x00\x00\xc7\x85\xb8\xfe\xff\xff\x3f' )
fw.write(b'\x00\x00\x00\xc7\x85\xbc\xfe\xff\xff\x7d\x00\x00\x00\xc7\x45\xfc' )
fw.write(b'\x01\x00\x00\x00\xc7\x45\xf8\x00\x00\x00\x00\xe9\xb9\x00\x00\x00' )
fw.write(b'\xc7\x45\xf4\x00\x00\x00\x00\xe9\x9f\x00\x00\x00\xc7\x45\xf0\x00' )
fw.write(b'\x00\x00\x00\xe9\x85\x00\x00\x00\x8b\x55\xf8\x89\xd0\x01\xc0\x01' )
fw.write(b'\xd0\x01\xc0\x89\xc2\x8b\x45\xf4\x01\xd0\x48\x98\x8b\xb4\x85\x50' )
fw.write(b'\xff\xff\xff\x8b\x55\xf8\x89\xd0\x01\xc0\x01\xd0\x01\xc0\x89\xc2' )
fw.write(b'\x8b\x45\xf0\x01\xd0\x48\x98\x48\x8d\x14\x85\x00\x00\x00\x00\x48' )
fw.write(b'\x8b\x85\x28\xfe\xff\xff\x48\x01\xd0\x8b\x00\x89\xc1\x8b\x55\xf0' )
fw.write(b'\x89\xd0\x01\xc0\x01\xd0\x01\xc0\x89\xc2\x8b\x45\xf4\x01\xd0\x48' )
fw.write(b'\x98\x8b\x84\x85\x30\xfe\xff\xff\x0f\xaf\xc8\x8b\x55\xf8\x89\xd0' )
fw.write(b'\x01\xc0\x01\xd0\x01\xc0\x89\xc2\x8b\x45\xf4\x01\xd0\x8d\x14\x0e' )
fw.write(b'\x48\x98\x89\x94\x85\x50\xff\xff\xff\x83\x45\xf0\x01\x83\x7d\xf0' )
fw.write(b'\x05\x0f\x8e\x71\xff\xff\xff\x83\x45\xf4\x01\x83\x7d\xf4\x05\x0f' )
fw.write(b'\x8e\x57\xff\xff\xff\x83\x45\xf8\x01\x83\x7d\xf8\x05\x0f\x8e\x3d' )
fw.write(b'\xff\xff\xff\xc7\x45\xec\x00\x00\x00\x00\xeb\x58\xc7\x45\xe8\x00' )
fw.write(b'\x00\x00\x00\xeb\x45\x8b\x55\xec\x89\xd0\x01\xc0\x01\xd0\x01\xc0' )
fw.write(b'\x89\xc2\x8b\x45\xe8\x01\xd0\x48\x98\x8b\x8c\x85\x50\xff\xff\xff' )
fw.write(b'\x8b\x55\xec\x89\xd0\x01\xc0\x01\xd0\x01\xc0\x89\xc2\x8b\x45\xe8' )
fw.write(b'\x01\xd0\x48\x98\x8b\x84\x85\xc0\xfe\xff\xff\x39\xc1\x74\x07\xc7' )
fw.write(b'\x45\xfc\x00\x00\x00\x00\x83\x45\xe8\x01\x83\x7d\xe8\x05\x7e\xb5' )
fw.write(b'\x83\x45\xec\x01\x83\x7d\xec\x05\x7e\xa2\x8b\x45\xfc\xc9\xc3\x45' )
fw.write(b'\xec\x38\xc3\xc0\x38\x8b\x00\x01')
fw.flush()
fw.close()
fr.close()
step 3：查看修改后的代码
使用ida64打开修改后的文件
__int64 __usercall sub_401216@<rax>(__int64 a1@<rbp>, __int64 a2@<rdi>)
{
v54 = a1;
*(&v54 - 59) = a2;
memset(&v47, 0, 0x90uLL);
v11 = 55030;
v12 = 61095;
v13 = 60151;
v14 = 57247;
v15 = 56780;
v16 = 55726;
v17 = 46642;
v18 = 52931;
v19 = 53580;
v20 = 50437;
v21 = 50062;
v22 = 44186;
v23 = 44909;
v24 = 46490;
v25 = 46024;
v26 = 44347;
v27 = 43850;
v28 = 44368;
v29 = 54990;
v30 = 61884;
v31 = 61202;
v32 = 58139;
v33 = 57730;
v34 = 54964;
v35 = 48849;
v36 = 51026;
v37 = 49629;
v38 = 48219;
v39 = 47904;
v40 = 50823;
v41 = 46596;
v42 = 50517;
v43 = 48421;
v44 = 46143;
v45 = 46102;
v46 = 46744;
*((_DWORD *)&v54 - 116) = 104;
*((_DWORD *)&v54 - 115) = 103;
*((_DWORD *)&v54 - 114) = 97;
*((_DWORD *)&v54 - 113) = 109;
*((_DWORD *)&v54 - 112) = 101;
*((_DWORD *)&v54 - 111) = 123;
*((_DWORD *)&v54 - 110) = 64;
*((_DWORD *)&v54 - 109) = 95;
*((_DWORD *)&v54 - 108) = 70;
*((_DWORD *)&v54 - 107) = 65;
*((_DWORD *)&v54 - 106) = 75;
*((_DWORD *)&v54 - 105) = 69;
*((_DWORD *)&v54 - 104) = 95;
*((_DWORD *)&v54 - 103) = 102;
*((_DWORD *)&v54 - 102) = 108;
*((_DWORD *)&v54 - 101) = 97;
*((_DWORD *)&v54 - 100) = 103;
*((_DWORD *)&v54 - 99) = 33;
*((_DWORD *)&v54 - 98) = 45;
*((_DWORD *)&v54 - 97) = 100;
*((_DWORD *)&v54 - 96) = 111;
*((_DWORD *)&v54 - 95) = 95;
*((_DWORD *)&v54 - 94) = 89;
*((_DWORD *)&v54 - 93) = 48;
*((_DWORD *)&v54 - 92) = 117;
*((_DWORD *)&v54 - 91) = 95;
*((_DWORD *)&v54 - 90) = 107;
*((_DWORD *)&v54 - 89) = 111;
v3 = 110;
v4 = 119;
v5 = 95;
v6 = 83;
v7 = 77;
v8 = 67;
v9 = 63;
v10 = 125;
v53 = 1;
for ( i = 0; i <= 5; ++i )
{
for ( j = 0; j <= 5; ++j )
{
for ( k = 0; k <= 5; ++k )
*((_DWORD *)&v54 + 6 * i + j - 44) += *((_DWORD *)&v54 + 6 * k + j - 116)
* *(_DWORD *)(4LL * (6 * i + k) + *(&v54 - 59));// 矩阵乘法
}
}
for ( l = 0; l <= 5; ++l )
{
for ( m = 0; m <= 5; ++m )
{
if ( *((_DWORD *)&v54 + 6 * l + m - 44) != *((_DWORD *)&v54 + 6 * l + m - 80) )// 与v11到v46比较
v53 = 0;
}
}
return v53;
}
发现判断函数发生了变化
第一个三重循环明显是一个矩阵乘法，第二个则是简单比较，由于这里指针有点绕，使用了gdb对每一项进行了判断
首先在第二个循环打断点
.text:00000000004015FB loc_4015FB: ; CODE XREF: sub_401216+42E↓j
.text:00000000004015FB mov edx, [rbp-14h]
.text:00000000004015FE mov eax, edx
.text:0000000000401600 add eax, eax
.text:0000000000401602 add eax, edx
.text:0000000000401604 add eax, eax
.text:0000000000401606 mov edx, eax
.text:0000000000401608 mov eax, [rbp-18h]
.text:000000000040160B add eax, edx
.text:000000000040160D cdqe
.text:000000000040160F mov ecx, [rbp+rax*4-0B0h]
.text:0000000000401616 mov edx, [rbp-14h]
.text:0000000000401619 mov eax, edx
.text:000000000040161B add eax, eax
.text:000000000040161D add eax, edx
.text:000000000040161F add eax, eax
.text:0000000000401621 mov edx, eax
.text:0000000000401623 mov eax, [rbp-18h]
.text:0000000000401626 add eax, edx
.text:0000000000401628 cdqe
.text:000000000040162A mov eax, [rbp+rax*4-140h]
.text:0000000000401631 cmp ecx, eax
.text:0000000000401633 jz short loc_40163C
.text:0000000000401635 mov dword ptr [rbp-4], 0
在cmp命令处打断点，查看ecx和eax寄存器的值，发现是拿计算结果和v11-v46进行比较
随后查看第一个大循环，关键点显然是乘法
.text:000000000040159E imul ecx, eax
打上断点后，发现是拿输入的6*6矩阵和104-125这段由36个数字构成的矩阵进行乘法
step 4：进行求解
所以接下来只需要求解矩阵即可，这里还是使用了z3
from z3 import *
s = Solver()
f = [ Int('f%d' % i) for i in range(36) ]
for i in range(36):
s.add(f[i] > 0x20)
s.add(f[i] < 0x7f)
s.add(f[ 0] == ord('h'))
s.add(f[ 1] == ord('g'))
s.add(f[ 2] == ord('a'))
s.add(f[ 3] == ord('m'))
s.add(f[ 4] == ord('e'))
s.add(f[ 5] == ord('{'))
s.add(f[35] == ord('}'))
a = [104, 103, 97, 109, 101, 123, 64, 95, 70, 65, 75, 69, 95, 102, 108, 97, 103, 33, 45, 100, 111, 95, 89, 48, 117, 95, 107, 111, 110, 119, 95, 83, 77, 67, 63, 125]
for c in a:
print(chr(c), end='')
print()
ans = [55030, 61095, 60151, 57247, 56780, 55726, 46642, 52931, 53580, 50437, 50062, 44186, 44909, 46490, 46024, 44347, 43850, 44368, 54990, 61884, 61202, 58139, 57730, 54964, 48849, 51026, 49629, 48219, 47904, 50823, 46596, 50517, 48421, 46143, 46102, 46744]
for i in range(6):
for j in range(6):
s.add(f[6 * i] * a[j] + f[6 * i + 1] * a[6 + j] + f[6 * i + 2] * a[12 + j] + f[6 * i + 3] * a[18 + j] + f[6 * i + 4] * a[24 + j] + f[6 * i + 5] * a[30 + j] == ans[6 * i + j])
if s.check() == sat:
model = s.model()
for i in range(36):
print (chr(model[f[i]].as_long().real), end='')
print('\nfinish')
# hgame{E@sy_Se1f-Modifying_C0oodee33}