异常：型号不可用

Question

我在使用符号执行模型的 z3 中收到模型不可用的错误消息。 初始代码添加了 v1 和 v2 并且它可以工作，但是一旦我替换 v1 和 v2 值，我就会收到模型不可用错误 我检查了其他帖子，但无法从中得到答案。

enter SEED = 682466241
prng = RNG(SEED)
v1 = prng.next(26)
v2 = prng.next(26)
print(SEED, v1, v2)

v1 = 57508594
v2 = 29407552
s = Solver()
s.add(seed >= 0)
s.add(seed <= 0xFFFFFFFF)
s.add(RNG(seed).next(26) == v1)
s.add(RNG(seed).next2(26) == v2)
s.check()
#print(s.check())
#print(s.model())
m = s.model()
print("Seed is: ", m[seed])

prng = RNG(int(str(m[seed])))
prng.next(26)
prng.next(26)
v3 = prng.next(26)
print("V3 is:", v3)

我从这个link获得了代码，并在这个video中使用了它，但是当我尝试它时，我收到模型不可用的错误消息。 任何解决此问题的帮助将不胜感激。

Answer 1

问题出在这两行：

v1 = 57508594
v2 = 29407552

如果您查看您站点的原始网页，他们没有这些作业。本质上，您更改了

v1

和

v2

的值（这很好），然后 z3 告诉您这些不是可行的值。也就是说，如果您从代码开始：

SEED = 682466241
prng = RNG(SEED)

并且有：

s.add(RNG(seed).next(26) == v1)
s.add(RNG(seed).next2(26) == v2)

然后

v1

和

v2

最终成为不同的值。这是一个冲突。因为你本质上是说

v1

计算出来的

RNG(seed).next(26)

一定是

57508594

，但实际上计算结果是

14325532

，并且约束

57508594 == 14325532

是不可满足的。 （因为这些数字彼此不相等。）因此，z3 最终告诉您

unsat

，即您的约束无法满足；因此没有模型。

您应该删除对

v1

或

v2

的分配才能获得工作程序。但当然，这完全取决于您到底想做什么。

一般来说，使用 SMT 求解器对某种加密算法进行“逆向工程”是徒劳的尝试。 （除非底层算法真的很简单；即，密码学上不强。）但话又说回来，在不知道你的目标的情况下，很难发表意见。