题目下载链接:f2fK9s2c8@1M7q4)9K6b7g2)9J5c8W2)9J5c8Y4u0W2N6X3g2J5M7$3W2F1k6#2)9J5k6h3E0J5i4K6u0r3k6r3!0%4L8X3I4G2j5h3c8Q4x3X3g2H3K9s2m8Q4x3@1k6F1i4K6y4p5y4H3`.`.

这次实验的题目为Reversing.kr网站中的一道题目。

题目要求:

这是一道典型的用户名-序列号形式的题目，序列号已经给出，且用户名的最后一位为p。

通俗讲，就是解方程。比如使用z3解二元一次方程：

z3代码如下:
ipython 交互

z3 难道就只能用来解小学方程吗？当然不是！来看题。

界面有两个输入框，无按钮，直接对GetWindowTextW下断后两次向上回溯即可到达核心逻辑函数，下面为该函数的代码。

username 只有4个字节。
serial 只有11字节，且第serial[5]=='-'。

这段代码量不是很多，只要细心，很快就能找出所有的限制条件。
1、username[0~3]值域为['a','z']
2、username[3] == 'p' //这个是题目给出的条件，非逆向所得。
3、0x0代码片段中有10个方程:

ord是python中的函数，功能是将字符转成对应int。为什么我要这么做呢？从逆向出的代码片段可知，原程序用itow_s将运算值转为文本，然后取文本的最高位和输入的ASCII进行比较，但是运算结果只有一位数，我就直接用加减0x30，其次z3条件里面好像不能有str()这样的函数出现。

[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课