Lean Artık Doğrulanmış Çekirdeklerle Geliyor

Yapay zeka ajanları, yazılımlardaki güvenlik açıklarını bulmakta son derece etkili hale geldi. Bu durum, Lean kanıt asistanının çekirdeği (kanıt denetleyicisi) için de geçerli. Ağustos ayında yayımlanan iki olay sonrası analiz raporu (1 Ağustos ve 24 Ağustos), bu kritik bileşenlerin bile ne kadar dikkatli korunması gerektiğini gösterdi. Buna yanıt olarak Lean ekibi resmi çekirdeği güçlendiriyor, yeni çekirdekler ekliyor ve geliştirmelerinizi harici çekirdeklerle yeniden denetlemeyi kolaylaştıran yeni araçlar inşa ediyor.

Sandbox İçinde Yeniden Denetleme ve Çoklu Çekirdek Desteği#

Lean v4.35.0 sürümü, lake check komutuyla birlikte geliyor. Bu komut, projenizi dışa aktarır ve tüm ek yüklerden arındırılmış resmi Lean çekirdeği olan leanchecker ile yeniden denetler. Tüm süreç güvenli bir sandbox (kum havuzu) içinde çalışır. İstenirse lake check --inadvisably-no-sandbox komutuyla sandbox devre dışı bırakılabilir.

Lean artık dört ek çekirdekle birlikte sunuluyor:

• nanoda
• lean4lean
• con-leche
• con-ron

Geliştirmelerinizi bu çekirdeklerin tamamıyla yeniden denetlemek için lake check --paranoid komutunu kullanabilirsiniz. Bu modda ayrıca, bellek bozulmalarını sessizce yanlış bir yanıt üretmek yerine kontrollü bir durdurmaya (checked abort) dönüştüren, güçlendirilmiş bellek ayırıcıya sahip resmi çekirdek varyantı da çalıştırılır.

Con-leche: Lean ile Yazılmış ve Tutarlılığı Kanıtlanmış İlk Çekirdek#

Con-leche, Lean dilinde yazılmış ve tutarlılığı matematiksel olarak kanıtlanmış ilk Lean çekirdeğidir. Lean FRO'dan Joachim Breitner'in sıkı gözetimi altında Claude (Fable ve Opus) tarafından uygulanmış ve kanıtlanmıştır. Burada "tutarlı" (consistent) ifadesi, Mario Carneiro'nun Lean tip teorisi modelini takip ederek, con-leche tarafından kabul edilen her ortamın küme teorisinde bir modeli olduğu anlamına gelir. Kanıtın kendisi resmi Lean çekirdeği tarafından denetlenir ve modelde kullanılan küme teorisinin tutarlılığını varsayar.

Bu yaklaşım, çekirdek uygulamasındaki programlama hataları gibi koca bir hata sınıfını tamamen ortadan kaldırır. Üstelik bunu performans kaybı olmadan başarır: Tam Mathlib dışa aktarımında con-leche, resmi çekirdeğin komut sayısının 0,69 katını çalıştırır ve sekiz iş parçacığı (thread) kullanarak tüm kütüphaneyi yaklaşık 100 saniyede denetler.

Derleyici Risklerine Karşı Con-ron ve Gelecek Planları#

Con-leche tek başına kurşun geçirmez değildir; çünkü onu derlemek için kullanılan derleyici ve çalışma zamanında (runtime) hatalar bulunabilir. Bu riski en aza indirmek için Joachim, yapay zeka yardımıyla con-leche'yi Rust diline çevirdi ve Rust sürümünün con-leche denetleme algoritmasını birebir karşıladığını kanıtlamak için Aeneas aracını kullandı. Ortaya çıkan bu çekirdeğe con-ron adı verildi.

Buradaki temel mühendislik çıkarımı şudur:

• Con-leche biçimsel bir tutarlılık kanıtına sahip olduğundan, geriye kalan olası hatalar büyük ihtimalle Lean derleyicisinde veya çalışma zamanındadır (bignum kütüphanesi dahil).
• Aynı hatanın hem Lean hem de Rust derleyicisinde veya çalışma zamanında bulunması son derece düşük bir ihtimaldir. Bu nedenle bir kanıtı hem con-leche hem de con-ron ile denetlemek, derleyici kaynaklı hatalara karşı üst düzey koruma sağlar.

Önümüzdeki birkaç ay içinde, resmi C++ çekirdek uygulamasını çok yakından takip eden lean4lean doğrulamasının da tamamlanması ve dağıtımdaki doğrulanmış çekirdek sayısının üçe çıkması bekleniyor. Ayrıca Arthur Adjedj, çekirdek yenileme planı (issue #14977) ve doğrulama süreçlerini basitleştirecek daha sade çekirdekler üzerinde çalışırken, Joachim de yapılan her değişikliğin con-leche kanıtlarıyla uyumlu kalmasını sağlıyor.

Yazılım Geliştirme İçin Pratik Çıkarımlar#

• Çoklu Doğrulama (N-Version Programming): Kritik sistemlerde tek bir doğrulayıcıya güvenmek yerine, farklı dillerde (Lean, Rust, C++) ve farklı çalışma zamanlarında çalışan bağımsız denetleyiciler kullanmak sistem güvenilirliğini katlar.
• İnsan Gözetiminde AI Destekli Geliştirme: Yapay zeka ajanları sadece güvenlik açığı bulmakla kalmayıp, uzman gözetiminde biçimsel olarak doğrulanmış kod üretmek ve diller arası güvenli dönüşüm (Lean'den Rust'a) yapmak için de güçlü bir kaldıraca dönüşmüştür.