长安杯 2021fantasy

runwu2204 Lv6
  2023-07-27 21:32:37 2023-07-27 21:32:37 创建   2023-07-27 21:42:26 2023-07-27 21:42:26 更新    

[长安杯 2021]fantasy | NSSCTF

只有一个主类

1
2
3
4
5
6
7
8
9
10
11
12
<?xml version="1.0" encoding="utf-8"?>
<manifest xmlns:android="http://schemas.android.com/apk/res/android" android:versionCode="1" android:versionName="1.0" android:compileSdkVersion="28" android:compileSdkVersionCodename="9" package="com.example.myapplication" platformBuildVersionCode="28" platformBuildVersionName="9">
    <uses-sdk android:minSdkVersion="15" android:targetSdkVersion="28"/>
    <application android:theme="@style/AppTheme" android:label="@string/app_name" android:icon="@mipmap/ic_launcher" android:debuggable="true" android:allowBackup="true" android:supportsRtl="true" android:roundIcon="@mipmap/ic_launcher_round" android:appComponentFactory="android.support.v4.app.CoreComponentFactory">
        <activity android:name="com.example.myapplication.MainActivity">
            <intent-filter>
                <action android:name="android.intent.action.MAIN"/>
                <category android:name="android.intent.category.LAUNCHER"/>
            </intent-filter>
        </activity>
    </application>
</manifest>

mainactivity

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
public boolean check(String to_check) {};//一坨二维数组
    int[][] ahhhhh = {};//一坨数组
    for (int ohh = 0; ohh < 32; ohh++) {
        int thats = 0;
        for (int gooood = 0; gooood < 32; gooood++) {
            int its = to_check.charAt(gooood) & 255;
            for (int so = 0; so < wow[ohh][gooood]; so++) {
                for (int awesome = 0; awesome < its; awesome++) {
                    thats++;
                }
            }
        }
        int ehhh = 0;
        for (int ehh = 0; ehh < 114514; ehh++) {
            ehhh += 114514;
        }
        double deep = 1919810 - ahhhhh[ohh][0];
        double dark = 1919810 - thats;
        double d = ehhh;
        Double.isNaN(deep);
        Double.isNaN(d);
        double fantasy = (114514.0d - Math.sqrt(d - (4.0d * deep))) / 2.0d;
        double d2 = ehhh;
        Double.isNaN(dark);
        Double.isNaN(d2);
        double ah = (Math.sqrt(d2 - (4.0d * dark)) + 114514.0d) / 2.0d;
        if (fantasy + ah != 114514.0d) {
            return false;
        }
    }
    return true;
}

此处条件可以化简

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
for (int ohh = 0; ohh < 32; ohh++) {
    int thats = 0;
    for (int gooood = 0; gooood < 32; gooood++) {
        int its = to_check.charAt(gooood) & 255;
        thats+=wow[ohh][gooood]*its
        }
    }
    int ehhh = 0;
    for (int ehh = 0; ehh < 114514; ehh++) {
        ehhh += 114514;
    }
    double deep = 1919810 - ahhhhh[ohh][0];
    double dark = 1919810 - thats;
    double d = ehhh;
    Double.isNaN(deep);
    Double.isNaN(d);
    double fantasy = (114514.0d - Math.sqrt(d - (4.0d * deep))) / 2.0d;
    double d2 = ehhh;
    Double.isNaN(dark);
    Double.isNaN(d2);
    double ah = (Math.sqrt(d2 - (4.0d * dark)) + 114514.0d) / 2.0d;
    if (fantasy + ah != 114514.0d) {
        return false;
    }

根据结果可以推导

       ah+fantasy=114514
       ((Math.sqrt(d2 - (4.0d * dark)) + 114514.0d)+(114514.0d - Math.sqrt(d - (4.0d * deep))))/2=114514
       (Math.sqrt(d2 - (4.0d * dark))-Math.sqrt(d - (4.0d * deep))=0
       d2 - (4.0d * dark)=d - (4.0d * deep)
       ∵d2=d
       ∴dark=deep
       ∴1919810 - ahhhhh[ohh][0]=1919810 - thats
       ∴thats=ahhhhh[ohh][0]

直接将数组之类的导入z3求解

exp:

此处有个问题就是当我将flag设置为位向量时计算量极大,跑半天跑不出来,在没有位运算且flag有唯一解的时候可以用Int型跑

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
from z3 import*
flag=[Int(f'flag[{i}]')for i in range(32)]
wow =[[89, 88, 60, 91, 74, 111, 84, 96, 111, 124, 102, 95, 106, 126, 80, 122, 55, 125, 57, 32, 61, 96, 98, 106, 36, 113, 79, 86, 43, 71, 91, 117],
[100, 113, 38, 112, 78, 74, 44, 64, 37, 81, 40, 35, 78, 41, 46, 54, 82, 92, 46, 64, 73, 45, 43, 120, 58, 127, 123, 53, 58, 112, 37, 119],
[96, 53, 32, 75, 113, 62, 37, 65, 69, 76, 118, 97, 33, 121, 63, 87, 78, 113, 103, 88, 50, 60, 92, 53, 50, 60, 45, 121, 41, 69, 84, 122],
[82, 125, 67, 38, 112, 121, 118, 74, 48, 37, 108, 42, 59, 112, 85, 41, 103, 75, 34, 89, 37, 74, 124, 40, 62, 36, 114, 127, 91, 51, 110, 63],
[99, 35, 49, 36, 108, 56, 36, 70, 80, 78, 114, 76, 73, 78, 104, 56, 48, 47, 69, 62, 97, 47, 74, 62, 39, 90, 97, 56, 114, 90, 47, 111],
[117, 87, 70, 32, 110, 43, 60, 127, 114, 119, 117, 71, 59, 90, 55, 72, 46, 48, 63, 66, 110, 108, 111, 35, 43, 113, 124, 91, 45, 81, 64, 67],
[64, 114, 50, 54, 94, 60, 127, 81, 92, 101, 78, 91, 68, 72, 95, 92, 48, 91, 34, 37, 77, 62, 74, 122, 75, 37, 127, 66, 90, 86, 67, 115],
[77, 80, 71, 61, 124, 79, 124, 111, 109, 121, 119, 52, 82, 100, 109, 57, 76, 99, 61, 37, 94, 113, 49, 72, 84, 96, 88, 106, 55, 123, 63, 57],
[90, 73, 75, 44, 104, 111, 78, 53, 82, 97, 76, 33, 92, 73, 113, 124, 101, 57, 94, 34, 76, 103, 48, 79, 74, 58, 76, 86, 65, 83, 89, 81],
[78, 100, 109, 36, 83, 98, 109, 98, 39, 73, 61, 94, 32, 107, 59, 84, 100, 86, 95, 43, 75, 78, 70, 73, 85, 99, 121, 91, 116, 65, 78, 64],
[110, 109, 98, 40, 77, 57, 105, 75, 111, 51, 49, 36, 82, 42, 38, 95, 97, 81, 47, 93, 100, 52, 75, 65, 68, 110, 90, 46, 73, 113, 36, 98],
[77, 77, 126, 126, 107, 63, 108, 38, 103, 86, 79, 101, 117, 41, 117, 115, 61, 47, 100, 93, 89, 36, 111, 116, 87, 96, 125, 82, 88, 84, 68, 100],
[57, 53, 84, 116, 104, 127, 48, 115, 99, 124, 70, 92, 101, 120, 39, 125, 60, 127, 45, 76, 66, 66, 78, 71, 114, 104, 61, 33, 95, 123, 75, 75],
[44, 120, 39, 117, 58, 65, 52, 91, 62, 57, 89, 43, 79, 39, 55, 42, 88, 92, 37, 47, 88, 44, 34, 97, 38, 67, 109, 40, 92, 101, 33, 100],
[51, 86, 114, 62, 44, 42, 83, 120, 73, 113, 99, 39, 112, 92, 34, 120, 58, 110, 56, 81, 75, 88, 53, 116, 102, 126, 112, 40, 72, 64, 76, 52],
[110, 34, 95, 67, 35, 56, 38, 84, 124, 103, 49, 70, 105, 122, 125, 38, 97, 71, 49, 122, 104, 126, 112, 113, 65, 70, 80, 105, 97, 74, 123, 46],
[87, 58, 49, 63, 86, 95, 111, 85, 75, 40, 63, 86, 43, 117, 66, 54, 92, 118, 76, 68, 40, 97, 102, 81, 117, 55, 34, 86, 70, 86, 84, 64],
[40, 87, 88, 72, 55, 116, 112, 52, 70, 80, 34, 49, 125, 65, 33, 106, 121, 111, 100, 116, 119, 36, 116, 66, 36, 72, 96, 82, 32, 87, 114, 115],
[34, 43, 121, 56, 88, 116, 75, 90, 92, 110, 89, 115, 115, 103, 100, 72, 42, 84, 116, 40, 115, 84, 68, 125, 92, 37, 47, 116, 110, 40, 124, 38],
[33, 93, 39, 44, 69, 54, 86, 59, 80, 92, 35, 45, 103, 96, 51, 111, 58, 79, 51, 124, 45, 59, 121, 36, 46, 114, 41, 34, 110, 100, 65, 41],
[71, 70, 106, 46, 51, 66, 66, 78, 100, 102, 55, 42, 88, 113, 33, 51, 65, 73, 127, 117, 108, 84, 121, 110, 123, 101, 40, 57, 63, 113, 90, 100],
[72, 86, 41, 125, 49, 67, 63, 127, 52, 106, 77, 49, 63, 70, 84, 87, 99, 63, 39, 122, 105, 62, 46, 123, 108, 127, 40, 89, 83, 79, 48, 62],
[49, 83, 46, 113, 119, 39, 109, 96, 101, 73, 82, 124, 109, 93, 48, 82, 96, 126, 105, 37, 90, 86, 116, 115, 53, 32, 106, 92, 33, 53, 119, 68],
[67, 105, 109, 65, 36, 64, 33, 119, 116, 35, 61, 55, 70, 117, 120, 105, 98, 37, 83, 64, 88, 119, 55, 33, 56, 44, 46, 84, 86, 49, 78, 93],
[34, 97, 100, 33, 71, 109, 71, 93, 104, 39, 70, 53, 96, 109, 119, 73, 58, 111, 122, 125, 91, 66, 70, 75, 43, 42, 48, 85, 62, 97, 94, 97],
[119, 96, 75, 59, 115, 33, 99, 51, 56, 49, 84, 45, 112, 60, 87, 117, 66, 106, 113, 59, 105, 40, 94, 87, 93, 64, 52, 39, 109, 93, 120, 33],
[115, 113, 50, 95, 42, 88, 119, 59, 86, 127, 79, 89, 107, 45, 64, 112, 68, 102, 45, 39, 63, 95, 35, 119, 38, 110, 43, 56, 67, 124, 106, 125],
[78, 83, 98, 86, 50, 68, 73, 52, 49, 97, 60, 84, 54, 118, 91, 100, 44, 97, 97, 96, 127, 79, 94, 77, 76, 118, 49, 111, 87, 125, 73, 77],
[103, 45, 119, 36, 94, 99, 81, 35, 97, 51, 107, 110, 120, 71, 64, 88, 83, 33, 120, 89, 114, 36, 110, 80, 85, 40, 105, 37, 66, 73, 91, 59],
[122, 56, 111, 52, 33, 118, 89, 105, 61, 117, 60, 123, 125, 52, 63, 57, 124, 109, 64, 47, 52, 98, 96, 60, 86, 45, 51, 86, 123, 70, 104, 110],
[51, 127, 85, 43, 79, 44, 118, 89, 78, 95, 87, 103, 33, 44, 102, 100, 40, 40, 55, 58, 43, 76, 115, 81, 68, 123, 69, 48, 66, 74, 83, 119],
[79, 55, 88, 105, 81, 104, 105, 100, 46, 34, 87, 68, 36, 74, 48, 70, 57, 39, 125, 80, 102, 61, 127, 82, 90, 85, 120, 35, 126, 60, 105, 104]]
ahhhhh = [
[195075],[164766],[168447],[176014],
[161107],[175809],[178310],[189827],
[181204],[182314],[168177],[196996],
[185129],[152876],[171067],[185573],
[166900],[184588],[182162],[148593],
[180204],[169933],[182766],[166651],
[178856],[175376],[187367],[182885],
[177145],[189716],[169531],[178924]]
f=Solver()
for ohh in range(32):
    thats=0
    for gooood in range(32):
        thats+=(flag[gooood])*wow[ohh][gooood]
    f.add(thats==ahhhhh[ohh][0])
while(f.check()==sat):
    condition = []
    m = f.model()
    p=""
    for i in range(32):
        p+=chr(int("%s" % (m[flag[i]])))
        condition.append(flag[i]!=int("%s" % (m[flag[i]])))
    print(p)
    f.add(Or(condition))

  • 标题: 长安杯 2021fantasy
  • 作者: runwu2204
  • 创建于 : 2023-07-27 21:32:37
  • 更新于 : 2023-07-27 21:42:26
  • 链接: https://runwu2204.github.io/2023/07/27/CTF WP/Re/安卓/长安杯 2021fantasy/
  • 版权声明: 本文章采用 CC BY-NC-SA 4.0 进行许可。
评论
目录
长安杯 2021fantasy