利用 Z3 SMT 约束求解破解弱随机数算法
导语：这篇文章主要是介绍Z3，它是麻省理工学院的一款SMT求解器，将讨论SMT求解器的一些典型用法，展示如何使用Z3的Python绑定生成约束，并提供使用此技术进行WebApp安全测试的示例。
0x00 基础介绍
这篇文章主要是介绍Z3，它是麻省理工学院的一款SMT求解器，将讨论SMT求解器的一些典型用法，展示如何使用Z3的Python绑定生成约束，并提供使用此技术进行WebApp安全测试的示例。
SMT求解器应用范围非常广泛，适用于从预测genomic regulatory logic到designing microfluidic systems 和 validating cloud network configurations。从本质上讲，SMT求解器提供了一种正式的方法来探索和推理复杂的相互依赖的系统。
SMT求解器的一个重要应用是形式验证，例如，软件的符号执行，输入分析和安全测试。此类别中的一些非常好用的工具包括Microsoft Research的SAGE，KLEE，S2E和Triton。对符号执行应用特别有用的SMT求解器包括Z3，STP，Z3str2和Boolector。
这篇文章分为三个部分，第一部分介绍了Z3的Python绑定，并演示了如何进行约束求解。第二部分介绍了线性同余生成器的概念，并演示了Z3如何用于预测PRNG输出。最后，第三部分扩展了第二部分中使用的模型，以演示使用OWASP Benchmark方法的实际使用。
0x01 介绍Z3
在深入研究更复杂的问题之前，我们会先演示一下如何对数学难题进行建模。我们的目标是让读者熟悉使用Z3的Python绑定约束求解。因此，如果你已经很熟悉Z3了，可以直接跳到第二部分。
我们使用一个典型的编程问题作为切入点：编写一个接受两个参数N和n并返回布尔值的函数，函数检查是否存在n个连续自然数（不包括零）使得∑ n i = 1 a i = N
如果你还记得这种计算问题，其实可以使用Gauss’s tric来计算总和：
或者使用简化方法：
使用这个公式，我们可以计算出一个候选者。如果候选者是自然数，则该函数应该返回true，否则就是假。代码虽然简单，但需要一些推导。
现在让我们将这个问题看作一个约束系统。第一个约束是：
ai+1=ai+1
另外，我们应该对总和有一个约束：
n∑i=1ai=N
让我们将这些约束转换为Z3模型：
import z3 as z
z.set_param('parallel.enable', False)首先，定义我们的目标：
n = 3 N = 1050
接下来将生成一些符号变量。符号变量（与我们稍后将使用的具体变量相对）充当占位符。它们的行为类似于Z3的键入机制，并帮助它选择合适的解决方案策略。此外，只要模型可以满足，就可以使用符号变量从模型中提取具体值。
注意使用列表推导（后面我们将广泛使用字典理解）和f-strings来生成具有唯一名称的多个符号变量。
ints = [z.Int(f'int_{i}') for i in range(n)]现在将实例化一个求解器对象。解算器对象接受约束检查，如果它们是可满足的。解决方案可以通过特定策略进行调整，给定中间目标，并充当Z3的前端。为了解决我们的问题，我们将设置三个约束：
1.a0,...,an−1∈N1.a0,...,an−1∈N - non-negative natural numbers
2.ai+1=ai+12.ai+1=ai+1 - consecutive numbers
3.∑ni=1ai=N3.∑i=1nai=N - sum must equal to some predefined value
s = z.Solver() for i in range(n-1): # Constraint #1 s.add(ints[i] > 0) # Constraint #2 s.add(ints[i+1] == ints[i] + 1) # Constraint #3 s.add(z.Sum(ints) == N)
最后，我们将使用check()求解器对象的方法来测试约束的可满足性。该check()方法返回以下响应之一：sat，不满，不可行或未知。我们的问题非常小（就限制数量而言），所以我们只能得到满足的响应。
if s.check() == z.sat:
m = s.model()
print('Found a solution')
print(f'({n} terms) {m[ints[0]].as_long()} + ... + {m[ints[n -1]].as_long()} == {N}')
else:
print(f'Finding {n} consecutive integers with a sum of {N} is unsatisfiable')
Found a solution
(3 terms) 349 + ... + 351 == 1050如上所述，约束是可以满足的。注意我们使用该model()方法来获取模型对象。然后，使用符号变量使用该as_long()方法从模型对象中提取具体值。
接下来，我们将概括我们的模型，并说明它可以用来提出一个更复杂的问题。
注意：这样就返回了求解器对象，稍后可以使用解算器添加其他约束来描述更复杂的模型。
def build_solver(n: int, N: int):
# Create symbolic variables
ints = [z.Int(f'int{i}') for i in range(n)]
# Instantiate a solver
s = z.Solver()
for i in range(n-1):
# Consecutive numbers
s.add(ints[i+1] == ints[i] + 1)
# Non-zero natural numbers
s.add(ints[i] > 0)
# Sum
s.add(z.Sum(ints) == N)
return s使用此方法，可以无缝地生成求解器对象。返回求解器对象的另一个原因是它可以让我们检查我们的约束，添加其他约束，强制求解策略等等：
s = build_solver(n = 3, N = 1337) print(s) [int1 == int0 + 1, int0 > 0, int2 == int1 + 1, int1 > 0, int0 + int1 + int2 == 1337]
使用这种方法，可以检查模型输入的集合是否可以满足。例如，下面是在探索N = 1337的解空间：
for i in range(3, 10):
print(f'Sum 1337 is {build_solver(n = i, N = 1337).check()} with {i} integers')
Sum 1337 is unsat with 3 integers
Sum 1337 is unsat with 4 integers
Sum 1337 is unsat with 5 integers
Sum 1337 is unsat with 6 integers
Sum 1337 is sat with 7 integers
Sum 1337 is unsat with 8 integers
Sum 1337 is unsat with 9 integers摘要：本节介绍Z3和基本模型的构建。我们演示了如何将数学问题表示为一组约束，将模型构造逻辑封装到函数中并探索问题的解空间。在下一节中，我们将演示如何使用Z3对算法进行建模并使用求解器对象提取（假设为）隐藏的内部状态。
0x02 使用PRNG算法建模
在熟悉Z3的基本特征之后，让我们尝试将这些技能应用到真实世界的算法中。在这个例子中，我们将：
· 描述流行的伪随机数发生器（PRNG）的工作原理：线性同余发生器（LCG）
· 开发一个使用Z3执行LCG的功能
· 预测LCG生成的数字序列中的下一个值
· 提取在已知LCG生成数字序列之前生成的值
· 提取用于实例化PRNG的种子
线性同余发生器（LCG）
这种功能具有数字随机数的属性（因此伪随机）。LCG是一种循环关系，其中初始值（称为“种子”）经历产生新数字的数学操作。新数字将成为下次调用函数时使用的种子。这种方法很快，只要仔细选择参数（下一节中更多关于它们），它就可以通过一些随机性统计测试。
有关LCG及其局限性的简短介绍，请查看有关线性同余生成器的Wikipedia页面。
典型的LCG通过执行以下步骤生成数字：
· 通过幻数乘以种子
· 在乘法结果中添加另一个幻数
· 用第三个幻数取结果的模数
因此，算法的魔术数字的选择是至关重要的。这些参数选择不当会产生强吸引力。吸引子是动态系统的一个特征，其中输入的扰动导致输出很少或没有变化（更多关于吸引子可以在这里找到）。下面可以看到参数选择不佳的一个例子，其中模数和被乘数之间存在简单的乘法关系。此选择会导致强吸引子和短周期（在重复数字之前调用函数的次数）：
这些图像中X轴上的值表示生成了多少个数字，Y轴表示生成的数字。对于种子值532（左图），我们看到强吸引子的行为。或者，对于种子值580（右图），我们看到短周期的示例。用于生成这些图像的小程序可在此处获得。
从上面的图像可以推断，使用魔术小数乘数= 10＆模数= 140和种子532或580，必然导致强吸引子行为。基本上，如果使用这些幻数并且生成两个提到的值中的一个，则序列的其余部分很容易预测。例如，假设我们选择了一个不同于532的种子，并且在生成n个调用532之后，序列中的所有未来数字都将为0。因此，即使选择“强”魔术数字有时也会导致质量随机性差。
作为一个实际的例子，我们将研究MSVC 2013中的LCG实现，已知MSVC相对较弱（即魔术数字选择不当）。
在MSVC 2013中实现rand（）
用于在MSVC 2013中实现rand（）的算法是简单LCG的一个很好的例子：
static unsigned long int next = 1;
int rand(void) /* RAND_MAX assumed to be 32767. */
{
next = next * 214013 + 2531011;
return (unsigned)(next/65536) % 32768;
}基于此片段，我们希望生成使用Z3模拟算法的约束。具体来说，假设我们有一系列由算法生成的数字：
· 我们能预测序列中的下一个值吗？
· 我们可以计算序列中的前一个数字吗？
· 我们需要提供Z3来正确预测序列中下一个数字的最短序列是什么？
· 解决方案是否独特？我们能找到满足我们约束条件的其他内部状态吗？
现在让我们假设我们运行了rand()10次并获得了以下数字：
4, 54, 63, 79, 13, 55, 76, 11, 14, 45
让我们构造模拟rand（）所需的约束并回答上述问题。 注意：通过打印rand（）％100生成数字以将数字约束到[0,100]范围，用于初始化该功能的种子是1337。
使用Z3模拟rand（）
在这个例子中，我们将开始使用位向量（BitVec）对象。这些对象是数据存储在内存中的方式的符号表示，需要定义它们的大小。使用位向量允许我们使用按位运算符，我们将在下一个示例中广泛使用它们。在这个例子中，我们将使用位移和'按位和'运算符来表示除法和模运算。
我们首先定义一些符号变量。我们将定义两个变量（output_prev，output_next）来表示序列之前和之后生成的数字。此外，我们将定义10个state＃变量来表示next代码片段中的变量。注意使用字典理解来生成state＃变量。使用字典是一种有用的模式，可以以可访问的方式保存大量符号变量。
output_prev = z.BitVec('output_prev', 32)
states = {f'state_{i}': z.BitVec(f'state_{i}', 32) for i in range(1, 11)}
output_next = z.BitVec('output_next', 32)实例化解算器
s = z.Solver()
现在让我们开始添加问题约束，第一个约束是数字序列是通过顺序调用生成的rand()，因此：
state_2=state_1×21401
state_3=state_2×214013+2531011
......
state_10=state_9×214013+2531011
for i in range(2, 11):
s.add(states[f'state_{i}'] == states[f'state_{i - 1}'] * 214013 + 2531011)
print(s)
[state_2 == state_1*214013 + 2531011,
state_3 == state_2*214013 + 2531011,
state_4 == state_3*214013 + 2531011,
state_5 == state_4*214013 + 2531011,
state_6 == state_5*214013 + 2531011,
state_7 == state_6*214013 + 2531011,
state_8 == state_7*214013 + 2531011,
state_9 == state_8*214013 + 2531011,
state_10 == state_9*214013 + 2531011]第二个约束表示我们为10个数字得到的值，我们将模拟return语句。在该示例中，我们将演示使用逐位操作，以显示在某些情况下基于Z3的逐位操作和基于Python的按位操作如何可以互换使用：
· 每个状态除以65536（相当于向右移16位）
· 然后我们将剩下的除以32768（相当于做n＆0x7FFF）
· 最后，提示％100应该等于我们集合中的每个数字
因此：
((state_1/65536)%32768)%100≡((state_1>>16)&0x7FFF)%100=4
((state_10/65536)%32768)%100≡((state_10>>16)&0x7FFF)%100=45
注意我们如何使用基于python和Z3的按位运算来构造约束。Z3为按位操作提供了便利，但知道使用它们不是强制性的，这很有用。Z3按位操作首选的一个特定情况是签名是必要的。例如，在我们的例子中，我们对无符号模数感兴趣，Z3为其提供了URem方法。
random_nums = [4, 54, 63, 79, 13, 55, 76, 11, 14, 45]
for i in range(2, 10):
s.add(z.URem((states[f'state_{i}'] >> 16) & 0x7FFF ,100) == random_nums[i - 1])最后，我们将为系列中的下一个和上一个数字设置约束：
s.add(output_prev == z.URem((states['state_1'] >> 16) & 0x7FFF ,100)) s.add(output_next == z.URem((states['state_10'] >> 16) & 0x7FFF ,100))
现在来看看我们的完整模型：
print(s) [state_2 == state_1*214013 + 2531011, state_3 == state_2*214013 + 2531011, state_4 == state_3*214013 + 2531011, state_5 == state_4*214013 + 2531011, state_6 == state_5*214013 + 2531011, state_7 == state_6*214013 + 2531011, state_8 == state_7*214013 + 2531011, state_9 == state_8*214013 + 2531011, state_10 == state_9*214013 + 2531011, URem(state_2 >> 16 & 32767, 100) == 54, URem(state_3 >> 16 & 32767, 100) == 63, URem(state_4 >> 16 & 32767, 100) == 79, URem(state_5 >> 16 & 32767, 100) == 13, URem(state_6 >> 16 & 32767, 100) == 55, URem(state_7 >> 16 & 32767, 100) == 76, URem(state_8 >> 16 & 32767, 100) == 11, URem(state_9 >> 16 & 32767, 100) == 14, output_prev == URem(state_1 >> 16 & 32767, 100), output_next == URem(state_10 >> 16 & 32767, 100)]
从一系列10个生成的数字开始。我们构造了一组模拟rand()函数操作的约束。使用序列中的中间8个数字来设置函数内部状态的约束。最后，设置约束output_next和output_previous符号变量。如果我们的约束是可满足的，则这两个变量应该与生成的序列中的第一个和最后一个数字保持相同的值。检查一下：
print(s.check()) sat print(s.model()) [state_3 = 3311639122, state_7 = 535860406, state_2 = 1700980091, state_4 = 4092565453, state_8 = 1173829793, state_5 = 2417052508, state_6 = 3389729967, state_1 = 2436150040, state_9 = 2200877280, output_next = 45, output_prev = 4, state_10 = 173405219]
结论：使用从源代码派生的一组约束，我们能够预测序列中的下一个数字。此外，我们能够计算序列之前的数字。
探索rand（）模型的解空间
接下来，尝试找到预测下次调用输出所需的最小值rand()。为此，我们将上述逻辑包装在一个函数中。该函数有两个参数：数字列表和序列中的下一个数字。该函数生成相关数量的约束并检查其可满足性。如果模型是可满足的，它会在序列中打印计算的和预期的下一个数字。
def break_rand(nums: list, next_num: int):
n_nums = len(nums)
#print(f'len nums: {n_nums}')
states = {f'state_{i}': z.BitVec(f'state_{i}', 32) for i in range(1, n_nums + 2)}
#print(states)
output_next = z.BitVec('output_next', 32)
s = z.Solver()
for i in range(2, n_nums + 2):
s.add(states[f'state_{i}'] == states[f'state_{i - 1}'] * 214013 + 2531011)
for i in range(1, n_nums + 1):
s.add(z.URem((states[f'state_{i}'] >> 16) & 0x7FFF ,100) == nums[i - 1])
s.add(output_next == z.URem((states[f'state_{n_nums + 1}'] >> 16) & 0x7FFF ,100))
#print(s)
if s.check() == z.sat:
print(f'For the sequence: {nums}, problem is satisfiable')
print(f'We were expecting: {next_num} and got: {s.model()[output_next]}\n')
else:
print(f'For the sequence: {nums}, problem is unsatisfiable')
return s, states, output_next
random_nums = [4, 54, 63, 79, 13, 55, 76, 11, 14, 45]
for i in range(3, 10):
break_rand(random_nums[:i], random_nums[i])
For the sequence: [4, 54, 63], problem is satisfiable
We were expecting: 79 and got: 94
For the sequence: [4, 54, 63, 79], problem is satisfiable
We were expecting: 13 and got: 60
For the sequence: [4, 54, 63, 79, 13], problem is satisfiable
We were expecting: 55 and got: 55
For the sequence: [4, 54, 63, 79, 13, 55], problem is satisfiable
We were expecting: 76 and got: 76
For the sequence: [4, 54, 63, 79, 13, 55, 76], problem is satisfiable
We were expecting: 11 and got: 11
For the sequence: [4, 54, 63, 79, 13, 55, 76, 11], problem is satisfiable
We were expecting: 14 and got: 14
For the sequence: [4, 54, 63, 79, 13, 55, 76, 11, 14], problem is satisfiable
We were expecting: 45 and got: 45结论：在所有情况下，我们都能找到满足约束条件的解决方案。虽然约束条件令人满意，但请注意上面的前两个结果：虽然预测的下一个数字与预期值不匹配，但约束条件是可满足的。该结果表明模型可满足性并不意味着唯一性。在求解约束系统时，Z3返回它找到的第一个解，在我们的例子中，它会在序列中产生错误的数字。尽管如此，当我们为求解器提供五个或更多个数时，它始终如一地预测序列中正确的下一个数字。可以从这些结果推断出的另一个结论是，对于三个和四个数字的序列，至少存在产生这些数字的两个不同的内部状态。不同的内部状态产生不同的序列，同时保持前三个或四个数字。
接下来，我们想尝试枚举满足我们约束的所有解决方案。枚举解决方案使我们能够衡量我们解决方案的独特性。
枚举解决方案
在本节中，我们将尝试枚举满足约束条件的所有可能解决方案。为此，将使用求解器对象并为我们已经找到的解决方案添加否定约束。即：
state_1,...,state_n≠solution[state_1],...,solution[state_n]
为了自动化这个实验，我们将定义一个重复尝试使用求解器对象查找解法的函数。每当求解器找到一组解决约束的不同内部状态时，我们将找到的值添加到禁用值列表中。请注意我们使用Or()和eval()作为构建约束的替代方法。
链接到代码段。
def enumerate_solutions(nums: list, next_num: int, print_model: bool = False, print_solutions: bool = False):
s, states, output_next = break_rand(nums = nums, next_num = next_num)
counter = 0
solution_list = []
while s.check() == z.sat:
counter += 1
solution_list.append(s.model()[output_next].as_long())
print(f'Solution #{counter}')
if print_model:
print(f'{s.model()}\n')
# Create constraints using string concatenation
or_expression = 'z.Or('
for i in states.keys():
if i == 'output_next': continue
or_expression += f'states[i] != s.model()[states[i]], '
or_expression += ')'
s.add(eval(or_expression))
print(f'Found a total of {counter} solutions')
if print_solutions:
print(f'The solutions are: \n{solution_list}')
print(f'The solution set is: \n{set(solution_list)}')
enumerate_solutions(random_nums[:5], random_nums[5], print_model = True)
For the sequence: [4, 54, 63, 79, 13], problem is satisfiable
We were expecting: 55 and got: 55
Solution #1
[state_3 = 1164155474,
state_2 = 3848463739,
state_1 = 288666392,
state_4 = 1945081805,
state_5 = 269568860,
output_next = 55,
state_6 = 1242246319]
Solution #2
[state_3 = 3311639122,
state_2 = 1700980091,
state_1 = 2436150040,
state_4 = 4092565453,
output_next = 55,
state_5 = 2417052508,
state_6 = 3389729967]
Found a total of 2 solutions
enumerate_solutions(random_nums[:9], random_nums[9], print_model=True)
For the sequence: [4, 54, 63, 79, 13, 55, 76, 11, 14], problem is satisfiable
We were expecting: 45 and got: 45
Solution #1
[state_7 = 2683344054,
state_2 = 3848463739,
state_1 = 288666392,
state_4 = 1945081805,
state_8 = 3321313441,
state_3 = 1164155474,
state_5 = 269568860,
state_6 = 1242246319,
state_9 = 53393632,
output_next = 45,
state_10 = 2320888867]
Solution #2
[state_7 = 535860406,
state_2 = 1700980091,
state_1 = 2436150040,
state_4 = 4092565453,
state_9 = 2200877280,
state_8 = 1173829793,
state_3 = 3311639122,
state_10 = 173405219,
output_next = 45,
state_5 = 2417052508,
state_6 = 3389729967]
Found a total of 2 solutions分析：用5或9个序号输入算法能够识别满足约束的两个不同的内部状态。虽然在每种情况下，我们确定了两个不同的状态，两者都在序列中产生正确的下一个数字。此外，我们已经确定了两个不同的初始内部状态（即state1,288666392或2436150040），它们导致相同的数字链。只要观察到至少五个连续数字，就可以预测序列中的下一个数字。
现在对4个数字的序列尝试相同的方法（我们已经知道它们不会在链中产生正确的下一个数字）。
enumerate_solutions(random_nums[:4], random_nums[4], print_solutions=True)
For the sequence: [4, 54, 63, 79], problem is satisfiable
We were expecting: 13 and got: 60
Solution #1
...
Solution #40
Found a total of 40 solutions
The solutions are:
[60, 49, 49, 9, 9, 29, 29, 32, 32, 18, 18, 93, 93, 69, 77, 77, 69, 67, 5, 5, 25, 25, 13, 13, 55, 55, 48, 48, 12, 12, 60, 24, 67, 24, 16, 16, 89, 89, 96, 96]
The solution set is:
{5, 9, 12, 13, 16, 18, 24, 25, 29, 32, 48, 49, 55, 60, 67, 69, 77, 89, 93, 96}分析：用4个连续rand()算法，我们能够识别满足约束的40（！）个不同的内部状态。这些是每个解决方案预测的序列中的下一个数字：
60, 49, 49, 9, 9, 29, 29, 32, 32, 18, 18, 93, 93, 69, 77, 77, 69, 67, 5, 5, 25, 25, 13, 13, 55, 55, 48, 48, 12, 12, 60, 24, 67, 24, 16, 16, 89, 89, 96, 96
虽然内部状态是不同的，但发现的所有解决方案都必须产生序列：4,54,63,79。这意味着我们找到了一组40个初始状态（state_1）来创建这个确切的序列。此外，40种不同的解决方案仅与链中的第5个数字不同。具体来说，如果我们知道序列中的前四个数字，那么第五个数字可以有20个不同的值。基本上，我们已经找到了有限数量的可能解决方案。因此，如果我们观察到四个数字，我们可以以5％的置信度预测序列中的下一个数字。
结论：基于上面概述的实验，我们可以找到产生特定序列（伪）随机数的有限数量的初始状态。只要我们观察到足够大的连续数字序列，这个陈述就成立了。此外，似乎对于MSVC 2013 rand()函数中使用的幻数（已知它们很弱），观察到5个数字的序列就足以完全放心地预测第6个数字。
上述方法的一种可能的扩展是找到产生例如四个零序列所需的种子：
enumerate_solutions([0, 0, 0, 0], 0) For the sequence: [0, 0, 0, 0], problem is satisfiable We were expecting: 0 and got: 10 Solution #1 ... Solution #38 Found a total of 38 solutions enumerate_solutions([0, 0, 0, 0, 0], 0) For the sequence: [0, 0, 0, 0, 0], problem is unsatisfiable Found a total of 0 solutions
结论：基于这两个实验，有38个初始状态（种子）导致四个连续的零输出，而没有种子产生五个连续的零。
0x03 将此方法扩展到现实环境的例子
我们将这种方法扩展到另一个基于LCG的PRNG。具体来说，在本教程中，重点是攻击在java.util.Random class中的PRNG 。在构建能够预测值并提取种子的模型之后，我们将在实际的WebApp上测试我们的方法。
与上述MSVC 2013 rand()函数类似，该PRNG 使用种子/先前生成的数字来生成序列中的下一个数字。下面是java.util.Random该类的（部分）源代码。
76: public class Random implements Serializable
77: {
...
121: public Random()
122: {
123: this(System.currentTimeMillis());
124: }
...
132: public Random(long seed)
133: {
134: setSeed(seed);
135: }
...
151: public synchronized void setSeed(long seed)
152: {
153: this.seed = (seed ^ 0x5DEECE66DL) & ((1L << 48) - 1);
154: haveNextNextGaussian = false;
155: }
...
173: protected synchronized int next(int bits)
174: {
175: &nb
发表评论
提供云计算服务