C*, makine denetimli kanıtları C kodunun içine gömerek programlamayı ve doğrulamayı birleştiriyor

Araştırmacılar ne geliştirdi

Bir araştırma ekibi, programcıların biçimsel doğruluk kanıtlarını, bu kanıtların tanımladığı kodun hemen yanına yazabilmesini sağlayan bir C dili uzantısı olan C*'ı önerdi. Yiyuan Cao, Qinxiang Cao, Yingfei Xiong ve Zhenjiang Hu'nun da aralarında bulunduğu bir grup tarafından Nisan 2025'te arXiv'e gönderilen makale, kısa süre önce Hacker News'in ana sayfasında öne çıktı.

Makaleye göre C* iki bileşene dayanıyor. İlki, bir programın tek bir çalışma yerine olası tüm çalışmalardaki davranışı hakkında akıl yürüten sembolik yürütme motoru. İkincisi ise LCF tarzı bir kanıt çekirdeği: yerleşik kanıt araçlarının geleneğindeki küçük, güvenilen bir çekirdek; her teorem, kabul edilmeden önce bu çekirdekten geçmek zorunda. Bu ikisi birlikte, ortamın hem kodun ne yaptığını hem de hakkında belirtilen bir özelliğin gerçekten geçerli olup olmadığını denetlemesini sağlıyor.

Programcılar doğrulamayı neden atlıyor

Biçimsel doğrulama, sistem yazılımında uzun süredir devam eden bir hedef; bu alandaki düşük düzeyli bellek işlemleri ve güvenlik açısından kritik sorumluluklar hataları pahalı hale getiriyor. Ancak yazarların da belirttiği gibi, geleneksel programcılar kendi kodlarını doğrulamaya nadiren katılıyor ve bu durum, doğrulanmış yazılımın geliştirme ve bakım maliyetlerini yükseltiyor.

Makaleye göre engel şurada: programlama ve doğrulama, birbirinden kopuk ortamlarda ve paradigmalar gerçekleşiyor; uygulama C'de ve onun araç zincirinde yaşıyor, kanıtlar ise genellikle başka yerde, ayrı araçlarla ve ayrı zaman çizelgelerinde geliştiriliyor. Bu ayrım erişilebilirliği sınırlıyor ve gerçek zamanlı denetimi imkânsız kılıyor; böylece doğrulama, normal düzenle-derle döngüsünün bir parçası haline hiç gelmiyor.

C* ikisini nasıl harmanlıyor

C*'ın yanıtı, her iki etkinlik için ortak dil olarak C'nin kendisini kullanmak. Programcılar kanıt kodu bloklarını uygulama kodunun yanına gömüyor ve prototip bunları gerçek zamanlı doğrulayarak, iş ilerledikçe geçerli kanıt durumunu etkileşimli olarak güncelliyor. Hedeflenen deneyim, ayrı bir ekibin sonradan yaptığı bir denetimden çok, yazdıkça yanıt veren bir type checker ya da linter'a benziyor.

Kanıt desteği aynı zamanda ifade gücü yüksek ve genişletilebilir olacak şekilde tasarlanmış. Kullanıcılar mantıksal tanımlardan ve teoremlerden oluşan yeniden kullanılabilir kütüphaneler kurabiliyor ve programlanabilir kanıt otomasyonu yazabiliyor; böylece tekrarlanan akıl yürütme kalıplarının her yeni fonksiyon veya modül için elle yeniden inşa edilmesi gerekmiyor.

Neler değerlendirildi

Yazarlar bir prototip uyguladı ve iki cephede test etti. İlk olarak, küçük C programlarından oluşan bir benchmark, makaleye göre C*'ın yaygın C programlama deyimlerinin geniş bir alt kümesini doğrulayabildiğini gösterdi. İkinci olarak, zorlu bir gerçek dünya vaka çalışması olarak, korumalı çekirdek sanal makine hipervizörünün bellek yönetimi mekanizmasının bir parçası olan pKVM'nin buddy allocator'ının attach fonksiyonunu doğruladılar. Yazarlar, C*'ın bu gerçek sistem kodu parçasının gerektirdiği karmaşık akıl yürütmeyi başarıyla yönettiğini bildiriyor.

Neden önemli

Dünyadaki güvenlik açısından kritik altyapımının büyük bölümü — çekirdekler, hipervizörler, sürücüler, gömülü denetleyiciler — C ile yazılıyor ve neredeyse hiçbiri makine denetimli doğruluk garantileriyle teslim edilmiyor. Bu tür garantileri taşıyan yazılımlar tarihsel olarak özel doğrulama uzmanlığı ve ayrı araçlar gerektirmiş; bu da bu pratiği nadir ve pahalı kılıyor.

C* farklı bir dengeye işaret ediyor: kanıtlar uygulamayla aynı dosyada, aynı dilde ve aynı geri bildirim döngüsünde yer alırsa, doğrulama, sonradan eklenen bir uzmanlık dalı olmaktan çıkıp programlamanın rutin bir parçası haline gelebilir. Kanıtlar şimdilik erken aşamada — bir prototip, küçük benchmarklar ve tek bir vaka çalışması — ve makale üretim hazırlığı iddiasında bulunmuyor. Ancak iki kopuk dünyayı köprülemek yerine programlamayı ve doğrulamayı birleştirme yönündeki bu tasarım yönü, doğruluğun yalnızca test edilerek değil, akıl yürütülerek kanıtlanması gereken sistem yazılımı geliştiren herkes için önemli.