-
-
[原创]BUUCTF逆向题:[ACTF新生赛2020]Universe_final_answer
-
2022-3-27 17:43 8817
-
1.基本信息探查:
1.EXEinfo:
2.运行一下:
2.IDA分析:
1.主函数分析:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 | __int64 __fastcall main( int a1, char * * a2, char * * a3) { __int64 v4; / / [rsp + 0h ] [rbp - A8h] BYREF char v5[ 104 ]; / / [rsp + 20h ] [rbp - 88h ] BYREF unsigned __int64 v6; / / [rsp + 88h ] [rbp - 20h ] v6 = __readfsqword( 0x28u ); __printf_chk( 1LL , "Please give me the key string:" , a3); scanf( "%s" , v5); if ( (unsigned __int8)sub_860(v5) ) { sub_C50(v5, &v4); __printf_chk( 1LL , "Judgement pass! flag is actf{%s_%s}\n" , v5); } else { puts( "False key!" ); } return 0LL ; } |
v5接收输入的值,作为参数调用到sub_860函数里面做运算,很明显只要返回值不为0就可以了,所以sub_860函数是我们要分析的关键函数,但是还有一个点需要注意输出的地方有两个值要输出但是后面只有一个参数。
2.sub_860()函数分析:
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 | bool __fastcall sub_860(char * a1) { int v1; / / ecx int v2; / / esi int v3; / / edx int v4; / / er9 int v5; / / er11 int v6; / / ebp int v7; / / ebx int v8; / / er8 int v9; / / er10 bool result; / / al int v11; / / [rsp + 0h ] [rbp - 38h ] v1 = a1[ 1 ]; v2 = * a1; v3 = a1[ 2 ]; v4 = a1[ 3 ]; v5 = a1[ 4 ]; v6 = a1[ 6 ]; v7 = a1[ 5 ]; v8 = a1[ 7 ]; v9 = a1[ 8 ]; result = 0 ; if ( - 85 * v9 + 58 * v8 + 97 * v6 + v7 + - 45 * v5 + 84 * v4 + 95 * v2 - 20 * v1 + 12 * v3 = = 12613 ) { v11 = a1[ 9 ]; if ( 30 * v11 + - 70 * v9 + - 122 * v6 + - 81 * v7 + - 66 * v5 + - 115 * v4 + - 41 * v3 + - 86 * v1 - 15 * v2 - 30 * v8 = = - 54400 && - 103 * v11 + 120 * v8 + 108 * v7 + 48 * v4 + - 89 * v3 + 78 * v1 - 41 * v2 + 31 * v5 - (v6 << 6 ) - 120 * v9 = = - 10283 && 71 * v6 + (v7 << 7 ) + 99 * v5 + - 111 * v3 + 85 * v1 + 79 * v2 - 30 * v4 - 119 * v8 + 48 * v9 - 16 * v11 = = 22855 && 5 * v11 + 23 * v9 + 122 * v8 + - 19 * v6 + 99 * v7 + - 117 * v5 + - 69 * v3 + 22 * v1 - 98 * v2 + 10 * v4 = = - 2944 && - 54 * v11 + - 23 * v8 + - 82 * v3 + - 85 * v2 + 124 * v1 - 11 * v4 - 8 * v5 - 60 * v7 + 95 * v6 + 100 * v9 = = - 2222 && - 83 * v11 + - 111 * v7 + - 57 * v2 + 41 * v1 + 73 * v3 - 18 * v4 + 26 * v5 + 16 * v6 + 77 * v8 - 63 * v9 = = - 13258 && 81 * v11 + - 48 * v9 + 66 * v8 + - 104 * v6 + - 121 * v7 + 95 * v5 + 85 * v4 + 60 * v3 + - 85 * v2 + 80 * v1 = = - 1559 && 101 * v11 + - 85 * v9 + 7 * v6 + 117 * v7 + - 83 * v5 + - 101 * v4 + 90 * v3 + - 28 * v1 + 18 * v2 - v8 = = 6308 ) { result = 99 * v11 + - 28 * v9 + 5 * v8 + 93 * v6 + - 18 * v7 + - 127 * v5 + 6 * v4 + - 9 * v3 + - 93 * v1 + 58 * v2 = = - 1697 ; } } return result; } |
if里面有一堆等式,我第一个想到就是利用z3约束器求解:
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 | from z3 import * s = Solver() v1 = Int ( 'v1' ) v2 = Int ( 'v2' ) v3 = Int ( 'v3' ) v4 = Int ( 'v4' ) v5 = Int ( 'v5' ) v6 = Int ( 'v6' ) v7 = Int ( 'v7' ) v8 = Int ( 'v8' ) v9 = Int ( 'v9' ) v11 = Int ( 'v11' ) s.add( - 85 * v9 + 58 * v8 + 97 * v6 + v7 + - 45 * v5 + 84 * v4 + 95 * v2 - 20 * v1 + 12 * v3 = = 12613 ) s.add( 30 * v11 + - 70 * v9 + - 122 * v6 + - 81 * v7 + - 66 * v5 + - 115 * v4 + - 41 * v3 + - 86 * v1 - 15 * v2 - 30 * v8 = = - 54400 ) s.add( - 103 * v11 + 120 * v8 + 108 * v7 + 48 * v4 + - 89 * v3 + 78 * v1 - 41 * v2 + 31 * v5 - ( v6 * 64 ) - 120 * v9 = = - 10283 ) s.add( 71 * v6 + (v7 * 128 ) + 99 * v5 + - 111 * v3 + 85 * v1 + 79 * v2 - 30 * v4 - 119 * v8 + 48 * v9 - 16 * v11 = = 22855 ) s.add( 5 * v11 + 23 * v9 + 122 * v8 + - 19 * v6 + 99 * v7 + - 117 * v5 + - 69 * v3 + 22 * v1 - 98 * v2 + 10 * v4 = = - 2944 ) s.add( - 54 * v11 + - 23 * v8 + - 82 * v3 + - 85 * v2 + 124 * v1 - 11 * v4 - 8 * v5 - 60 * v7 + 95 * v6 + 100 * v9 = = - 2222 ) s.add( - 83 * v11 + - 111 * v7 + - 57 * v2 + 41 * v1 + 73 * v3 - 18 * v4 + 26 * v5 + 16 * v6 + 77 * v8 - 63 * v9 = = - 13258 ) s.add( 81 * v11 + - 48 * v9 + 66 * v8 + - 104 * v6 + - 121 * v7 + 95 * v5 + 85 * v4 + 60 * v3 + - 85 * v2 + 80 * v1 = = - 1559 ) s.add( 101 * v11 + - 85 * v9 + 7 * v6 + 117 * v7 + - 83 * v5 + - 101 * v4 + 90 * v3 + - 28 * v1 + 18 * v2 - v8 = = 6308 ) s.add( 99 * v11 + - 28 * v9 + 5 * v8 + 93 * v6 + - 18 * v7 + - 127 * v5 + 6 * v4 + - 9 * v3 + - 93 * v1 + 58 * v2 = = - 1697 ) if s.check() = = sat: result = s.model() print (result) |
重新排列一下:
1 2 | v1 = 48 , v2 = 70 , v3 = 117 , v4 = 82 , v5 = 84 , v6 = 95 , v7 = 121 , v8 = 55 , v9 = 119 , v11 = 64 , |
这里还要注意的地方就是:
这些值都要换回来,之后将它们换成ASCII码值就行:
1 | F0uRTy_7w@ |
这里搞定了但之前主函数还有个问题就是输出的参数有两个,这里的解决方式是,直接运行输入flag看回显:
flag is actf{F0uRTy_7w@_42}
赞赏
他的文章
看原图