Ponce – Symbolic Execution dla “klikaczy”

Osobiście lubię “zwalać” pracę na mój procesor. Zwłaszcza nudne i powtarzalne czynności bo często w nich strzelam babole, które skutkują jeszcze większymi błędami na wyjściu. Fajnym dodatkiem do tego wszystkiego jest sensowna “klikalność” rozwiązania – sensowność rozumiem w ten sposób, że czynność mogę zautomatyzować za pomocą trzech kliklnięć a nie trzydziestu trzech.

Wszystkie wymienione wyżej warunki spełnia Ponce, czyli plugin do IDA’y pozwalający wyklikać sobie zadane zmienne symbolic execution / taint analysis i rozwiązać odpowiednio skonstruowane równanie. W moim mniemaniu jest to bardzo fajne narzędzie do wszelakich zadań CTF które dają się rozwiązać w prosty sposób a brakuje czasu aby to zrobić 🙂

W tym poście przedstawię rozwiązanie zadania rozgrzewkowego RE, z wrześniowego CTF Ekoparty za pomocą Ponce.

Rozwiązanie zadania

Od ogranizatorów otrzymujemy statycznie skompilowaną pod x64 binarkę ELF:

a@b:~/Desktop$ file warmup 
warmup: ELF 64-bit LSB executable, x86-64, version 1 (GNU/Linux), statically linked, for GNU/Linux 2.6.32, BuildID[sha1]=b9e93849cf9889813b7f88f5b7a0609df69bbf48, stripped

Zadanie jest klasycznym problemem do rozwiązania za pomocą symbolic execution – poniżej długi listing zdekompilowanej funkcji:

signed __int64 sub_4009D8()
{
  signed __int64 result; // rax@29

  if ( unk_6CCD62 == aO[0] )
  {
    if ( unk_6CCD72 == a_[0] )
    {
      if ( unk_6CCD6D == aU[0] )
      {
        if ( unk_6CCD67 == aT[0] )
        {
          if ( unk_6CCD69 == a1[0] )
          {
            if ( unk_6CCD63 == asc_4A1725[0] )
            {
              if ( unk_6CCD6C == aJ[0] )
              {
                if ( unk_6CCD65 == aS_0[0] )
                {
                  if ( unk_6CCD68 == asc_4A172B[0] )
                  {
                    if ( unk_6CCD64 == a1[0] )
                    {
                      if ( unk_6CCD6A == aS_0[0] )
                      {
                        if ( unk_6CCD6B == a_[0] )
                        {
                          if ( unk_6CCD66 == a_[0] )
                          {
                            if ( unk_6CCD7A == a_[0] )
                            {
                              if ( unk_6CCD6E == a5[0] )
                              {
                                if ( unk_6CCD6F == aT[0] )
                                {
                                  if ( unk_6CCD70 == a_[0] )
                                  {
                                    if ( unk_6CCD71 == off_4A1731 )
                                    {
                                      if ( unk_6CCD61 == BYTE2(off_4A1731) )
                                      {
                                        if ( unk_6CCD73 == unk_4A1735 )
                                        {
                                          if ( unk_6CCD74 == off_4A1731 )
                                          {
                                            if ( unk_6CCD75 == unk_4A1737 )
                                            {
                                              if ( unk_6CCD76 == unk_4A1739 )
                                              {
                                                if ( unk_6CCD77 == a_[0] )
                                                {
                                                  if ( unk_6CCD78 == aU[0] )
                                                  {
                                                    if ( unk_6CCD79 == off_4A173B )
                                                    {
                                                      if ( unk_6CCD60 == BYTE2(off_4A173B) )
                                                      {
                                                        if ( unk_6CCD7B == unk_4A173F )
                                                        {
                                                          sub_4101B0("valid!");
                                                          result = 1LL;
                                                        }
                                                        else
                                                        {
                                                          result = 0LL;
                                                        }
                                                      }
                                                      else
                                                      {
                                                        result = 0LL;
                                                      }
                                                    }
                                                    else
                                                    {
                                                      result = 0LL;
                                                    }
                                                  }
                                                  else
                                                  {
                                                    result = 0LL;
                                                  }
                                                }
                                                else
                                                {
                                                  result = 0LL;
                                                }
                                              }
                                              else
                                              {
                                                result = 0LL;
                                              }
                                            }
                                            else
                                            {
                                              result = 0LL;
                                            }
                                          }
                                          else
                                          {
                                            result = 0LL;
                                          }
                                        }
                                        else
                                        {
                                          result = 0LL;
                                        }
                                      }
                                      else
                                      {
                                        result = 0LL;
                                      }
                                    }
                                    else
                                    {
                                      result = 0LL;
                                    }
                                  }
                                  else
                                  {
                                    result = 0LL;
                                  }
                                }
                                else
                                {
                                  result = 0LL;
                                }
                              }
                              else
                              {
                                result = 0LL;
                              }
                            }
                            else
                            {
                              result = 0LL;
                            }
                          }
                          else
                          {
                            result = 0LL;
                          }
                        }
                        else
                        {
                          result = 0LL;
                        }
                      }
                      else
                      {
                        result = 0LL;
                      }
                    }
                    else
                    {
                      result = 0LL;
                    }
                  }
                  else
                  {
                    result = 0LL;
                  }
                }
                else
                {
                  result = 0LL;
                }
              }
              else
              {
                result = 0LL;
              }
            }
            else
            {
              result = 0LL;
            }
          }
          else
          {
            result = 0LL;
          }
        }
        else
        {
          result = 0LL;
        }
      }
      else
      {
        result = 0LL;
      }
    }
    else
    {
      result = 0LL;
    }
  }
  else
  {
    result = 0LL;
  }
  return result;
}

Naszym zadaniem jest zlokalizowanie bufora wejściowego i oznaczenie go jako symbolizowanej pamięci. Można to zrobić w prosty sposób, wpisując dowolną wartość i lokalizując ją w pamięci na początku wykonania funkcji sprawdzającej. W moim przypadku inputem będzie EKO{AAAAAAAAAAAAAAAAAAAAAAA}.

Znaleziony bufor rezyduje w pamięci pod adresem 0x06CCD60. Taki adres, wraz z rozmiarem bufora (26) wpisujemy w okienku dialogowym Ponce po wybraniu opcji “Symbolize Memory” (pomarańczowa strzałka, czerwona pokazuje log z Ponce):

Po wskazaniu Ponce co nas interesuje, przechodzimy do dalszego wykonania naszego zadania. Ponce zaznacza na grafie symbolizowane odwołania do pamięci na jasnozielono, wraz z komentarzem.

Ostatnim krokiem jest wyklikanie rozwiązania solvera SMT (i tak do ostatniego znaku flagi 😉 ). W moim wypadku klikam prawym przyciskiem myszy na warunek jaki musi być spełniony, aby przejść do interesującego mnie brancha (czerwona strzałka) i wybieram opcję: SMT -> Solve formula:

W okienku Output pojawią się rozwiązania zadanego równania (na screenie rozwiązanie dla literki “O” z flagi):

Klikając tak kilkanaście razy i składając literki do kupy, naszym oczom ukaże się rozwiązanie zadania: EKO{1s_th1s_ju5t_4_w4rm_up?}.

Leave a Reply

Your email address will not be published. Required fields are marked *