第一周-cnblog

发布时间 2023-11-26 19:39:32作者: CCb0nd

第一周笔记

一.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中

image-20231122133802811

然后发现调用了VirtualProtect(encrypt, 0xC8u, 4u, &flOldProtect),对内存权限进行了修改,猜测是SMC

简单看一下逻辑,v7应该就是我们的输入,后面检查输入字符长度,说明flag应该是24位的,然后再进行wrong()和omg()

image-20231122134043967

点开encrypt,发现报错

image-20231122134147243

再看看wrong和omg函数

image-20231122134945105

image-20231122135112312

此处明显是把&unk_4030C0的值赋给v2,然后a1的值要等于v2,a1的值再wrong里面进行一些很简单的操作,先找到v2的值,然后可以写出逆向脚本,因为是int数组,所以是四位四位取

image-20231122135720718

与运算,其实就是i是奇数则(i&1)=1,为偶数(i&1)=0,奇数位就加回来,偶数位就异或.

image-20231122140209396

得到的是fakeflag,再看下面的encrypt

这里用到动态调试破解SMC,在自加密结束后下一个断点,注意输入的长度应该为24位,输入123456789123456789123456

image-20231122140607513

直接反汇编窗口下断点好像断不下来,于是在汇编里面下断点

image-20231122140741426

这次成功断下来了,然后F7进入encrypt函数,先按U取消函数定义,然后选中所有的数据,按c转换为代码

image-20231122140934092

这里选择force,然后回到开始按P,定义为函数,F5成功得到函数(这里其实有两个函数)

image-20231122141041153

第一个函数里面就是个简单的异或

image-20231122141919460

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,于是找了下,进行相同操作后发现第二个函数

image-20231122141330487

先将%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

image-20231122155121567

还是按U取消定义,然后往下,在这个地方按D,第二个函数也是一样的image-20231122155202063

然后运行ida python脚本

image-20231122155416958

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函数

image-20231123195220913

题目已经提示是迷宫题了,if里面检测了输入的长度,说明解迷宫步数应该是54,有个createmap函数,点进去看

image-20231123195352442

是用num数组里面的数进行操作然后得到map的值,现在map里面什么都没有

image-20231123195420719

于是在函数的结尾下一个断点,通过动态调试得到map

image-20231123195504726

随便输入几个数都行,因为判断长度的逻辑是在createmap后

image-20231123195519752

F7步入函数后,按F9运行到断点

image-20231123195658076

此时的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函数一堆看不懂的,于是准备动态调试寻找函数逻辑

image-20231123201716177

在最开始的地方下断点,第一个sub_140002410函数应该是printf的功能,下面那个猜应该是scanf的功能,开始调试

image-20231123202203484

果然在这里断下来了并且要求输入,为了方便看直接改名字scanf,并且将输入传入了函数的那个参数中,size应该是输入字符的长度

于是输入38个a继续看,发现Src这个参数就是我们的输入

image-20231123202529241

后面又是一堆乱七八糟的,看不太懂继续跑,if里面的判断其实就是干扰,动调发现里面的东西都会运行

image-20231123202719642

先是将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]

知道了加密逻辑,下一步就应该找到加密后的结果,继续动态调试

image-20231123203859799

看到有个buf2,后面又有cmp,感觉不用继续动态调试了,已经能猜出来了,buf2里面应该就是我们最后比较的值,提取出来

image-20231123204007467

最后写出加密脚本:

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中,函数名一堆看不懂,用动态调试寻找函数逻辑

image-20231124113251869

sub_472810(&dword_47DD80, Buf2)感觉像是输入函数

image-20231124113524718

这个明显就是比较函数了,所以感觉sub_4015A0(Buf2, strlen(Buf2), Destination, 6)像是关键的加密函数,在这个函数的入口下断点

image-20231124113723814

buf2里面明显是我们的输入,可以改改函数名和变量名方便看,步入加密函数看看

image-20231124113951903

看到关键的256,联想到RC4,后面v15是初始化s盒,v16是我们key(就是litctf)

image-20231124114317254

RC4是对称加密,于是继续运行到比较阶段,把密文dump下来,然后拿到cyberchef看

image-20231124120621148

得到的是假的flag,继续往后走,这里又对buf1进行了一次赋值,继续dump下来解密

image-20231124120653690

这次成功得到了flag

image-20231124121125323

4.[GDOUCTF 2023]Tea

题目链接:[GDOUCTF 2023]Tea | NSSCTF

一道魔改XTEA+动态调试寻找函数逻辑题

64位无壳,丢入ida64,先找字符串然后通过交叉引用定位关键代码,还是需要用动态调试来寻找函数作用

image-20231124194251908

经过调试可以改名一些函数,并且找到关键的三个函数

image-20231124201006294

第一个函数貌似是给V7重新赋值

image-20231124201043424

第二个函数就是把我们的输入复制到V9里面去image-20231124201153321

第三个函数就是很明显的加密函数了,这是个tea加密,我们需要找到三个值,Δ,key和加密后的密文,传进去的第一个参数就是我们的输入,就是等待加密的密文,第二个参数是V7,它的值就应该是我们的密钥了。然后根据逻辑Δ就是256256256

image-20231124201223822

接下来应该找加密后比较的密文了,在这个函数里面可以找到,然后就可以开始写脚本了,为了锻炼自己我决定手搓一个XTEA解密

image-20231124201734282

image-20231124201752137

#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

image-20231124105552024

判断输入长度为38后的两个函数应该是关键函数,点开一片红

image-20231124105628879

按D,然后将花指令nop掉,然后按C还原为代码

image-20231124105721484

得到第一个函数,第二个同类(要按p识别为函数)

image-20231124105811871

image-20231124105859689

最后写出解密脚本

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()判断是否有解,它将返回satunsat作为结果,如果有解就是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

很简单的逻辑就是求解

image-20231126140815112

直接写脚本

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}