第一周笔记
一.SMC:
1.什么是SMC
-
SMC(Software-Based Memory Encryption)是一种局部代码加密技术,它可以将一个可执行文件的指定区段进行加密,使得黑客无法直接分析区段内的代码,从而增加恶意代码分析难度和降低恶意攻击成功的可能性。
SMC的基本原理是在编译可执行文件时,将需要加密的代码区段(例如函数、代码块等)单独编译成一个section(段),并将其标记为可读、可写、不可执行(readable, writable, non-executable),然后通过某种方式在程序运行时将这个section解密为可执行代码,并将其标记为可读、可执行、不可写(readable, executable, non-writable)。这样,攻击者就无法在内存中找到加密的代码,从而无法直接执行或修改加密的代码。
-
在执行某一段代码时,程序会对自身的该段代码进行自修改,只有在修改后的代码才是可汇编、可执行的。
-
在程序未对该段代码进行修改之前, 在静态分析状态下, 均是不可读的字节码,IDA之类的反汇编器无法识别程序的正常逻辑
-
如何实现先不说,先解决如何解决SMC问题,得到原来的代码
2.SMC如何逆向分析
1.SMC的特征
- 先异或再进行函数的调用
- 在Linux系统中,可以通过mprotect函数修改目标内存的权限
- 在Windows系统中,VirtualProtect函数实现内存权限的修改
2.SMC的破解方法
- 找到对代码或数据加密的函数后通过idapython写解密脚本
- 动态调试到SMC解密结束的地方dump出来
3.SMC题目复现(wp)
1.[网鼎杯 2020 青龙组]jocker
附上题目链接:网鼎杯 2020 青龙组]jocker | NSSCTF
第一步仍然是查壳,无壳,32位,丢进ida32中
然后发现调用了VirtualProtect(encrypt, 0xC8u, 4u, &flOldProtect),对内存权限进行了修改,猜测是SMC
简单看一下逻辑,v7应该就是我们的输入,后面检查输入字符长度,说明flag应该是24位的,然后再进行wrong()和omg()
点开encrypt,发现报错
再看看wrong和omg函数
此处明显是把&unk_4030C0的值赋给v2,然后a1的值要等于v2,a1的值再wrong里面进行一些很简单的操作,先找到v2的值,然后可以写出逆向脚本,因为是int数组,所以是四位四位取
与运算,其实就是i是奇数则(i&1)=1,为偶数(i&1)=0,奇数位就加回来,偶数位就异或.
得到的是fakeflag,再看下面的encrypt
这里用到动态调试破解SMC,在自加密结束后下一个断点,注意输入的长度应该为24位,输入123456789123456789123456
直接反汇编窗口下断点好像断不下来,于是在汇编里面下断点
这次成功断下来了,然后F7进入encrypt函数,先按U取消函数定义,然后选中所有的数据,按c转换为代码
这里选择force,然后回到开始按P,定义为函数,F5成功得到函数(这里其实有两个函数)
第一个函数里面就是个简单的异或
key = 'hahahaha_do_you_find_me?'
v2 = [0x0E, 0x0D, 0x9, 0x6, 0x13, 0x5, 0x58, 0x56, 0x3E, 0x6,0x0C, 0x3C, 0x1F, 0x57, 0x14, 0x6B, 0x57, 0x59, 0x0D]
flag = ""
for i in range(19):
flag+=(chr(v2[i] ^ ord(key[i])))
print(flag)
#flag{d07abccf8a410c
只有一半flag,于是找了下,进行相同操作后发现第二个函数
先将%tp&:赋值给v3,v4是个伪随机数,v1不知道干嘛的不管他,后面一堆也看不懂是什么意思,然后继续猜呗,应该就是对v3五个数进行操作,最后一位的结果应该是 },就猜是异或,于是得到flag
key = 'hahahaha_do_you_find_me?'
v2 = [0x0E, 0x0D, 0x9, 0x6, 0x13, 0x5, 0x58, 0x56, 0x3E, 0x6,0x0C, 0x3C, 0x1F, 0x57, 0x14, 0x6B, 0x57, 0x59, 0x0D]
flag = ""
for i in range(19):
flag+=(chr(v2[i] ^ ord(key[i])))
b=['%','t','p','&',':']
key2= ord('}')^ord(':')
for i in range(5):
flag+=chr(ord(b[i])^key2)
print(flag)
#flag{d07abccf8a410cb37a}
下面再来说第二种静态方法:使用ida python脚本过SMC
还是按U取消定义,然后往下,在这个地方按D,第二个函数也是一样的
然后运行ida python脚本
import idc
addr = 0x401500 # encrypt函数的地址
for i in range(187):
b = get_bytes(addr + i, 1)
idc.patch_byte(addr + i, ord(b) ^ 0x41)
就可以得到解密后的函数,然后就和第一种方法一样的
二.动态调试
1.断点类型
- 硬件断点
- 软件断点
2.题目复现
1.[HUBUCTF 2022 新生赛]help
题目链接:[HUBUCTF 2022 新生赛]help | NSSCTF
64位无壳,拖入ida64找到main函数
题目已经提示是迷宫题了,if里面检测了输入的长度,说明解迷宫步数应该是54,有个createmap函数,点进去看
是用num数组里面的数进行操作然后得到map的值,现在map里面什么都没有
于是在函数的结尾下一个断点,通过动态调试得到map
随便输入几个数都行,因为判断长度的逻辑是在createmap后
F7步入函数后,按F9运行到断点
此时的map已经成功被找到,shift+e直接提取,注意地图应该是16x16的,而且根据得到的提示,flag应该是得到的答案的md5值
[1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
[1, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 1, 1, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 0, 1, 1, 0, 0, 0, 1, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 0, 0, 0, 0, 1, 0, 1, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 1, 1, 1, 0, 1, 0, 1, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 1, 1, 1, 0, 0, 0, 1, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 0, 1, 1, 1]
[1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 0, 0, 0, 1]
[1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 1, 0, 1, 0, 1]
[1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 1, 0, 1, 0, 1]
[1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 1, 1, 0, 1, 0, 0]
[1, 0, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 1]
[1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
wwdddwwwaaawwwwwwwwwddddssssdddssdsssssssdddwwwwddsssd
#NSSCTF{a8622109e2fb1296e06d5eed6f78f954}
2.[CISCN 2022 东北]easycpp
题目链接:[CISCN 2022 东北]easycpp | NSSCTF
64位,无壳,丢到ida64里面,main函数一堆看不懂的,于是准备动态调试寻找函数逻辑
在最开始的地方下断点,第一个sub_140002410函数应该是printf的功能,下面那个猜应该是scanf的功能,开始调试
果然在这里断下来了并且要求输入,为了方便看直接改名字scanf,并且将输入传入了函数的那个参数中,size应该是输入字符的长度
于是输入38个a继续看,发现Src这个参数就是我们的输入
后面又是一堆乱七八糟的,看不太懂继续跑,if里面的判断其实就是干扰,动调发现里面的东西都会运行
先是将V6,V7,V8,V9,V10,V11的值变成我们的输入,后面的关键逻辑就很好看了
*((_BYTE *)v7 + v5) ^= *((_BYTE *)v6 + v5 + 1)
//input[i]^=input[i+1] 这里v5其实就是一个索引的作用
*((_BYTE *)v9 + v5 + 1) ^= *((_BYTE *)v8 + v5 + 2);
//input[i+1]^=input[i+2]
*((_BYTE *)v11 + v5 + 2) ^= *((_BYTE *)v10 + v5 + 3);
//input[i+2]^=input[i+3]
知道了加密逻辑,下一步就应该找到加密后的结果,继续动态调试
看到有个buf2,后面又有cmp,感觉不用继续动态调试了,已经能猜出来了,buf2里面应该就是我们最后比较的值,提取出来
最后写出加密脚本:
a=[0x0A, 0x0B, 0x7D, 0x2F, 0x7F, 0x67, 0x65, 0x30, 0x63, 0x60,
0x37, 0x3F, 0x3C, 0x3F, 0x33, 0x3A, 0x3C, 0x3B, 0x35, 0x3C,
0x3E, 0x6C, 0x64, 0x31, 0x64, 0x6C, 0x3B, 0x68, 0x61, 0x62,
0x65, 0x36, 0x33, 0x60, 0x62, 0x36, 0x1C, 0x7D]
for i in range(len(a)-4,-1,-1):
a[i+2]=a[i+2]^a[i+3]
a[i+1]=a[i+1]^a[i+2]
a[i]=a[i]^a[i+1]
for i in range(38):
print(chr(a[i]),end="")
#flag{37c1b0258164803691d1d193b00ec56a}
题外话:range的用法,这样就不用去手动改数组
range其实并不是一个函数,而是一个迭代器,range里面有三个参数:range(a1,a2,a3)
第一个参数表示start,就是迭代范围的开始
第二个参数表示stop,就是迭代范围的结束
其中表示范围的规则是前闭后开(取不到stop)
第三个参数表示step,就是迭代的增量或者减量(负数表示减)
3.[LitCTF 2023]程序和人有一个能跑就行了
题目链接:[LitCTF 2023]程序和人有一个能跑就行了 | NSSCTF
32位,无壳,丢进ida32中,函数名一堆看不懂,用动态调试寻找函数逻辑
sub_472810(&dword_47DD80, Buf2)感觉像是输入函数
这个明显就是比较函数了,所以感觉sub_4015A0(Buf2, strlen(Buf2), Destination, 6)像是关键的加密函数,在这个函数的入口下断点
buf2里面明显是我们的输入,可以改改函数名和变量名方便看,步入加密函数看看
看到关键的256,联想到RC4,后面v15是初始化s盒,v16是我们key(就是litctf)
RC4是对称加密,于是继续运行到比较阶段,把密文dump下来,然后拿到cyberchef看
得到的是假的flag,继续往后走,这里又对buf1进行了一次赋值,继续dump下来解密
这次成功得到了flag
4.[GDOUCTF 2023]Tea
题目链接:[GDOUCTF 2023]Tea | NSSCTF
一道魔改XTEA+动态调试寻找函数逻辑题
64位无壳,丢入ida64,先找字符串然后通过交叉引用定位关键代码,还是需要用动态调试来寻找函数作用
经过调试可以改名一些函数,并且找到关键的三个函数
第一个函数貌似是给V7重新赋值
第二个函数就是把我们的输入复制到V9里面去
第三个函数就是很明显的加密函数了,这是个tea加密,我们需要找到三个值,Δ,key和加密后的密文,传进去的第一个参数就是我们的输入,就是等待加密的密文,第二个参数是V7,它的值就应该是我们的密钥了。然后根据逻辑Δ就是256256256
接下来应该找加密后比较的密文了,在这个函数里面可以找到,然后就可以开始写脚本了,为了锻炼自己我决定手搓一个XTEA解密
#include <stdio.h>
int main()
{
int key[] = {2233, 4455, 6677, 8899};
unsigned int value[10];
value[0] = 0x1A800BDA;
value[1] = 0xF7A6219B;
value[2] = 0x491811D8;
value[3] = 0xF2013328;
value[4] = 0x156C365B;
value[5] = 0x3C6EAAD8;
value[6] = 0x84D4BF28;
value[7] = 0xF11A7EE7;
value[8] = 0x3313B252;
value[9] = 0xDD9FE279;
int dalte = 0xF462900;
int i = 0;
int count;
int sum = 0;
for(i=8;i>=0;i--){
count=33;
sum = dalte * (i+count);
while(count!=0){
sum=sum-dalte;
value[i+1] -= (sum+key[(sum>>11)&3])^(value[i]+((value[i]>>5)^(16*value[i])));
value[i]-=sum^(value[i+1]+((value[i+1]>>5)^(16*value[i+1]))^(sum+key[sum&3]));
count--;
}
}
for(i=0;i<=9;i++){
printf("%x", value[i]);
}
return 0;
}
三.花指令
1.什么是花指令
企图隐藏掉不想被逆向工程的代码块(或其它功能)的一种方法,在真实代码中插入一些垃圾代码的同时还保证原有程序的正确执行,而程序无法很好地反编译, 难以理解程序内容,达到混淆视听的效果。简单的说就是在代码中混入一些垃圾数据阻碍你的静态分析。
可执行花指令:
这部分花指令代码在程序的正常执行过程中会被执行,但执行这些代码没有任何意义,执行前后不改变任何寄存器的值(当然eip这种除外),同时这部分代码也会被反汇编器正常识别。
不可执行式花指令:
花指令虽然被插入到了正常代码的中间,但是并不意味着它一定会得到执行,这类花指令通常形式为在代码中出现了类似数据的代码,或者IDA反汇编后为jmupout(xxxxx)。
这类花指令一般不属于CPU可以识别的操作码,那么就需要在上面用跳转跳过这些花指令才能保证程序的正常运行。
实现:
1、简单的花指令
简单的花指令 0xe8是跳转指令,可以对线性扫描算法进行干扰,但是递归扫描算法可以正常分析。
![img](file:///C:\Users\cpqyyds\AppData\Local\Temp\ksohtml2688\wps1.jpg)
两个跳转一个指向无效数据,一个指向正常数据来干扰递归扫描算法。
![img](file:///C:\Users\cpqyyds\AppData\Local\Temp\ksohtml2688\wps2.jpg)
2、简单的jmp
OD能被骗过去,但是因为ida采用的是递归扫描的办法所以能够正常识别。
![img](file:///C:\Users\cpqyyds\AppData\Local\Temp\ksohtml2688\wps3.jpg)![img](file:///C:\Users\cpqyyds\AppData\Local\Temp\ksohtml2688\wps4.jpg)
3、多级跳转
本质上和简单跳转是一样的,只是加了几层跳转。显然无法干扰ida
![img](file:///C:\Users\cpqyyds\AppData\Local\Temp\ksohtml2688\wps5.jpg)
4、call&ret构造花指令
__asm{
call label1
_emit junkcode
label1:
add dword ptr ss:[esp],8//具体增加多少根据调试来
ret
_emit junkcode
}
call指令:将下一条指令地址压入栈,再跳转执行
ret指令:将保存的地址取出,跳转执行
![img](file:///C:\Users\cpqyyds\AppData\Local\Temp\ksohtml2688\wps6.jpg)
2.如何清除花指令
1.手动清除:
找到所有的花指令,重新设置数据和代码地址。或者将花指令设置为nop(0x90)
![img](file:///C:\Users\cpqyyds\AppData\Local\Temp\ksohtml2688\wps7.jpg)
在0x401051设置为数据类型(快捷键D),在0x401052设置为代码类型(快捷键C)
![img](file:///C:\Users\cpqyyds\AppData\Local\Temp\ksohtml2688\wps8.jpg)
2.python脚本去花
网上可以自己找脚本,不说了
3.题目复现
1.[MoeCTF 2022]chicken_soup
题目链接:[MoeCTF 2022]chicken_soup | NSSCTF
32位无壳,丢入ida
判断输入长度为38后的两个函数应该是关键函数,点开一片红
按D,然后将花指令nop掉,然后按C还原为代码
得到第一个函数,第二个同类(要按p识别为函数)
最后写出解密脚本
a=[0xCD, 0x4D, 0x8C, 0x7D, 0xAD, 0x1E, 0xBE, 0x4A, 0x8A, 0x7D,
0xBC, 0x7C, 0xFC, 0x2E, 0x2A, 0x79, 0x9D, 0x6A, 0x1A, 0xCC,
0x3D, 0x4A, 0xF8, 0x3C, 0x79, 0x69, 0x39, 0xD9, 0xDD, 0x9D,
0xA9, 0x69, 0x4C, 0x8C, 0xDD, 0x59, 0xE9, 0xD7]
for i in range(len(a)):
a[i]=(a[i]>>4)|(a[i]<<4)& 0xff
for i in range(len(a)-2,-1,-1):
a[i]=a[i]-a[i+1]
for i in a:
print(chr(i),end="")
#moectf{p4tch_pr0gr4m_t0_d3c0mpi1e_it!}
四.Z3求解器在CTF中的简单使用
Z3是一个微软研究院开源的theorem prover(定理证明器),支持位向量、布尔、数组、浮点数、字符串以及其他数据类型。Z3是一个SMT solver以及支持SMTLIB的格式。
1.用法
z3中有3种类型的变量,分别是整型(Int),实型(Real)*和*向量(BitVec)
Int-整数型
from z3 import *
a = Int('a')#声明单个整型变量
a,b = Ints('a b')#声明多个整型变量
Real-实数型
from z3 import *
a = Real('a')#声明单个实型变量
a,b = Reals('a b')#声明多个实型变量
BitVec-向量
from z3 import *
a = BitVec('a',8) #声明单个8位的变量
a, b = BitVec('a b',8)#声明多个8位的变量
约束求解器
一般来说遇到的约束条件肯定不止一个,这个时候需要先创建一个求解器对象(Solver()),然后通过s.add(约束条件)添加约束条件
然后可以通过s.check()判断是否有解,它将返回sat
或unsat
作为结果,如果有解就是sat,然后可以通过s.model()来输出解
2.简单的应用:
1.[GDOUCTF 2023]Check_Your_Luck
题目链接:[GDOUCTF 2023]Check_Your_Luck | NSSCTF
给的cpp文件,直接打开:
#include <iostream>
using namespace std;
void flag_checker(int v, int w,int x,int y,int z);
int main(){
int v,w,x,y,z;
cout << "Input 5 random number and check your luck ;)" << endl;
cout << "Num1: ";
cin >> v;
cout << "Num2: ";
cin >> w;
cout << "Num3: ";
cin >> x;
cout << "Num4: ";
cin >> y;
cout << "Num5: ";
cin >> z;
cout << endl;
flag_checker(v,w,x,y,z);
}
void flag_checker(int v,int w, int x, int y, int z){
if ((v * 23 + w * -32 + x * 98 + y * 55 + z * 90 == 333322) &&
(v * 123 + w * -322 + x * 68 + y * 67 + z * 32 == 707724) &&
(v * 266 + w * -34 + x * 43 + y * 8 + z * 32 == 1272529) &&
(v * 343 + w * -352 + x * 58 + y * 65 + z * 5 == 1672457) &&
(v * 231 + w * -321 + x * 938 + y * 555 + z * 970 == 3372367)){
cout << "Congratulations, Here is your flag:\n";
cout << "flag{" << v << "_" << w << "_" << x << "_" << y << "_" << z << "}" << endl;
}
else{
cout << "\nSeems your luck is not in favor right now!\nBetter luck next time!" << endl;
}
}
很明显的约束求解,用Z3约束求解器来做这道题,很容易写出脚本
from z3 import *
s=Solver()
v,w,x,y,z=Ints('v w x y z')
s.add(v * 23 + w * -32 + x * 98 + y * 55 + z * 90 == 333322)
s.add(v * 123 + w * -322 + x * 68 + y * 67 + z * 32 == 707724)
s.add(v * 266 + w * -34 + x * 43 + y * 8 + z * 32 == 1272529)
s.add(v * 343 + w * -352 + x * 58 + y * 65 + z * 5 == 1672457)
s.add(v * 231 + w * -321 + x * 938 + y * 555 + z * 970 == 3372367)
if s.check()==sat:
print(s.model())
得到的就是flag,记得注意顺序
flag{4544_123_677_1754_777}
2.[HNCTF 2022 WEEK2]来解个方程?
题目链接:[HNCTF 2022 WEEK2]来解个方程? | NSSCTF
很简单的逻辑就是求解
直接写脚本
from z3 import *
s = Solver()
v2, v3, v4, v5, v6, v7, v8, v9, v10, v11, v12, v13, v14, v15, v16, v17, v18, v19, v20, v21, v22, v23 = Ints(
"v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23")
s.add(245 * v6 + 395 * v5 + 3541 * v4 + 2051 * v3 + 3201 * v2 + 1345 * v7 == 855009)
s.add(3270 * v6 + 3759 * v5 + 3900 * v4 + 3963 * v3 + 1546 * v2 + 3082 * v7 == 1515490)
s.add(526 * v6 + 2283 * v5 + 3349 * v4 + 2458 * v3 + 2012 * v2 + 268 * v7 == 854822)
s.add(3208 * v6 + 2021 * v5 + 3146 * v4 + 1571 * v3 + 2569 * v2 + 1395 * v7 == 1094422)
s.add(3136 * v6 + 3553 * v5 + 2997 * v4 + 1824 * v3 + 1575 * v2 + 1599 * v7 == 1136398)
s.add(2300 * v6 + 1349 * v5 + 86 * v4 + 3672 * v3 + 2908 * v2 + 1681 * v7 == 939991)
s.add(212 * v22 + 153 * v21 + 342 * v20 + 490 * v12 + 325 * v11 + 485 * v10 + 56 * v9 + 202 * v8 + 191 * v23 == 245940)
s.add(348 * v22 + 185 * v21 + 134 * v20 + 153 * v12 + 460 * v9 + 207 * v8 + 22 * v10 + 24 * v11 + 22 * v23 == 146392)
s.add(177 * v22 + 231 * v21 + 489 * v20 + 339 * v12 + 433 * v11 + 311 * v10 + 164 * v9 + 154 * v8 + 100 * v23 == 239438)
s.add(68 * v20 + 466 * v12 + 470 * v11 + 22 * v10 + 270 * v9 + 360 * v8 + 337 * v21 + 257 * v22 + 82 * v23 == 233887)
s.add(246 * v22 + 235 * v21 + 468 * v20 + 91 * v12 + 151 * v11 + 197 * v8 + 92 * v9 + 73 * v10 + 54 * v23 == 152663)
s.add(241 * v22 + 377 * v21 + 131 * v20 + 243 * v12 + 233 * v11 + 55 * v10 + 376 * v9 + 242 * v8 + 343 * v23 == 228375)
s.add(356 * v22 + 200 * v21 + 136 * v11 + 301 * v10 + 284 * v9 + 364 * v8 + 458 * v12 + 5 * v20 + 61 * v23 == 211183)
s.add(154 * v22 + 55 * v21 + 406 * v20 + 107 * v12 + 80 * v10 + 66 * v8 + 71 * v9 + 17 * v11 + 71 * v23 == 96788)
s.add(335 * v22 + 201 * v21 + 197 * v11 + 280 * v10 + 409 * v9 + 56 * v8 + 494 * v12 + 63 * v20 + 99 * v23 == 204625)
s.add(428 * v18 + 1266 * v17 + 1326 * v16 + 1967 * v15 + 3001 * v14 + 81 * v13 + 2439 * v19 == 1109296)
s.add(2585 * v18 + 4027 * v17 + 141 * v16 + 2539 * v15 + 3073 * v14 + 164 * v13 + 1556 * v19 == 1368547)
s.add(2080 * v18 + 358 * v17 + 1317 * v16 + 1341 * v15 + 3681 * v14 + 2197 * v13 + 1205 * v19 == 1320274)
s.add(840 * v18 + 1494 * v17 + 2353 * v16 + 235 * v15 + 3843 * v14 + 1496 * v13 + 1302 * v19 == 1206735)
s.add(101 * v18 + 2025 * v17 + 2842 * v16 + 1559 * v15 + 2143 * v14 + 3008 * v13 + 981 * v19 == 1306983)
s.add(1290 * v18 + 3822 * v17 + 1733 * v16 + 292 * v15 + 816 * v14 + 1017 * v13 + 3199 * v19 == 1160573)
s.add(186 * v18 + 2712 * v17 + 2136 * v16 + 98 * v13 + 138 * v14 + 3584 * v15 + 1173 * v19 == 1005746)
flag = []
if s.check() == sat:
ans=s.model()
flag.append(ans[v2])
flag.append(ans[v3])
flag.append(ans[v4])
flag.append(ans[v5])
flag.append(ans[v6])
flag.append(ans[v7])
flag.append(ans[v8])
flag.append(ans[v9])
flag.append(ans[v10])
flag.append(ans[v11])
flag.append(ans[v12])
flag.append(ans[v13])
flag.append(ans[v14])
flag.append(ans[v15])
flag.append(ans[v16])
flag.append(ans[v17])
flag.append(ans[v18])
flag.append(ans[v19])
flag.append(ans[v20])
flag.append(ans[v21])
flag.append(ans[v22])
flag.append(ans[v23])
for i in flag:
print((i),end=",")
print()
b=[78,83,83,67,84,70,123,112,105,112,95,105,110,115,116,64,108,108,95,90,51,125]
for i in b:
print(chr(i),end="")
#78,83,83,67,84,70,123,112,105,112,95,105,110,115,116,64,108,108,95,90,51,125,
#NSSCTF{pip_inst@ll_Z3}