TCTF-Elements

By xia0

TCTF-Elements

这道题其实是一个数学问题,当时没有做出来,解题过程中走了很多弯路,踩了很多坑,不过也补了很多知识。

Elements

下面是main函数伪代码

signed __int64 __fastcall main(__int64 a1, char **a2, char **a3)
{
  char v3; // bl
  const __int32_t **v4; // rax
  char *v5; // rcx
  size_t v6; // rcx
  signed __int64 result; // rax
  char *v8; // r12
  signed __int64 v9; // r14
  char v10; // bl
  signed __int64 v11; // rax
  const unsigned __int16 *v12; // rcx
  signed __int64 v13; // rdx
  __int64 v14; // rsi
  unsigned __int16 v15; // bx
  signed __int64 v16; // rsi
  __m128i v17; // xmm0
  char *v18; // rax
  double v19; // xmm2_8
  double v20; // xmm0_8
  double v21; // xmm2_8
  double v22; // xmm3_8
  double v23; // [rsp+20h] [rbp-148h]
  double v24; // [rsp+28h] [rbp-140h]
  double v25; // [rsp+30h] [rbp-138h]
  char s[8]; // [rsp+40h] [rbp-128h]
  char v27; // [rsp+6Bh] [rbp-FDh]

  fgets(s, 256, stdin);
  v3 = s[0];
  if ( s[0] )
  {
    v4 = __ctype_tolower_loc();
    v5 = &s[1];
    do
    {
      *(v5 - 1) = (*v4)[v3];
      v3 = *v5++;
    }
    while ( v3 );
  }
  v6 = strlen(s);
  result = 0LL;
  if ( v6 >= 0x2C && (*(_QWORD *)s & 0xFFFFFFFFFFLL) == 530015415398LL && v27 == 125 )
  {
    v27 = 0;
    v8 = strtok(&s[5], "-");
    v9 = 0LL;
    if ( v8 )
    {
      while ( strlen(v8) == 12 )
      {
        v10 = *v8;
        v11 = 0LL;
        if ( *v8 )
        {
          v12 = *__ctype_b_loc();
          v13 = 1LL;
          v11 = 0LL;
          do
          {
            v14 = v10;
            v15 = v12[v10];
            if ( (char)v14 <= 102 && v15 & 0x400 )
            {
              v16 = v14 - 87;
            }
            else
            {
              if ( !(v15 & 0x800) )
                goto LABEL_31;
              v16 = v14 - 48;
            }
            v11 = v16 | 16 * v11;
            if ( v13 > 11 )
              break;
            v10 = v8[v13++];
          }
          while ( v10 );
        }
        if ( !v9 && v11 != 62791383142154LL )
          break;
        v17 = (__m128i)_mm_sub_pd(
                         (__m128d)_mm_unpacklo_epi32((__m128i)(unsigned __int64)v11, (__m128i)xmmword_400BD0),
                         (__m128d)xmmword_400BE0);
        *(&v23 + v9++) = COERCE_DOUBLE(_mm_shuffle_epi32(v17, 78)) + *(double *)v17.m128i_i64;
        v18 = strtok(0LL, "-");
        v8 = v18;
        if ( v9 > 2 || !v18 )
        {
          if ( v24 <= v23 || v25 <= v24 || v23 + v24 <= v25 )
            break;
          v19 = v24 * v24 + v23 * v23 - v25 * v25;
          v20 = sqrt(4.0 * v23 * v23 * v24 * v24 - v19 * v19) * 0.25;
          v21 = (v20 + v20) / (v23 + v24 + v25) + -1.940035480806554e13;
          if ( v21 < 0.00001 && v21 > -0.00001 )
          {
            v22 = v23 * v24 * v25 / (v20 * 4.0) + -4.777053952827391e13;
            if ( v22 < 0.00001 && v22 > -0.00001 )
              puts("Congratz, input is your flag");
          }
          return 0LL;
        }
      }
    }
LABEL_31:
    result = 0xFFFFFFFFLL;
  }
  return result;
}

这个题整个逻辑很清晰,前面一部分对输入的字符串做了一些格式和字符数量判断。

分析可得到需要输入以下格式flag{xxxxxxxxxxxx-xxxxxxxxxxxx-xxxxxxxxxxxx}

这里通过-分割成三个部分,其中第一部分是已知的391bc2164f0a,后面就是程序验证逻辑

          if ( v24 <= v23 || v25 <= v24 || v23 + v24 <= v25 )
            break;
          v19 = v24 * v24 + v23 * v23 - v25 * v25;
          v20 = sqrt(4.0 * v23 * v23 * v24 * v24 - v19 * v19) * 0.25;
          v21 = (v20 + v20) / (v23 + v24 + v25) + -1.940035480806554e13;
          if ( v21 < 0.00001 && v21 > -0.00001 )
          {
            v22 = v23 * v24 * v25 / (v20 * 4.0) + -4.777053952827391e13;
            if ( v22 < 0.00001 && v22 > -0.00001 )
              puts("Congratz, input is your flag");
          }

当时一看其实就知道是一个三角形相关的运算,整理可得以下表达式

$c>b,b>a,a+b>c$

$p=\frac{\sqrt{4a^2b^2-(a^2+b^2-c^2)^2)}}{2(a+b+c)}-1.940035480806554e13$

$q=\frac{abc}{(\sqrt{4a^2b^2-(a^2+b^2-c^2)^2})}-4.777053952827391e13$

$-0.00001<p<0.00001,-0.00001<q<0.00001 $

但并没有看出来是三角形内外圆的半径公式,所以想着直接上约束求解器z3

from z3 import *
x = Real('x')
y = Real('y')
z = Real('z')

m = Real('m')
n = Real('n')

p = Real('p')
q = Real('q')

solver = Solver()

m = x*x+y*y-z*z
n = (4.0*x*x*y*y-m*m)**0.5*0.25
p = 2*n/(x+y+z) + (-1.940035480806554296875E13)
q = x*y*z/(4.0*n) + (-4.777053952827391e13)

solver.add(z > y)
solver.add(y > x)
solver.add(x + y > z)
solver.add(p > -100,p<100)
solver.add(q > -100,q<100)
solver.add(x == 6.2791383142154e13)

if solver.check() == sat:
    print(solver.model())
else:
    print('unsolve')

结果求解了很久z3解不出来,后来才知道z3不能求解该类问题。z3文档中有提及只能解决非线性多项式约束,导致花了很长时间在思考是不是脚本的问题。然后用wolframalpha去求解也没有结果(目前还不清楚原因

下来思考了很久才知道是求解三角形的内外半径,通过内外圆的性质得到如下公式

$$Rr=\frac{abc}{2(a+b+c)}$$

$$tan\frac{C}{2} = \frac{2r}{a+b-c} = \frac{sinC}{1+cosC}$$

这里$sinC,cosC,R,r,c$都是已知的

所以联立能得到$$a=7.0802074077033E13,b=9.5523798483318E13 $$

得到对应的浮点数表示4064e4798769,56e0de138176

movq    xmm0, rax
punpckldq xmm0, xmmword ptr cs:qword_400BD0
subpd   xmm0, cs:xmmword_400BE0
pshufd  xmm1, xmm0, 4Eh
addpd   xmm1, xmm0
movlpd  [rsp+r14*8+168h+var_148], xmm1

在这里需要逆向求解出rax的值,即flag后面两部分。刚开始在这里卡了一下,感觉求解不出来。后面观察到qword_400BD0和xmmword_400BE0这两个数十分特殊

qword_400BD0=0x4530000043300000
xmmword_400BE0=0x45300000000000004330000000000000

punpckldq指令会将qword_400BD0和rax分成两部分组合,这里恰好qword_400BD0为浮点数的阶数部分,rax为尾数部分

然后再分别与4530000000000000,4330000000000000相减。特殊在于这两个数阶数和上面对应相等,尾数部分为0,倒是相减结果又变回原始值。

所以其实这里的变换等于没有变换。

所以三个边长分别等于391bc2164f0a,4064e4798769,56e0de138176

最后的flag=flag{391bc2164f0a-4064e4798769-56e0de138176}

补充:浮点数表示、运算、指令

浮点数有单精度和双精度之分,float占4个字节,double占8个字节

在表示小数的时候采用类比科学计数法的方法,把二进制小数转换为2为底的指数表示$V=(-1)^sM2^E$

e等于向左或向右移动到1为止的个数

比如:12.25 对应二进制:1100.01 这里需要向右移动三位$1.10001*2^3$

下面以float表示12.25这个数,分为三部分,符号位(1位)、指数(8位)、尾数(23位)

符号位0,指数3,尾数10001(第一位默认为1不需要表示)

由于指数也有负指数,所以其实还需要一位表示符号位, IEEE规定,小于01111111的指数位为负数

其实这里可以理解为首位表示符号位,这样的话采用如下计算出float指数部分表示10000000+11-1=10000010

最后12.15单精度浮点数表示为:0 10000010 10001000000000000000000

十六进制:0x41440000 内存中小端表示:00 00 44 41

Float/Double 符号位 指数 尾数 示例 16进制
Float 1位 8位 23位 0 10000010 10001000000000000000000 41440000
Double 1位 11位 52位 0 10000000010 1000100000000000000000000000 000000000000000000000000 4028800000000000

特殊的数表示:当全指数尾数全为0时,表示最小的数,这里定义为0;当指数全为1,尾数全为0时,表示最大的数,这里定义为无穷。

在线转换http://www.binaryconvert.com/

浮点数在进行加减运算的时候需要先对阶然后尾数部分运算

浮点数指令查询https://asm.inightmare.org/opcodelst/index.php

这里解释下pshufd xmm1, xmm0, 4Eh指令

pshufd可以按照指定的方式重新排列数据

这里4E二进制01 00 11 10

寄存器
xmm0 42cc8d80 00000000 41e842c9 e1400000
4E 01 00 11 10
xmm1 41e842c9 e1400000 42cc8d80 00000000