Sembolik Yürütme: Matematiksel Temeller, İspat ve SMT Teorisi

Bu yazıda Sembolik Yürütme konusuna öyle kuru kuru “hacker aracı” veya basit bir fuzzer gözüyle bakmayacağız. Olayı biraz daha derinden, tam bir Biçimsel Doğrulama problemi olarak ele alacağız. Yani anlayacağınız, yazılımdaki bir hatayı bulmak aslında matematiksel bir teoremi ispatlamaya (ya da çürütmeye) benziyor [1].

Normal testlerde (Birim Testi vb.) elimizdeki üç beş veriyle programı deneriz, değil mi? Ama biçimsel doğrulamada işler değişiyor; programın tüm olası durumlarını kapsayıp matematiksel olarak “Bu kod sağlam!” diyebiliyoruz.

Sembolik yürütme dediğimiz şey, aslında programın akışındaki her bir yolun, Birinci Dereceden Mantık formülüne çevrilmesinden ibaret. Bu dönüşümü yaptıktan sonra, “Acaba program şu satıra ulaşabilir mi?” veya “Burada bir güvenlik açığı patlar mı?” sorusu, artık bir mantık bulmacasına dönüşüyor. Bilgisayar da bu bulmacayı çözüp cevabı bize veriyor [3].

1. İşin Matematiği ve Durumlar

Programın çalışmasını soyut bir makine gibi düşünelim. Ama bu makineye öyle 5’tir, “admin”dir gibi somut veriler vermiyoruz. Onun yerine $\alpha$ gibi, $\beta + 5$ gibi sembollerle konuşuyoruz. Sembolik yürütmede bir Durum ($S$) dediğimiz şey üç parçadan oluşuyor:

Peki bunlar ne işe yarıyor?

• $\sigma$ (Sembolik Depo): Değişkenlerin o anki matematiksel karşılığı diyebiliriz. Belleğin cebirsel bir fotoğrafını çekmek gibi. Bellekteki her şey girişlere bağlı bir fonksiyon aslında. Mesela: $\sigma = { x \mapsto \alpha, y \mapsto \alpha + \beta, z \mapsto 2\beta }$
• $\pi$ (Yol Kısıtı): “Bu noktaya gelmek için ne olması gerekirdi?” sorusunun cevabı. O ana kadar biriken şartların listesi. Bu kısıtlar sayesinde ihtimalleri daraltıyoruz. Mesela: $\pi = (\alpha > 0) \land (\alpha + \beta \neq 5) \land (2\beta < 100)$
• $pc$ (Program Sayacı): Kodda hangi satırda olduğumuzu gösteren sayaç. Sıradaki işlem neyse onu işaret eder.

Adım Adım İlerleyelim

Bir komut çalıştığında durumumuz $S_i$’den $S_{i+1}$’e geçiyor. Gelin basit bir örnekle bunu canlandıralım:

Kodumuz şu: y = x + 5; if (y > 10) ...

Adım 1: Atama Yapıyoruz

y = x + 5 satırına geldik. Sembolik motor x sembolünü alıyor, matematiksel olarak 5 ekliyor ve y’ye yapıştırıyor. Henüz bir şart yok, o yüzden yol kısıtı ($\pi$) aynı kalıyor.

Adım 2: Yol Ayrımı (Dallanma)

İşte işlerin karıştığı yer! if (y > 10) satırına geldik. Motor bakıyor; durum ($\alpha + 5 > 10$) doğru da olabilir, yanlış da. Ne yapıyor dersiniz? Evreni ikiye bölüyor! Tıpkı bir ağaç gibi dallanıp budaklanıyoruz:

• Evet Dalı: Bu evrende y kesinlikle 10’dan büyük. Bunu şart olarak kenara not ediyoruz. $S_{\text{true}} = (\sigma, \pi \land (\alpha + 5 > 10), pc_{\text{true}})$
• Hayır Dalı: Bu evrende ise tam tersi, y 10’a eşit veya küçük. Bunu da not ediyoruz. $S_{\text{false}} = (\sigma, \pi \land \neg(\alpha + 5 > 10), pc_{\text{false}})$

Bu hikaye program bitene, hata bulunana ya da “Buradan çıkış yok!” denilene kadar devam ediyor.

2. İspat Teorisi: Oraya Gidebilir miyiz?

Bir kod bloğuna (mesela tehlikeli bir fonksiyona) ulaşıp ulaşamayacağımızı ispatlamak, aslında bir Tatmin Edilebilirlik (SAT) problemi. Yani kodun çalışması, matematiksel bir teoremi kanıtlamaya dönüşüyor.

Teoremimiz şu: Bir noktaya ($L$) ancak ve ancak oraya giden tüm şartları ($\pi_L$) sağlayan bir girdi varsa ulaşabiliriz.

Eğer böyle bir girdi ($I$) yoksa, o kod bloğuna ulaşmak matematiksel olarak imkansızdır. Yani orası “Ölü Kod”dur.

Tersten Gidelim: Çelişki ile İspat

Güvenlikçiler olarak genelde “Bu kod sağlam, patlamaz” demek isteriz. Bunu kanıtlamak için de “Ya patlarsa?” diye tersini varsayarız. Mesela assert(x > 0) satırının asla hata vermeyeceğini ispatlamak için çözücüye şunu sorarız:

• Hipotez: assert(x > 0) her zaman doğrudur.
• Sorgu: “Yol buraya kadar geldi VE x 0’dan küçük veya eşit. Böyle bir dünya var mı?” ($\pi_{\text{path}} \land \neg(x > 0)$)

Çözücünün cevabı kaderimizi belirliyor:

• Cevap UNSAT (İmkansız): Korkacak bir şey yok! Hatayı tetikleyen matematiksel bir yol yok. Hipotezimiz doğru, kodumuz o kısım için taş gibi sağlam.
• Cevap SAT (Mümkün): Eyvah! Hipotez yanlış. Çözücü bize hatayı tetikleyen bir değer ($x = -1$ gibi) buldu. İşte bu değer bizim karşı örneğimiz. Siber güvenlikçiler buna ne diyor biliyor musunuz? Exploit! [4]

3. Püf Noktası: BitVector Teorisi ve Modüler Aritmetik

Modern işlemciler matematikteki o sonsuz tamsayılarla uğraşmaz. Onların dünyası sabit bitlerle sınırlıdır. İşte teorik matematikle bilgisayarın ayrıldığı kritik nokta burası. Bu yüzden modellememizi standart sayılarla değil, Modüler Aritmetik ($\mathbb{Z}_{2^n}$) ile yapmalıyız.

Neden mi Önemli? (Overflow Meselesi)

Normal matematikte $x + 1$ her zaman $x$’ten büyüktür, değil mi? Ama bilgisayar dünyasında (mesela 32-bit sayılarda) işler her zaman öyle yürümüyor. Sayı doğrusu bir çember gibi davranıyor.

Gördüğünüz gibi $x + 1$ hop diye $x$’ten küçük oluverdi! İşte bu “taşma” olayları, siber güvenlikteki o meşhur zafiyetlerin çoğunun kaynağı.

Z3 gibi çözücüler bu durumları BitVector Teorisi (QF_BV) ile simüle eder [2]. Yani toplama işlemini $(x+y) \pmod{2^{32}}$ gibi yapar. Eğer biz hala normal tamsayı matematiği kullanırsak, çözücü bu açıkları göremez ve bize “Güvenli” diyerek yanlış rapor verir.

Bir Örnek: Karışık Keygen

Aşağıdaki C koduna bir bakın. Tersine mühendislerin kafasını karıştırmak için bit işlemlerini bolca kullanmışlar. Ama matematik için bu sadece çözülmesi gereken bir denklemden ibaret.

// Hedef: Bu fonksiyonun 1 dönmesini (Başarılı) sağlamak.
int check_password(unsigned int x) {
    // 1. İşlem: Sağa kaydır, XOR yap falan...
    unsigned int y = (x >> 2) ^ 0xAA;
    
    // 2. İşlem: Sonuçla x'i topla.
    // DİKKAT: Burada gizli bir taşma (overflow) olabilir!
    // İşlemci bunu yutar ama matematik affetmez.
    if ((y + x) == 0xDEADBEEF) {
        return 1; // HEDEF
    }
    return 0;
}

Bu karmaşayı çözen Python scripti de aşağıda. Özellikle Python’un devasa sayılarıyla C’nin sınırlı sayıları arasındaki farka dikkat!

from z3 import *

def prove_and_solve():
    # 1. Değişkeni Tanımla
    # 32-bitlik bir kutucuk (BitVec) oluşturuyoruz. Taşmaları simüle edecek.
    x = BitVec('x', 32)

    # 2. Matematiği Kur
    # C kodunu Z3'ün anlayacağı dile çeviriyoruz.
    # LShR: İşaretsiz sağa kaydırma demek.
    y = (LShR(x, 2)) ^ 0xAA

    # 3. Hedefi Belirle
    # (y + x) işlemi 0xDEADBEEF olsun istiyoruz.
    # Z3, "+" işaretini görünce otomatikman modüler aritmetik yapıyor.
    goal_constraint = (y + x) == 0xDEADBEEF

    # 4. Çözücüyü Hazırla
    s = Solver()
    s.add(goal_constraint)

    print("Bakalım çözüm var mı (SAT Check)...")
    
    # 5. Sonuç?
    result = s.check()
    
    if result == sat:
        print("[+] Buldum! Bu yola gidilebilir.")
        m = s.model()
        
        # Çözümü alalım
        solution = m[x].as_long()
        print(f"[+] İşte anahtar (Input): {hex(solution)} ({solution})")
        
        # --- SAĞLAMASINI YAPALIM ---
        # Burası önemli: Python'un sayıları sonsuzdur, taşmaz.
        # Z3'ün bulduğu o taşmalı sonucu Python'da taklit etmek için
        # her işlemden sonra (& 0xFFFFFFFF) maskesiyle kırpmamız lazım.
        
        val_x = solution
        val_y = (val_x >> 2) ^ 0xAA
        
        # Taşmayı simüle et:
        res = (val_y + val_x) & 0xFFFFFFFF 
        
        print(f"[+] Doğrulama: ({hex(val_y)} + {hex(val_x)}) & Mask == {hex(res)}")
        if res == 0xDEADBEEF:
            print("[+] Süper: Model doğru çalışıyor.")
        else:
            print("[-] Hata: Python ile C uyuşmadı galiba.")
            
    else:
        print("[-] UNSAT: Maalesef matematiksel olarak imkansız. Ölü kod bu.")

if __name__ == "__main__":
    prove_and_solve()

4. Baş Belası: Yol Patlaması (Path Explosion)

Sembolik yürütmenin en büyük derdi ne biliyor musunuz? Yol Patlaması.

Şöyle bir döngü düşünün:

for (int i=0; i < N; i++) {
    if (input[i] == 'A') { ... } // Her turda ikiye bölünüyoruz
}

Bu döngüde ihtimaller $2^N$ diye gidiyor. $N=100$ olsa, ortaya çıkan yol sayısı evrendeki atom sayısını geçiyor! Sembolik motor her ayrımda belleği kopyalayıp yeni bir dünya yarattığı için, hem RAM hem de işlemci bir süre sonra “Yeter artık!” diyor.

Peki Çözüm Ne?

• Durum Birleştirme: Farklı yollardan gelip aynı noktada buluşan durumları (mesela bir if-else çıkışını) tek bir formülde birleştiriyoruz. Angr [5] gibi araçlar bunu sıkça kullanır. Yani iki ayrı durumu hafızada tutmak yerine, sembolik bir seçim değişkeni ($c$) ile tek bir paket yapıyoruz: $\pi_{\text{merged}} = (c \rightarrow \pi_1) \land (\neg c \rightarrow \pi_2)$ Bu sayede yol sayısı azalıyor ama çözücüye giden formül biraz “çorba” oluyor, çözmesi zorlaşabiliyor.
• Konkolik Yürütme (Somut + Sembolik): Sadece sembolik gidince kayboluyoruz. O yüzden hibrit takılıyoruz: Konkolik. Programı normal verilerle çalıştırırken (Somut), arkadan sembolik motoru (İzleyici) gönderiyoruz.
  • Somut Yürütme: Dosya işlemleri gibi karışık yerleri hızlıca geçmemizi sağlıyor.
  • Sembolik Motor: Sadece ilginç yol ayrımlarında devreye giriyor. Mevcut yolun şartını tersine çevirip (!condition) yeni bir girdi üretiyor ve programı zorla o yeni yola sokuyor. Bu teknik, DART, SAGE [6] ve KLEE [3] gibi efsane araçların temelini oluşturuyor.

Özetle

Sembolik yürütme, olayı tersten okumaktır. “Girdi verdim ne çıktı?” diye sormaz; “Şu duruma gelmek için ne girmem lazım?” der.

Matematiksel olarak bu bir ters fonksiyon problemidir ($f^{-1}(y)$). Ama programlar çok karmaşık olduğu için normal matematikle çözülmez, CDCL gibi mantıksal çıkarım algoritmalarıyla çözülür [7].

Kaynakça

Meraklısı için bu işin temel taşlarını şuraya bırakıyorum. Derinlemesine dalmak isteyenler için birebir.

• [1] [King76] İşin Başlangıcı: King, J. C. (1976). Symbolic execution and program testing. Bu makale olayın “Anayasası” sayılır.
• [2] [Z3-08] SMT Çözücüler: De Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. Z3’ün kaputunun altını anlatan makale.
• [3] [KLEE08] Pratik Uygulama: Cadar, C. et al. (2008). KLEE. Teoriyi gerçek dünyaya taşıyan devrimsel çalışma.
• [4] [AEG11] Otomatik Hack: Avgerinos, T. et al. (2014). AEG. Matematiği exploit’e çeviren CMU çalışması.
• [5] [Angr16] Modern Araçlar: Shoshitaishvili, R. et al. (2016). Angr. CTF’çilerin gözbebeği.
• [6] [SAGE12] Microsoft’un Sırrı: Godefroid, P. et al. (2012). SAGE. Windows hatalarını bulan efsane araç.
• [7] [CDCL09] Algoritmalar: Biere, A. et al. (2009). Handbook of Satisfiability. İşin matematiksel ispat kitabı.