z3约束求解
z3约束求解安装python版安装 1$ pip3 install z3-solver 基本用法变量表示一阶命题逻辑公式由项(变量或常量)与扩展布尔结构组成,在 z3 当中我们可以通过如下方式创建变量实例: 整型(integer,长度不限) 12>>> import z3>>> x = z3.Int(name = 'x') # x is an integer 实数类型(real number,长度不限) 1>>> y = z3.Real(name = 'y') # y is a real number 位向量(bit vector,长度需在创建时指定) 1>>> z = z3.BitVec(name = 'z', bv = 32) # z is a 32-bit vector 布尔类型(bool) 1>>> p = z3.Bool(name =...
常见编码加密识别
常见加密和编码识别常见加密算法和编码识别前言在对数据进行变换的过程中,除了简单的字节操作之外,还会使用一些常用的编码加密算法,因此如果能够快速识别出对应的编码或者加密算法,就能更快的分析出整个完整的算法。CTF 逆向中通常出现的加密算法包括 base64、TEA、AES、RC4、MD5 等。 Base64Base64 是一种基于 64 个可打印字符来表示二进制数据的表示方法。转换的时候,将 3 字节的数据,先后放入一个 24 位的缓冲区中,先来的字节占高位。数据不足 3 字节的话,于缓冲器中剩下的比特用 0 补足。每次取出 6 比特(因为 ),按照其值选择ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/中的字符作为编码后的输出,直到全部输入数据转换完成。 通常而言 Base64 的识别特征为索引表,当我们能找到 ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/ 这样索引表,再经过简单的分析基本就能判定是 Base64...
大小端的解析
大小端Errata Security: How to teach endian 理解字节序 - 阮一峰的网络日志 12大端字节序:高位字节在前,低位字节在后,这是人类读写数值的方法。小端字节序:低位字节在前,高位字节在后,即以0x1122形式储存。 小端的优势在于性能,计算机电路先处理低位字节,效率比较高,因为计算都是从低位开始的。所以,计算机的内部处理都是小端字节序。 大端的优势在于易读,符合人类读取数据的方法。 所以在计算机的内部处理中,基本上都使用小端,而不是人类易读的大端。 但是有一个特殊情况,数组在计算机的内部处理中不受大小端的影响,两者中数组的顺序一致。
Objection的基础使用
objectionobjection的介绍objection是一个运行时移动探索工具包,观察类方法,报告执行情况,由Frida提供支持。支持iOS 和 Android。 objection的安装1234Python 3.7.1pip3 install frida==12.8.0pip3 install frida-tools==5.3.0pip3 install objection==1.8.4 启动1.手机端或者模拟器开启对应版本的frida-server 12345┌──(root㉿r0env)-[~]└─# adb shellbullhead:/ $ su bullhead:/ # cd data/local/tmp/ bullhead:/data/local/tmp #...
buu第一页wp
buu1 Easyre main函数 reverse1 {hello_world}中‘o’被0替换 reverse2 {hacking_for_fun} i r被替换为1 内涵的软件 发现类似flag的字符串,用flag{}包住得到flag 新年快乐 upx Xor 对global再进行一次异或得到flag Exp: reverse3 先对输入字符串base64编码,再字符串加密 过程反向即可得到flag Exp: Hello world Mainactivity类中 不一样的flag 上下左右4种操作,应该是迷宫题 字符串可以分为5行 *1111 01000 01010 00010 1111# 遇到1退出 遇到#正确提升 说明要从*沿0走到# Flag为flag{222441144222} SimpleRev 先把text...