5152092425

   遇到一个ctf的逆向题,链接如下:/static2.ichunqiu.com/icq/resources/fileupload/phrackCTF/REVERSE/findkey

打开看发现没有后缀名,拖入文件分析工具看到是pyc,然后反编译pyc得到py源代码,思路还是很清晰的

FileAnalysis->Easy Python Decompiler

接着看代码:

# Embedded file name: findkey
import sys

lookup = [196,
          153,
          149,
          206,
          17,
          221,
          10,
          217,
          167,
          18,
          36,
          135,
          103,
          61,
          111,
          31,
          92,
          152,
          21,
          228,
          105,
          191,
          173,
          41,
          2,
          245,
          23,
          144,
          1,
          246,
          89,
          178,
          182,
          119,
          38,
          85,
          48,
          226,
          165,
          241,
          166,
          214,
          71,
          90,
          151,
          3,
          109,
          169,
          150,
          224,
          69,
          156,
          158,
          57,
          181,
          29,
          200,
          37,
          51,
          252,
          227,
          93,
          65,
          82,
          66,
          80,
          170,
          77,
          49,
          177,
          81,
          94,
          202,
          107,
          25,
          73,
          148,
          98,
          129,
          231,
          212,
          14,
          84,
          121,
          174,
          171,
          64,
          180,
          233,
          74,
          140,
          242,
          75,
          104,
          253,
          44,
          39,
          87,
          86,
          27,
          68,
          22,
          55,
          76,
          35,
          248,
          96,
          5,
          56,
          20,
          161,
          213,
          238,
          220,
          72,
          100,
          247,
          8,
          63,
          249,
          145,
          243,
          155,
          222,
          122,
          32,
          43,
          186,
          0,
          102,
          216,
          126,
          15,
          42,
          115,
          138,
          240,
          147,
          229,
          204,
          117,
          223,
          141,
          159,
          131,
          232,
          124,
          254,
          60,
          116,
          46,
          113,
          79,
          16,
          128,
          6,
          251,
          40,
          205,
          137,
          199,
          83,
          54,
          188,
          19,
          184,
          201,
          110,
          255,
          26,
          91,
          211,
          132,
          160,
          168,
          154,
          185,
          183,
          244,
          78,
          33,
          123,
          28,
          59,
          12,
          210,
          218,
          47,
          163,
          215,
          209,
          108,
          235,
          237,
          118,
          101,
          24,
          234,
          106,
          143,
          88,
          9,
          136,
          95,
          30,
          193,
          176,
          225,
          198,
          197,
          194,
          239,
          134,
          162,
          192,
          11,
          70,
          58,
          187,
          50,
          67,
          236,
          230,
          13,
          99,
          190,
          208,
          207,
          7,
          53,
          219,
          203,
          62,
          114,
          127,
          125,
          164,
          179,
          175,
          112,
          172,
          250,
          133,
          130,
          52,
          189,
          97,
          146,
          34,
          157,
          120,
          195,
          45,
          4,
          142,
          139]
pwda = [188,
        155,
        11,
        58,
        251,
        208,
        204,
        202,
        150,
        120,
        206,
        237,
        114,
        92,
        126,
        6,
        42]
pwdb = [53,
        222,
        230,
        35,
        67,
        248,
        226,
        216,
        17,
        209,
        32,
        2,
        181,
        200,
        171,
        60,
        108]
flag = raw_input('Input your Key:').strip()
if len(flag) != 17:
    print 'Wrong Key!!'
    sys.exit(1)
flag = flag[::-1]
for i in range(0, len(flag)):
    if ord(flag[i]) + pwda[i] & 255 != lookup[i + pwdb[i]]:
        print 'Wrong Key!!'
        sys.exit(1)

print 'Congratulations!!'

首先flag[::-1]的作用是反转输入,然后下面一个逐字判断

解决问题的思路有两种,一个是直接爆破,另一个则是今天要介绍的主角,z3_solver

我也是看某dalao的writeup才知道的,然后就自己试了试。

首先是安装,安装的话pip直接安装不能成功,因为这个会调用vs编译

先去github上clone下代码:/github.com/angr/angr-z3

然后按照提示先生成make文件

python scripts/mk_make.py -x

再然后应该先打开vs2017的命令行工具,然后再执行cmake

cd build
nmake

编译好后如图:

图片.png

按上面的提示,应该把代码写在build\pyhon目录下,不然就把这个目录加入path,这里我用的是第一种方法

最后就是按照正向思路写一份代码就好了,很神奇有木有。

from z3 import *

flag = [BitVec('c%d' % i, 32) for i in range(17)]
lookup = [196,
          153,
          149,
          206,
          17,
          221,
          10,
          217,
          167,
          18,
          36,
          135,
          103,
          61,
          111,
          31,
          92,
          152,
          21,
          228,
          105,
          191,
          173,
          41,
          2,
          245,
          23,
          144,
          1,
          246,
          89,
          178,
          182,
          119,
          38,
          85,
          48,
          226,
          165,
          241,
          166,
          214,
          71,
          90,
          151,
          3,
          109,
          169,
          150,
          224,
          69,
          156,
          158,
          57,
          181,
          29,
          200,
          37,
          51,
          252,
          227,
          93,
          65,
          82,
          66,
          80,
          170,
          77,
          49,
          177,
          81,
          94,
          202,
          107,
          25,
          73,
          148,
          98,
          129,
          231,
          212,
          14,
          84,
          121,
          174,
          171,
          64,
          180,
          233,
          74,
          140,
          242,
          75,
          104,
          253,
          44,
          39,
          87,
          86,
          27,
          68,
          22,
          55,
          76,
          35,
          248,
          96,
          5,
          56,
          20,
          161,
          213,
          238,
          220,
          72,
          100,
          247,
          8,
          63,
          249,
          145,
          243,
          155,
          222,
          122,
          32,
          43,
          186,
          0,
          102,
          216,
          126,
          15,
          42,
          115,
          138,
          240,
          147,
          229,
          204,
          117,
          223,
          141,
          159,
          131,
          232,
          124,
          254,
          60,
          116,
          46,
          113,
          79,
          16,
          128,
          6,
          251,
          40,
          205,
          137,
          199,
          83,
          54,
          188,
          19,
          184,
          201,
          110,
          255,
          26,
          91,
          211,
          132,
          160,
          168,
          154,
          185,
          183,
          244,
          78,
          33,
          123,
          28,
          59,
          12,
          210,
          218,
          47,
          163,
          215,
          209,
          108,
          235,
          237,
          118,
          101,
          24,
          234,
          106,
          143,
          88,
          9,
          136,
          95,
          30,
          193,
          176,
          225,
          198,
          197,
          194,
          239,
          134,
          162,
          192,
          11,
          70,
          58,
          187,
          50,
          67,
          236,
          230,
          13,
          99,
          190,
          208,
          207,
          7,
          53,
          219,
          203,
          62,
          114,
          127,
          125,
          164,
          179,
          175,
          112,
          172,
          250,
          133,
          130,
          52,
          189,
          97,
          146,
          34,
          157,
          120,
          195,
          45,
          4,
          142,
          139]
pwda = [188,
        155,
        11,
        58,
        251,
        208,
        204,
        202,
        150,
        120,
        206,
        237,
        114,
        92,
        126,
        6,
        42]
pwdb = [53,
        222,
        230,
        35,
        67,
        248,
        226,
        216,
        17,
        209,
        32,
        2,
        181,
        200,
        171,
        60,
        108]
solve = Solver()

for i in range(17):
    solve.add(flag[i] >= 32)
    solve.add(flag[i] <= 127)

for i in range(17):
    solve.add((flag[i] + pwda[i]) & (255) == lookup[i + pwdb[i]])

print(solve.check())
if solve.check() == sat:
    m = solve.model()
    res = ""
    for i in range(17):
        res += chr(m[flag[i]].as_long())

    print(res[::-1])

结果我第一次还把key和ans搞反了。

还有一个要注意的是,

flag = [BitVec('c%d' % i, 32) for i in range(17)]

这里不能够直接用IntVec类型,因为后面有位运算,转换成Bit才是正解。

以上。

705-424-4766

这是一篇受密码保护的文章,您需要提供访问密码:

CTF工具集

CTF比赛一般都是使用网络安全常用工具,比如burp、IDA等,但是会有很多大家不常见的工具。这里我列举一些聚合:

/github.com/truongkma/ctf-tools
/github.com/P1kachu/v0lt
/github.com/zardus/ctf-tools

/github.com/TUCTF/Tools