v5 = serial[6] + serial[0] - serial[7] - serial[2];
LOBYTE(v5) = serial[1];
v8 = serial[3] + v5 - serial[4];
if ( v8 != serial[5] )
goto FAIL;
变量
serial[]是一个数组，表示键abcdefgh的字节。 Dor示例serial[0] = 0x61。如果我们假设serial[5]是0x66（字母'f'），那么我如何计算所需的密钥以在0x66中获得v8，因为您会看到一些计算已确定v8的可能值。 />#1 楼
好了，等式非常简单，您说哈希是通过以下公式完成的：找出这些方程式的可能关键字：实际上，您可以根据需要添加任何约束（如果需要，可以尝试将序列强制在标准可打印ASCII字符之内（请注意，它可能不接受任何解决方案！）。评论
因此，smt求解器也将其推广为b + d -e = f，因此在assert（> f 0x60）处添加约束应产生0x61，我认为
– blabb
17年7月4日在6:20
非常感谢，这正是我所需要的。 （对不起，我无法接受答案，因为问题是我加入之前提交的）
– 0x3h
17年7月4日在7:27
嗯，这篇文章让我想起了->'Assemby手动伪代码'。
–恐怖
17年7月5日在12:26
@ 0x3h，如果您未收到我的举报消息，请使用底部的“联系我们”链接合并两个帐户。
–伊戈尔·斯科钦斯基♦
17年7月5日在13:08
@perror大声笑是的，没错:)我还是删除了博客。.我发现我并不是真正的博客人。
– 0x3h
17年7月6日在5:35
#2 楼
通过错误和我的初始假设扩大答案范围提供的输入字符串“ abcdefgh”的结果将导致“ b + de = f”
提供约束输入字符串z3确实返回了
char“ a”作为第一个可能的model（），这里是经过略微修改的
python脚本，由perror发表在他的答案中/>
:\>cat z3t.py
from z3 import *
s0,s1,s2,s3,s4,s5,s6,s7 = BitVecs( 's0 s1 s2 s3 s4 s5 s6 s7', 8)
v5,v8 = BitVecs ('v5 v8', 16)
v5 = ((s6 + s0 - s7 - s2) & 0xff00) | s1
v8 = s3 + v5 - s4
s = Solver()
s.add(v8 == s5,s0 == ord('a'),s1 == ord('b'),s2 == ord('c'),s3 == ord('d'))
s.add(s4 == ord('e'), s5 > 0x60,s6 == ord('g'),s7 == ord('h'))
s.check()
print chr((s.model()[s5]).as_long())
:\>python .\z3t.py
a
评论
是的，我应该只使用字母数字，您的回答绝对正确且完整……您应该得到我的投票（有时我只是个懒惰的混蛋！
–恐怖
17年7月4日在10:54
评论
我更喜欢disasm而不是这种伪形式，因为我认为算法可能会用movzx丢弃符号位，因此最终将以b + d-e =结果，因此结果将是aie abcdeagh，看看是否有意义br />