Büyük Dil Modelleri (LLM'ler) Biçimsel Yazılım Doğrulamayı Çok Daha Büyük Ölçekte Uygulanabilir Kılıyor

Modern yazılımların büyük çoğunluğu hatalarla (bug) doludur ve günümüzde yapay zeka modelleri bu açıkları kolayca bulup istismar edebilmektedir. Siber saldırılara karşı kullanılan standart savunma mekanizmaları artık tek başına yeterli değildir; kodun hatalardan arınmış olduğunu matematiksel olarak kanıtlayacak yöntemlere ihtiyacımız var. Biçimsel yazılım doğrulama (formal software verification) bu garantiyi sağlayabilse de, tarihsel olarak yıllar süren uzman çabası gerektirdiği için gerçek dünya projelerinin çoğunda uygulanması pratik olmamıştır.

Ancak Theorem iş birliğiyle yürütülen çalışmalar, bu durumun artık değiştiğini gösteriyor: Büyük Dil Modelleri (LLM'ler) artık büyük ölçekte biçimsel kanıtlar üretebiliyor ve kanıtlanmış güvenlik garantileri içeren yeni yazılım geliştirme iş akışlarını mümkün kılıyor. Claude kullanılarak, 100'den fazla gerçek dünya açık kaynaklı yazılım kütüphanesinde assembly kodu (RISC-V) düzeyinde güvenlik özellikleri kanıtlandı. Bu çalışma, üretim yazılımlarına assembly düzeyinde biçimsel doğrulama uygulamak için yapay zekanın kullanıldığı ilk büyük ölçekli girişimi temsil ediyor. Üstelik Claude, bu kanıtları yazarken trilyonlarca test çalışmasına rağmen yıllarca fark edilemeyen gizli hataları da ortaya çıkardı. Model yetenekleri geliştikçe, biçimsel doğrulamanın güvenli yazılım geliştirmenin ayrılmaz bir parçası haline gelmesi bekleniyor.

Bölüm 01: Giriş#

Olgunlaşmış ve yoğun şekilde test edilmiş yazılımlar bile hatalar içerir ve LLM'ler bunları bulmakta giderek ustalaşmaktadır. Bugün dünya çapında milyarlarca cihazda çalışan, en iyi test edilmiş yazılımlardan biri olan Linux çekirdeğinde (kernel) yakın zamanda 1.000'den fazla güvenlik açığı bildirildi. Öncü modellerin görünüşte zararsız hataları birbirine zincirleyerek kritik istismarlara (exploit) dönüştürme yeteneği arttıkça, bu hataları sahada istismar edilmeden önce tespit edip düzeltebilecek tekniklere ihtiyacımız var. İdeal olarak bu teknikler tüm hataları bulup yamamalı ve ardından bulunacak başka hata kalmadığına dair kesin bir kanıt sunmalıdır.

Biçimsel doğrulama, bunu başarmanın yollarından biridir. Bu süreçte geliştiriciler kodlarını matematiksel bir modele dönüştürür ve her zaman tanımlanmış bir dizi güvenlik kuralına uyduğunu kanıtlamaya çalışır. Eğer kanıtlamada başarısız olurlarsa, kodda kuralı ihlal edebilecek bir hata olduğu anlaşılır ve başarısızlığın doğası hatanın ne olabileceğine işaret eder. Her seferinde başarısızlık nedenini ortadan kaldırarak bu süreci tekrarlamak, nihayetinde kodun bu kuralları ihlal edecek hiçbir hata barındırmadığının kanıtını sunar.

Ne var ki biçimsel doğrulama kolay değildir. Kanıtlar orijinal koddan katbekat daha büyük olabilir ve bunları yazmak ciddi bir çaba ile niş, yüksek düzeyde uzmanlaşmış bir beceri seti gerektirir. Örneğin, seL4 işletim sistemi çekirdeğini geliştirmek 2 kişi-yıl sürerken, onu biçimsel olarak doğrulamak 20 kişi-yıl sürmüştür. Bu nedenle biçimsel doğrulama, bugüne kadar yalnızca Airbus'ın aviyonik kodları gibi gerçekten kritik görev uygulamalarında pratik olabilmiştir.

Ancak LLM'ler bu süreci çok daha kolay hale getiriyor. Öncü modeller artık gerçek dünya yazılımları için tamamen otonom bir şekilde doğruluk kanıtları üretebiliyor. Bunu göstermek adına Claude'dan 123 açık kaynaklı kütüphanede yararlı güvenlik özelliklerini kanıtlaması istendi. Buna, bazı çalıştırılabilir çıktıların (executable artifacts) belirli koşullar altında asla çökmeyeceğini göstermek ve programların bellek hatalarını tetiklemeden her zaman normal şekilde sonlanacağını kanıtlamak da dahildi.

Yazılım Geliştirme ve Öğrenme Açısından Pratik Çıkarımlar#

• Testten Kanıta Geçiş: Geleneksel birim ve entegrasyon testleri yalnızca belirli senaryolarda hata olmadığını gösterirken, LLM destekli biçimsel doğrulama kodun hiçbir koşulda belirli kuralları ihlal etmeyeceğini matematiksel olarak garanti eder.
• Güvenlik İş Akışlarının Dönüşümü (Shift-Left): Yapay zeka modelleri saldırganlar tarafından açıkları birleştirmek için kullanılırken, savunma tarafında CI/CD süreçlerine otonom biçimsel doğrulama adımlarının eklenmesi yakın gelecekte standart bir pratik haline gelecektir.
• Maliyet ve Erişilebilirlik: Eskiden yalnızca havacılık veya savunma sanayii gibi devasa bütçeli projelerin karşılayabildiği matematiksel doğrulama maliyetleri, LLM'lerin otonom kanıt üretme yeteneği sayesinde standart açık kaynak ve kurumsal projeler için erişilebilir olmaktadır.
• Geliştirici Yetkinliklerinin Evrimi: Yazılım mühendisleri için karmaşık teorem kanıtlama dillerini sıfırdan yazmak yerine, sistemin uyması gereken güvenlik kurallarını (spesifikasyonları) doğru tanımlama ve yapay zekanın ürettiği kanıtları doğrulama becerisi öne çıkacaktır.