题目本身是个自解压程序，解压出来后需要安装 .NET 框架。exeinfo 查出也是 C# 程序：

运行一下，有个decode按钮，点一下出现一串加密字符，猜测内部对flag进行加密操作：

直接拖进dnSpy，顺着main函数找到关键点：

逻辑比较简单，下几个断点就会发现text就是flag。相当于dat_secret是密文，解了一次密到text就是flag，然后加了个 \0。后面再两个字符交换和异或加密，输出到 label。

然后关于这题，你可以把三个text都动调或者逆向算法解出，但是我想用 z3 写个求 secret 的正向脚本。然后我发现怎么 check 都是 unsat：

我纳闷了，仔细研究了一下这个位操作：

突然意识到我这低级错误，secret 超过 8 位的字节经过左移肯定会溢出，所以 BitVec不应该设置为 8 位。在这里因为最大也就是 12 位，减少计算量可以设置成 12 位。然后 12 位的话会有为大于 8 位的情况，需要再添加 flag 字节必须小于等于 8 位的约束条件，解出来就是正确的 secret 了。