wjh 收录于 Reverse CTF

2021-03-15 2024-02-12 约 1900 字预计阅读 4 分钟 - 次阅读 - 条评论

这是我第一次出题目，感谢师傅们的捧场。

这道题目的标题 FilpGame 其实就是一个 hint，通过搜索我们可以得知

FlipGame，又名点灯游戏，是一个十分有趣的智力游戏：有一行 N 行 N 列的灯，开始时全部是灭的，当你点击其中一盏灯时他的上下左右（若存在的话）状态全部改变，现在要求你以最少地步数，将全部的灯点亮。

转换逻辑

变换代码

这部分内容也可以通过代码中的关键变换语句看到

这个异或属于常见的一种位运算，而当它在这里的时候，起到的作用就是让 0 变成 1,1 变成 0。做到了翻转的功能，而**1 « (15 - v12)**实际上就是让坐标小的来作为数据中的高位，更加贴近一般思路。

最终目标

可以发现，当 data 数组的内容全部都是-1（0xFFFF）的时候，会输出 flag 的信息，所以我们的目标就是让 data 数组中的全部内容都变成 0xFFFF，从之前搜索到的信息，这个时候就可以猜测程序把灯的亮灭（10）都放在了一个一个 int16 的变量中（状态压缩），从而达到节省程序空间的目的。

解题思路

所以我们要解决的就是如何以最少的步数来让全部灯亮起来，并且需要记录操作。这需要一些算法的知识，很多师傅可能卡在了这里，希望各位师傅可以善用搜索来学习。

注意一下，这道题用 dfs 搜索是不可行的，因为 16*16 的规模比较大，用 dfs 的时间是不能够接受的。所以应该用爆破第一层，其余层按上一层的内容推出。

我这里贴一下我生成数据的代码，以及本题的代码。

解题程序

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
#define MAXN 16
#include <cstdio>
#include <cstring>
#include <algorithm>
#include <cstdlib>
#include <ctime>
#include <vector>
using namespace std;
char a[MAXN][MAXN], g[MAXN][MAXN];
int dx[] = { -1, 0, 0, 0, 1 }, dy[] = { 0, 0, -1, 1, 0 }, ans;
vector < pair<int, int> > PathVec;
vector < pair<int, int> > PathAns;
void filp(int y, int x)
{
	PathVec.push_back(make_pair(x, y));
	ans++;
	for (int i = 0; i < 5; i++)
	{
		int nx = x + dx[i], ny = y + dy[i];
		if (0 <= nx && nx < MAXN && 0 <= ny && ny < MAXN) g[ny][nx] ^= 1;
	}
}

int solve()
{
	int min_Ans = 1000;
	for (int i = 0; i < 1 << 16; i++)
	{
		PathVec.clear();
		ans = 0;
		memcpy(g, a, sizeof(a));
		for (int j = 0; j < MAXN; j++)
			if (i >> j & 1) filp(0, j);
		for (int j = 0; j < MAXN - 1; j++)
			for (int k = 0; k < MAXN; k++)
				if (g[j][k] == 0) filp(j + 1, k);
		for (int j = 0; j < MAXN; j++)
			if (g[MAXN - 1][j] == 0) 
				goto next;
		if (min_Ans > ans)
		{
			PathAns.assign(PathVec.begin(), PathVec.end());
			min_Ans = ans;
		}
	next:;
	}
	if (min_Ans == 1000) min_Ans = -1;
	return min_Ans;
}
char ToChar(int x)
{
	if (x >= 10) return x - 10 + 'A';
	return x + '0';
}
int main()
{
	unsigned short data[MAXN] = { 0xBEF5, 0x8BBC, 0xA0E9, 0x7310, 0xD910, 0xA3AD, 0xCCB6, 0x4DDE, 0x344C, 0x3BD6, 0x6711, 0x868F, 0x1C7A, 0x8425, 0x6B0D, 0x1B4C };
	while (true)
	{
		/*
		memset(data, 0, sizeof(data));
		time_t t;
		srand((unsigned)time(&t));
		for (int i = 0; i < MAXN; i++)
		{
			for (int j = 0; j < MAXN; j++)
				data[i] = data[i] << 1 | (rand() % 2);
		}
		*/
		for (int i = 0; i < MAXN; i++)
			for (int j = 0; j < MAXN; j++)
				a[i][j] = data[i] >> (MAXN - 1 - j) & 1;
		int ans = solve();
		if (ans != -1) break;
	}
	for (auto x : PathAns)
	{
		printf("%c%c", ToChar(x.first), ToChar(x.second));
	}
	printf("\n");
	for (int i = 0; i < MAXN; i++)
	{
		printf("0x%X, ", data[i]);
	}

	return 0;
}

2021 年 8 月 14 添加 z3 解法

实际上这道题目还可以用 z3 来求解（使用 ZeroExt 可以让两个不同 btv 的 BitVec 相加）

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
from z3 import *

init_check = [
    [1, 0, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 0, 1],
    [1, 0, 0, 0, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0, 0],
    [1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 1, 0, 1, 0, 0, 1],
    [0, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 0, 0, 0, 0],
    [1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0],
    [1, 0, 1, 0, 0, 0, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1],
    [1, 1, 0, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 1, 0],
    [0, 1, 0, 0, 1, 1, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0],
    [0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 0, 0, 1, 1, 0, 0],
    [0, 0, 1, 1, 1, 0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0],
    [0, 1, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 0, 0, 0, 1],
    [1, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1],
    [0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0],
    [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1],
    [0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 1],
    [0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0]
]

posx = [0, -1, 0, 1, 0]
posy = [0, 0, -1, 0, 1]

solver = Solver()

change = [[BitVec('change%x%x' % (i, j), 1) for j in range(16)] for i in range(16)]

for i in range(16):
    for j in range(16):
        for k in range(5):
            if 0 <= i + posx[k] < 16 and 0 <= j + posy[k] < 16:
                init_check[i][j] ^= (change[i + posx[k]][j + posy[k]])

for i in range(16):
    for j in range(16):
        solver.add(init_check[i][j] == 1)

sum = BitVec('sum', 16)
t = sum
solver.add(sum == 0)
for i in range(16):
    for j in range(16):
        t += ZeroExt(15, change[i][j])

solver.add(t <= 214 // 2)
solver.check()
ans = solver.model()

for i in range(16):
    for j in range(16):
        if ans[change[i][j]] == 1:
            print('%X%X' % (j, i), end='')

题目代码

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
#define MAXN 16
#define MAXS 0x6b
#include <cstdio>
unsigned short a[MAXN] = { 0xBEF5, 0x8BBC, 0xA0E9, 0x7310, 0xD910, 0xA3AD, 0xCCB6, 0x4DDE, 0x344C, 0x3BD6, 0x6711, 0x868F, 0x1C7A, 0x8425, 0x6B0D, 0x1B4C };
int posX = 0, posY = 0;
int dx[] = { -1, 0, 0, 0, 1 }, dy[] = { 0, 0, -1, 1, 0 };
int max_idx = -1;
inline bool check(int x, int y)
{
	return x >= 0 && x < MAXN && y >= 0 && y < MAXN;
}
inline int ToNum(char x)
{
	if ('0' <= x && x <= '9') return x - '0';
	if ('A' <= x && x <= 'Z') return x - 'A' + 10;
	return -1;
}
int main()
{
	printf("Input: ");
	char data[0x200];
	scanf_s("%s", data, 0x200);
	for (int i = 0; data[i]; i++)
	{
		if (i >= MAXS * 2) goto exit;
		if (i & 1) posY = ToNum(data[i]);
		else posX = ToNum(data[i]);
		if (!check(posX, posY)) goto exit;
		if (i & 1)
		{
			int idx = posY * MAXN + posX;
			if (max_idx >= idx) goto exit;
			max_idx = idx;
			for (int j = 0; j < 5; j++)
			{
				int nx = posX + dx[j], ny = posY + dy[j];
				if (check(nx, ny)) a[ny] ^= 1 << (MAXN - nx - 1);
			}
		}
	}
	for (int i = 0; i < MAXN; i++) if (a[i] != 0xFFFF) goto exit;
	printf("right, vnctf{MD5(%s)}\n", data);
	return 0;
exit:
	printf("wrong\n");
	return 0;
}

VNCTF2021 FilpGame