【CTF】CTF的一把梭Z3
发表于|更新于|CTF
|总字数:112|阅读时长:1分钟|浏览量:
安装z3
Z3开源项目地址：https://github.com/z3prover
Python文档翻译：https://arabelatso.github.io/2018/06/14/Z3%20API%20in%20Python/
- 官方文档
- C++ API
- .NET API
- Java API
- Python API (also available in pydoc format)
- Julia
首先访问Pypi下载对应的架构的whl文件，下载的时候注意对应自己电脑的平台和Python对应的版本。下载好后打开cmd输入pip install 下载的文件路径进行z3的安装。如图所示
文章作者: Jamie793
文章链接: https://blog.jamiexu.cn/2022/02/25/%E3%80%90ctf%E3%80%91ctf%E7%9A%84%E4%B8%80%E6%8A%8A%E6%A2%ADz3/
版权声明: 本博客所有文章除特别声明外，均采用 CC BY-NC-SA 4.0 许可协议。转载请注明来源 Jamie793’ S Blog！
赞助
wechat
alipay
相关推荐
2022-07-17
【CTF&WriteUp】2022-07 “强国杯” WriteUp含Re
战队名：超级飞侠撰写时间：2022-07-16 20:43强国杯【线上-2022】I. WEB【upload_lol】考点 上传绕过解法 经过多次测试发现，文件后缀不能带有php，文件内容不能有<? ，而?>这个好像没有过滤，文件类型改为image/jpeg即可；所以先上传一个.htaccess，内容为 12AddType application/x-httpd-php .jpgphp_value auto_append_file "php://filter/convert.base64-decode/resource=shell.jpg" 然后在shell.jpg文件里面写入base64加密过的一句话木马 蚁剑连上在var目录下得到flag 【file_sql_new】考点 字符型注入 过滤绕过解法 字符型注入，过滤了select，会替换为空，双写select绕过，回显2、3字段 爆表名 爆列名 获取flag路径 使用load_file读取flag II. MISC【welcome_to_QGB】考点 base64解...
2022-08-01
【CTF&WriteUP&Re】2022强网杯 ”Reverse“ WriteUp
2022强网杯 ”Reverse“ WPReverse1.【game】考点 Android逆向分析， Android网络请求，Web数据 解法 下载程序解压，发现是”ab”结尾的文件推测是安卓备份文件，用010Editor打开看一下，发现有明显的标识 ”ANDROID BACKUP“ 。 直接用android-backup-extractor提取出数据 提取之后发现有两个文件其中一个是apk文件直接用Jeb打开apk安装包 打开Manifest清单文件找到启动Act直接双击，tab键转成Java代码 根据Android生命周期可以知道onCreate是第一个启动的函数，直接找onCreate函数 经过分析发现在App启动的时候会自动登录，如果登陆失败则会跳转到LoginAct，否则跳转到MainAct 本想跟进autoLogin查看是如何登录的，结果发现了关键字眼函数”getFlag“ 那就先分析getFlag，发现需要传入三个参数然后通过发包获取Flag。根据后面的Api.class发现远程文件名 文件名搞到手了，剩下的是远程服务器地址了。直接暴力搜索h...
2022-06-08
【CTF&Re&WriteUp】第二届广东大学生网络安全攻防大赛ReWP
LUOJIABASUO 半个月前参加了一场比赛，我主要是负责的Re但是只解出了一个比较简单的那就是Pyre其他的我打开来看了一下就关了甚至没调试。后来发现还是挺简单的一个题目 RE反调试 首先老规矩IDA打开静态分析看看，发现压根无法分析。主要是这里使用了虚表调用。虚表调用的子程序（函数）是在每次运行的时候才计算出来子程序的地址。这导致IDA分析的时候是无法对齐静态的分析的。所以 按照老规矩动态调试挂起来，发现IDA没有控制权无法控制程序当程序运行起来的 时候没有响应切不能在IDA结束远程的调试目标。那说明存在反调试。 如何寻找反调试的地方在哪呢？也挺简单的只要在入口处下个断点不断的运行程序看看哪里IDA没有控制权了那么说明该地方具有反调试 要注意的 是main函数不是最开始的入口，”__scrt_common_main_seh“ 这个子程序才是最开始执行的 引用来自https://www.dazhuanlan.com/relic256/topics/1212274 虽然 VS 系列入口函数均为mainCRTStartup，但不同版本的实现仍...
2022-06-05
【WP/CTF】RCTF 2018 Simple vm
下载：下载 VM虚拟保护——Simple VM需要知识 数电基础 C语言基础 x86汇编指令 逻辑分析能力 VM保护基本术语 Dispatcher: 调度器，用于判断跳转到对应的Handler执行指令 Handler: 处理器，用于模拟每个指令 分析 下载后发现有两个文件，分别是 p.bin vm_rel 我们直接用IDA打开vm_rel这个文件，发现是一个64位的elf文件。老规矩在左边的Function names中搜索main直接打开main函数查看一下伪代码 - 经过简单的分析知道，首先程序会打开“p.bin”的文件然后在内存中分配一个和文件大小一样大的空间。并把分配 好的内存的地址存放到v5，再经过fread()函数读取文件中的内容存放到内存中 然后调用子程序sub_4008996开始程序的执行 直接双击该子程序进去可以看到由while(1),switch语句构成整个子程序 在虚拟机保护的分析中只要看到类似的结构，就可以判断出该子程序就是整个vm的核心Dispatcher - 看到这里对于初学者来说可能比较...
2022-06-01
【CTF/WP】DDCTF 2018黑盒破解——简单的VM入门
下载：DDCTF 2018黑盒破解 LUOJIBASUO这是我初学VM的第一个程序，虽说网络上有其他博主下写的WP但是对于刚开始学VM的来说我觉得是难以理解的，主要是程序的执行流程懂得了程序如何执行剩下的就好办了。同时感谢其他博主的WP学习了很多 分析文件 文件下载下来后，发现有两个文件 1、ReverseMe.elf 2、flag-48ee204317.txt 根据做题的经验和文件后缀大概猜测一下文件的类型是ELF64的Linux程序。直接用IDA64打开 打开后看可以看到我们猜测的没错，不会猜测可以使用PEID和exeinfope 打开直接搜索main函数，在右侧代码可以看到是判断了byte_603F00的变量是否正确。 把用鼠标点击一下该变量光标放在鼠标上按键盘的 “X” 即可打开变量的交叉引用。如上图，Type中是 “w” 为写，如果是 “r” 就是读，从图中可以看到在sub_40133D这个子程序设置了该参数的数值。双击第一条数据可以直接跳转到对应的地方 发现经过了几个判断成功后才置1，如果按照刚刚的方法直接查找该子程...
2022-06-09
【CTF/WP/Crypto】第二届广东大学生网络安全攻防大赛
Crypto-xor2程序分析 ”轮环异或加密，你能解开么？格式：flag{}“ 文件下载有一个py文件和一个文本文件 从描述可得知就是一个异或加密 从图中分析得知密钥是四位的密钥且不知道，然后flag也不知道。基本上无解了 But!!!从描述中可知flag前四位是”flag”又是异或加密。异或有个特性就是异或两次等于原文那么是不是可以利用给出的前四个flag进行key的解密呢 解密脚本编写123456789101112131415161718# 从cipher中整理得到的数据 encData = [ 0x1E, 0x14, 0x19, 0x1F, 0x03, 0x1E, 0x1B, 0x1B, 0x1A, 0x48, 0x4E, 0x4E, 0x4D, 0x55, 0x1A, 0x1B, 0x1D, 0x4D, 0x55, 0x1C, 0x4B, 0x4A, 0x41, 0x55, 0x19, 0x1B, 0x19, 0x4F, 0x55, 0x41, 0x41, 0x49, 0x4F, 0x41, 0...
评论
公告
Welcome to my blog. The harder you work, the more luck you have.