misc周报01

周报01

【古之立大事者，不惟有超世之材，亦必有坚忍不拨之志 ——苏轼】

AliyunCTF 题目复现

题目：mba

首先，要清楚这个题是干什么的。

题目：mba

I rolled my own MBA simplifier, but how disastrous could it be?

根据题目描述，这道题是关于一个mba简化器的，了解一下mba:

MBA混淆算法是一种用于软件保护和恶意软件混淆的技术。它通过将算术运算（如加法、乘法）和布尔运算（如与、或、非）混合，生成复杂的表达式，从而增加代码的可读性和逆向工程的难度。这种算法常用于软件加固和恶意软件中，以隐藏核心逻辑

MBA表达式：

根据官方WP的解释，这是一个基于MBA-Blast算法的简易MBA简化器。

---

我们首先查看题目中有用的附件：

【1】new-tactic.patch

在patches文件夹中，是new-tactic.patch文件，（.patch 文件是一种用于描述代码变更的文本文件，通常用于版本控制系统（如 Git、SVN 等）或软件开发中。它记录了文件的修改、添加或删除操作，以便将这些变更应用到其他代码库或分支中。.patch 文件的核心作用是提供一种标准化的方式来传递和应用代码变更。）

那么我们可以得知，官方WP中提到的Tactic的内容应该在这个文件中。WP：本题实现了一个基于MBA-Blast算法的简易的MBA简化器。具体的逻辑被作为一个Tactic实现在了Z3Prover的内部，并通过Z3 Python API调用

我们可以在其中查看mba_tactic.cpp的内容：

<简单说下结论，mba_tactic.cpp就是用来实现Z3 定理证明器来解析和验证布尔代数表达式>

（在mba_tactic.cpp 文件实现了一个 Z3 策略，用于处理和简化 MBA 表达式。它通过递归构建表达式、计算基向量组合来简化表达式，并提供了多个辅助函数来处理布尔函数和位向量表达式。

它定义了一个名为 mba_tactic 的类，该类通过重载 Z3 的 tactic 接口来实现 MBA 表达式的简化逻辑。

这个策略使用 MBA-Blast 算法来简化 MBA 表达式，尝试找到更简单的等价表达式。

mba_tactic.cpp 负责处理位向量（bit-vector）运算和布尔逻辑，将它们转换为简化的数学形式。）

【2】server.py

<同样先说结论：server.py 类似于主程序，用来处理用户的输入，并给出对应的结果>

一个 Python 程序，它使用 Z3 定理证明器来解析和验证布尔代数表达式。（它使用 Z3 Python API 来调用 mba_tactic 实现的逻辑，从而利用 Z3 定理证明器的能力。server.py 负责接收用户输入的表达式，将其解析为 MBAExpr 对象，然后使用 mba_tactic 进行简化。）

程序的主要逻辑如下：

定义语法规则：使用 Lark 库定义了一套语法规则（Rule），用于解析布尔代数表达式。表达式可以包含变量（如 x 和 y）、布尔运算符（如 &、|、^）、一元取反操作符（~）、整数常量以及括号。
解析器：使用 Lark 库生成两个解析器（P 和 PT），分别用于解析完整的表达式和单个项。
转换器：定义了一个转换器类 MBATransformer，用于将解析得到的抽象语法树（AST）转换为内部表示的 MBAExpr 对象。
布尔函数和 MBA 表达式：
BoolFunction 类表示布尔函数，可以是单个变量、取反变量或两个变量之间的布尔运算。
MBAExpr 类表示多线性布尔代数表达式，由多个项组成，每个项是一个系数和一个布尔函数的组合。
Z3 集成：使用 Z3 库将 BoolFunction 和 MBAExpr 转换为 Z3 表达式，以便进行逻辑验证。
主逻辑：

1.serve_challenge 函数是程序的主入口，它提示用户输入一个布尔代数表达式，然后尝试解析和验证该表达式。
2.用户输入的表达式首先被解析为 MBAExpr 对象。
3.如果表达式有效（不超过 200 个字符，项数不超过 15），则使用 Z3 定理证明器检查表达式是否恒等（即 expr != expr 是否为不可满足）。
4.如果表达式恒等，输出 "It works!"；否则，输出flag

---

那么，通过分析附件，我们知道：要想获取flag，我们需要做的事情就是构造一个符合要求的布尔代数表达式，使得使用z3定理证明器检查时，表达式不恒等！

假设现在我们已经有了一个表达式s，我们来分析它是怎样被进行检查的：

代码中，MBA 表达式被定义为一个包含多个项（coterms）的对象，每个项是一个系数和布尔函数的组合。代码中定义了 MBAExpr 类和 BoolFunction 类来表示和处理 MBA 表达式。

表达式首先被解析为 MBAExpr 对象的代码如下：

# 定义 MBATransformer 类，该类继承自 Lark 的 Transformer，
# 用于将解析得到的抽象语法树（AST）转换为 MBAExpr 对象。
class MBATransformer(Transformer):
    # Transformer 中定义了各种方法，用于处理解析树中的不同节点，
    # 并构建 MBAExpr 对象。

# 定义解析器 P，用于解析完整的表达式。
P = Lark(Rule, parser='lalr', start='start')

# 定义 parse 函数，它使用 MBATransformer 转换器和解析器 P，
# 将输入的表达式字符串解析为 MBAExpr 对象。
def parse(expr: str) -> MBAExpr:
    return MBATransformer().transform(P.parse(expr))

在主函数 serve_challenge 中，调用 parse 函数来解析用户输入的表达式：

def serve_challenge():
    FLAG = os.environ.get('FLAG', 'aliyunctf{this_is_a_test_flag}')

    expr = input("Please enter the expression: ")
    if len(expr) > 200:
        print("Expression is too long")
        exit(1)

    try:
        mba = parse(expr)  # 这里调用 parse 函数解析表达式
    except Exception as e:
        print("Could not parse the expression")
        exit(1)

    if len(mba.coterms) > 15:
        print("Too many terms")
        exit(1)

    # ... (后续逻辑处理)

在上述代码中，parse 函数是解析过程的关键，它接受一个字符串形式的表达式，通过 Lark 解析器和 MBATransformer 转换器将其转换为 MBAExpr 对象

terms 是 MBAExpr 类的一个属性，它是一个列表，包含表达式的各个项（coterms）。每个项是一个元组，由一个整数系数和一个 BoolFunction 对象组成。这些项代表了多线性布尔代数（MBA）表达式的各个部分。

<回顾一下>

以下是相关代码：

class MBAExpr(object):
    def __init__(self, coterms: List[Tuple[int, BoolFunction]]):
        self._coterms = coterms

    # ...（其他方法）...

    @property
    def coterms(self) -> List[Tuple[int, BoolFunction]]:
        return self._coterms

在这个类中：

• __init__ 方法用于初始化 MBAExpr 对象，接受一个包含多个项（coterms）的列表作为参数。
• coterms 属性是一个只读属性，返回 MBAExpr 对象中存储的项列表。

每个项（coterm）可以表示为：

• 一个整数系数，表示该项在表达式中的权重。
• 一个 BoolFunction 对象，表示该项对应的布尔函数。

例如，一个 MBA 表达式 2*(x & y) + 3*(~x) 可以被分解为两个项：

1. (2, BoolFunction('&', ['x', 'y']))
2. (3, BoolFunction('~', ['x']))

其中，这两项中的系数项通过coeff_type存放的（long long 类型）

[呃呃，不会了]

【求助ing………………………….】

使用 Z3 定理证明器检查表达式是否恒等的部分主要集中在 check_expression 函数中。以下是该函数的代码：

def check_expression(t: z3.Tactic, e: MBAExpr) -> bool:
  expr = e.to_z3expr(64)
  s = t.solver()
  s.add(expr != expr)

  s.set('timeout', 30000)   # 30 seconds
  r = s.check()
  if r == z3.unknown:
    print("Solver timed out")
    exit(1)
  return r == z3.unsat

这段代码的工作流程如下：

1. 将 MBAExpr 对象 e 转换为 Z3 表达式 expr，假设表达式使用的位数为 64。
2. 创建一个 Z3 求解器 s。
3. 向求解器添加约束 expr != expr，这是一个恒等式，如果表达式有效，则此约束应导致求解器返回 不可满足（unsatisfiable）。
4. 设置求解器的超时时间为 30 秒。
5. 调用求解器的 check 方法来检查约束是否可满足。
6. 如果求解器返回 z3.unknown（表示超时或出错），则打印超时信息并退出程序。
7. 如果求解器返回 z3.unsat（表示约束不可满足），则返回 True，表示表达式恒等。

本周取证专题练习（NSSCTF）

（源自NSSCTF的取证题）

题目：[蓝帽杯 2022 初赛]计算机取证_1

内存取证题目

直接使用volatility：

因为题目要求获得taqi7的开机密码，所以使用hashdump，拿到密码的哈希值

解密后拿到flag：

题目：[蓝帽杯 2022 初赛]计算机取证_2

要查看制作该内存镜像的进程Pid号：

buuCTF misc部分题目记录

题目01：SXMgdGhpcyBiYXNlPw==

第一步，题目为base64编码，先翻译过来：Is this base?，可知题目应当与base有关，打开题目，果然看到一连串的base64。

对其解密，得到明文：

这是法语歌曲《L’Assasymphonie》（杀人交响曲）的歌词，出自法国音乐剧《Mozart L’opéra Rock》（摇滚莫扎特），然而，我们将明文进行base64加密后，却发现与原来的base64编码不同！

因此，这道题目实质考察base64的隐写，使用脚本进行解密：

得到flag！

题目02：间谍启示录

非常简单的题目

iso镜像,直接使用foremost文件提取，在提取出来的rar压缩包中发现flag.exe!

注意这里如果直接打开iso镜像似乎是得不到flag.exe的

解压并运行，得到flag！

题目03：喵喵喵

图片放入StegSolve,在RGB的0通道发现异常，推测存在LSB隐写

在其BGR通道，发现一张png图片：

将其16进制数据导出，我们发现它（png）的文件头有问题，正常应该是89 50 4e……，将其文件头恢复，保存为png:

发现这是一张二维码，但是只有一半：

很明显的修改了图片的高度，将其放入随波逐流，恢复原宽高：

扫码后，是一串网址，打开百度网盘，下载flag压缩包（本以为flag出来了，没想到还是隐写）

这里是NTFS文件流隐写，使用AlternateStreamView进行扫描，导出flag.pyc文件

这里使用在线工具进行反编译，拿到源代码：

#!/usr/bin/env python
# visit https://tool.lu/pyc/ for more information
# Version: Python 2.7

import base64

def encode():
    flag = '*************'
    ciphertext = []
    for i in range(len(flag)):
        s = chr(i ^ ord(flag[i]))
        if i % 2 == 0:
            s = ord(s) + 10
        else:
            s = ord(s) - 10
        ciphertext.append(str(s))
    
    return ciphertext[::-1]

ciphertext = [
    '96',
    '65',
    '93',
    '123',
    '91',
    '97',
    '22',
    '93',
    '70',
    '102',
    '94',
    '132',
    '46',
    '112',
    '64',
    '97',
    '88',
    '80',
    '82',
    '137',
    '90',
    '109',
    '99',
    '112']

加密过程分析

1. 初始化:
   • flag 是一个字符串，假设为 '*************'（实际内容未知）。
   • ciphertext 是一个空列表，用于存储加密后的结果。
2. 加密循环:
   • 遍历 flag 中的每个字符，索引为 i。
   • 对每个字符进行以下操作：
     • s = chr(i ^ ord(flag[i]))：将字符的 ASCII 码与索引 i 进行异或操作，然后转换回字符。
     • 如果 i 是偶数，则将 s 的 ASCII 码加 10。
     • 如果 i 是奇数，则将 s 的 ASCII 码减 10。
     • 将处理后的 s 转换为字符串并添加到 ciphertext 列表中。
3. 反转列表:
   • 最后，将 ciphertext 列表反转，得到最终的加密结果。

解密过程

为了解密 ciphertext，我们需要逆向执行上述加密步骤：

1. 反转列表:
   • 首先将 ciphertext 反转，得到原始的加密顺序。
2. 解密循环:
   • 遍历 ciphertext 中的每个字符串，索引为 i。
   • 对每个字符串进行以下操作：
     • 将字符串转换为整数 s。
     • 如果 i 是偶数，则将 s 减去 10。
     • 如果 i 是奇数，则将 s 加上 10。
     • 将 s 转换回字符，然后与索引 i 进行异或操作，得到原始的 flag 字符。

写出解密脚本：

def decode(ciphertext):
    ciphertext = ciphertext[::-1]  # 反转列表
    flag = []
    for i in range(len(ciphertext)):
        s = int(ciphertext[i])
        if i % 2 == 0:
            s -= 10
        else:
            s += 10
        s = chr(i ^ s)
        flag.append(s)
    return ''.join(flag)

ciphertext = [
    '96', '65', '93', '123', '91', '97', '22', '93', '70', '102', '94', '132',
    '46', '112', '64', '97', '88', '80', '82', '137', '90', '109', '99', '112'
]

flag = decode(ciphertext)
print(flag)

得到flag：

题目04：小易的U盘

iso镜像,直接使用foremost文件提取，可以发现里面有一大堆文件：

这时候我们点击autorun.inf,出现提示信息，指向第32个副本：

将其放入随波逐流，得到flag：

题目05：[WUSTCTF2020]爬

文件类型未知，通过随波逐流查看，发现文件类型为pdf。

修改后缀名：

提示flag被图片覆盖住了：

我们需要移开图片，将pdf放入word打开，删除图片，我们发现下面有一行数据：

0x77637466323032307b746831735f31735f405f7064665f616e645f7930755f63616e5f7573655f70686f7430736830707d

很显然是十六进制（0x）,进行进制转换后得到flag：

题目06：[RoarCTF2019]黄金6年

题目是一个视频，对其分帧查看，发现隐藏的二维码：

第一个：

拿到key1

第二个：

第三个：

使用PS修复后进行扫描，得到key:

第四个：

将四个key合并在一起：iwantplayctf

那么这个key是用来干什么的呢？我们用010打开视频文件

在其底部发现一串base64编码：

进行解码，其中有一个rar压缩包，那么iwantplayctf应当就是密码了！

解压得到flag！

题目07：alison_likes_jojo

两张图片，先用随波逐流扫描一下，第一章图片里面有个zip,提取出来：

发现需要密码，这里并不是未加密，由于没有其他信息，尝试暴力破解，成功得到密码888866：

里面是base64,

进行多次base64解码后，拿到明文；

接下里看第二张图片，此为outguess隐写（别问怎么知道的，因为做不出来看了WP）

成功拿到flag!

学习总结：

base64隐写：

正常情况下，解Base64得到的文本再次Base64编码，得到的值应该是和原Base64编码一样的。如果不一样，则证明这段Base64编码文本被隐写了。
一般在做CTF题目时遇到大量Base64编码的文本时，就要考虑Base64隐写。
题目文件中每一行为一串Base64编码后的字符串，解题思路大致如下：
依次读取每行，从中提取出隐写位。

如果最后没有‘=’，说明没有隐写位，跳过。
如果最后是一个‘=’，说明有两位隐写位，将倒数第二个字符转化为对应的二进制索引，然后取后两位。
如果最后是两个‘=’，说明有四位隐写位，将倒数第三个字符转化为对应的二进制索引，然后取后四位。
将每行提取出的隐写位依次连接起来，每8位为一组转换为ASCII字符，最后不足8位的丢弃

base64隐写脚本：

#base64隐写
import base64

def Base64Stego_Decrypt(LineList):
    Base64Char = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"     #Base64字符集 已按照规范排列
    BinaryText = ""
    for line in LineList:
        if line.find("==") > 0:     #如果文本中有2个=符号
            temp = bin(Base64Char.find(line[-3]) & 15)[2:]      #通过按位与&15运算取出二进制数后4位 [2:]的作用是将0b过滤掉
            BinaryText = BinaryText + "0" * (4 - len(temp)) + temp      #高位补0
            print(BinaryText)
        elif line.find("=") > 0:        #如果文本中有1个=符号
            temp = bin(Base64Char.find(line[-2]) & 3)[2:]       #通过按位与&3运算取出二进制数后2位
            BinaryText = BinaryText + "0" * (2 - len(temp)) + temp      #高位补0
    Text = ""
    if(len(BinaryText) % 8 != 0):       #最终得到的隐写数据二进制位数不一定都是8的倍数，为了避免数组越界，加上一个判断
        print("警告:二进制文本位数有误，将进行不完整解析。")
        for i in range(0, len(BinaryText), 8):
            if(i+8 > len(BinaryText)):
                Text = Text + "-" + BinaryText[i:]
                return Text
            else:
                Text = Text + chr(int(BinaryText[i : i + 8], 2))
    else:
        for i in range(0, len(BinaryText), 8):
            Text = Text + chr(int(BinaryText[i : i + 8], 2))      #将得到的二进制数每8位一组对照ASCII码转化字符
        return Text

def Base64_ForString_Decrypt(Text):     #Base64解密
    try:
        DecryptedText = str(Text).encode("utf-8")
        DecryptedText = base64.b64decode(DecryptedText)
        DecryptedText = DecryptedText.decode("utf-8")
    except:
        return 0
    return DecryptedText

if __name__ == "__main__":
    Course = input("文件名:")
    File = open(Course, "r")
    LineList = File.read().splitlines()
    #print("显式内容为:")
    #for line in LineList:
    #    print(Base64_ForString_Decrypt(line),end="")
    print("隐写内容为:")
    print(Base64Stego_Decrypt(LineList))
    

解隐写脚本：

#解码base64隐写编码
#python版本 3.9

import base64

def int2Bin(digit):
	return bin(digit)[2:]	#将索引转成二进制，去掉'0b';


def binAsc(string):		#二进制转成ASCII码
	temp = ''
	for i in range(int(len(string) / 8)):
		temp += chr(int(string[i * 8 : i* 8 + 8] , 2))
	return temp

def readBase64FromFile(filename):
	Base64Char = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"     #Base64字符集 已按照规范排列
	result = ''
	with open(filename ,'r') as f:
		for data in f.readlines():
			if data.find('==') > 0:
				result += int2Bin(Base64Char.index(data[-4]))[-4:]		#根据隐写原理，‘==’情况取等号前最后一个字符转换后取后4位
			elif data.find('=') > 0:
				result += int2Bin(Base64Char.index(data[-3]))[-2:]		#根据隐写原理，‘=’情况取等号前最后一个字符转换后取后2位
	print(binAsc(result))

readBase64FromFile('flag.txt')

整形溢出

原理：

1. 每种整数数据类型（如 int, long, short 等）都有一个最大值和最小值，这个范围是由其位数（bit-width）决定的。例如，一个 32 位的有符号整数（int）通常有一个范围是 -2,147,483,648 到 2,147,483,647。

2. 当进行加法、减法、乘法等算术运算时，如果计算结果超出了数据类型所能表示的最大值或最小值，就会发生整数溢出