Rust’ın core ve alloc crate’lerini Coq’a çevirerek biçimsel doğrulama

 (formal.land)
1 puan yazan GN⁺ 2024-05-16 | 1 yorum | WhatsApp'ta paylaş
  • Rust programlarını Coq’a aktaran coq-of-rust, standart kütüphanenin core ve alloc crate’lerini de ele almaya başlayarak primitive fonksiyonlar için Coq tanımlarını elle yazma yükünü azaltıyor
  • Bu iki crate, unsafe ve ileri seviye Rust kodu içeren büyük kod tabanları olduğundan, otomatik çeviri çıktısını derlenebilir ve doğrulanabilir birimler olarak ele almak temel zorluk haline geliyor
  • Çıktılar giriş Rust dosyası bazında bölününce alloc 54 dosya ve 171.783 satıra, core ise 190 dosya ve 592.065 satıra ulaştı; paralel derleme ve hata ayıklama kolaylaştı
  • impl bloklarındaki modül adı çakışmaları, where koşulu bilgileri dahil edilerek azaltıldı; ancak şu anda Coq’ta derlenmeyen dosyalar toplamın %4’ü olarak kalıyor
  • Option::unwrap_or_default örneği, otomatik çeviri tanımı ile basit fonksiyonel tanımın eşdeğerliğini kanıtlayarak kullanma yaklaşımını gösteriyor; bu da hem otomasyona güven hem de kanıt anında kontrol gerektiriyor

Rust standart kütüphanesindeki primitive’lerin ele alınması

  • Formal Land, Rust programlarını Coq biçimsel kanıt sistemine çeviren coq-of-rust üzerinde çalışıyor
  • Önceden, Rust standart kütüphanesinin primitive bileşenlerini ele almak için her fonksiyonun davranışını gösteren ayrı Coq tanımları oluşturmak gerekiyordu
  • Bu yükü azaltmak için Rust’ın core ve alloc crate’leri coq-of-rust ile çevrildi
  • Çeviri sonuçları aşağıdaki yollardan görülebilir

İlk çeviri çalıştırmasının sonuçları

  • coq-of-rust, alloc ve core üzerinde ilk kez çalıştırıldığında, her bir crate’in tamamına karşılık gelen yüz binlerce satırlık iki Coq dosyası üretildi
  • Aracın büyük kod tabanlarında da çalışabildiği doğrulandı, ancak üretilen Coq kodu doğrudan derlenemedi
  • Hatalar seyrek görülüyordu; birkaç bin satırda yaklaşık bir hata düzeyindeydi
  • cloc ölçümüne göre giriş Rust kodunun boyutu şöyleydi
    • alloc: 26.299 satır Rust kodu
    • core: 54.192 satır Rust kodu
  • Çeviri sürecinde makro genişletme gerçekleştiği için gerçek çeviri hedefi özgün satır sayısından daha büyüktür

Üretilen Coq kodunun bölünmesi

  • En büyük değişiklik, coq-of-rust çıktısını her giriş Rust dosyası için bir Coq dosyası olacak şekilde bölmekti
  • Bu bölme, çevirinin tanım sırasına duyarsız ve context-free olması sayesinde mümkün oldu
  • Rust dosyaları arasında genellikle döngüsel bağımlılıklar bulunur ve Coq buna izin vermez; ancak bu çeviri yönteminde dosya bazlı ayırma mümkündür
  • Bölmeden sonra çıktı boyutu şöyle oldu
    • alloc: 54 Coq dosyası, 171.783 satır Coq kodu
    • core: 190 Coq dosyası, 592.065 satır Coq kodu
  • Dosyaların bölünmesiyle üretilen kodda gezinmek ve bakımı kolaylaştı
    • Derlemeyi paralelleştirmek daha kolay
    • Tek tek dosyalara odaklanarak hata ayıklanabilir
    • Derlenmeyen dosyaları hariç tutmak daha kolay
    • Tek dosyalık diff’leri izlemek daha kolay hale geldi

Modül adı çakışmalarının düzeltilmesi ve kalan dosyalar

  • Bazı hatalar, impl bloklarındaki modül adı çakışmalarından kaynaklandı
  • Çözüm, modül adına daha fazla bilgi ekleyerek benzersizliği artırmaktı
    • Önceden eksik olan where koşulu bilgileri dahil edildi
    • Örneğin Mapping<K, V> için Default trait implementasyonunda, hem K hem de V için Default implementasyonu gerektiği koşulu modül adına yansıtılır
  • Şu anda Coq’ta derlenmeyen dosyalar şunlar
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • Bu, tüm dosyaların %4’üne karşılık geliyor
  • Derlenen dosyaların içinde de henüz ele alınmamış Rust bileşenleri aksiyomlaştırılmış durumda; bu nedenle yalnızca bu oranla tüm desteklenmeyen kapsamı değerlendirmek zor

Option::unwrap_or_default çeviri örneği

  • Rust’taki Option::unwrap_or_default, değer Some(x) ise x döndürür, None ise T::default() çağırır
  • coq-of-rust bunu monadic biçimde bir Coq tanımına çevirir
    • Girdi argümanları ve türleri eşleştirir
    • Some dalında tuple field’ını alıp kopyalar
    • None dalında core::default::Default trait’inin default metodunu çağırır
  • Gerçek doğrulamada, otomatik üretilmiş tanım yerine daha basit bir fonksiyonel tanım kullanılır
    • None ise core.simulations.default.Default.default döndürür
    • Some x ise x döndürür
  • Otomatik üretilmiş tanım ile basit tanımın eşdeğer olduğuna dair kanıt CoqOfRust/core/proofs/option.v içinde bulunur
  • Özgün Rust kodu değişirse bu kanıt aracılığıyla değişiklik yakalanır
  • core kütüphanesinin çevirisi otomatik yapıldığı için üretilen tanıma, elle yazılmış tanımdan daha fazla güvenilebilir
  • Bununla birlikte coq-of-rust içinde de hata veya eksiklikler olabileceğinden, kanıt anında kodun geçerli olup olmadığı kontrol edilmelidir

Kalan işler

  • Rust programlarının doğrulanmasında standart kütüphane biçimselleştirmesine duyulan güven artıyor
  • Bir sonraki hedef hâlâ zahmetli olan kanıt sürecini basitleştirmek
  • Özellikle simülasyonun özgün Rust koduyla eşdeğer olduğunu göstermek için şu işler gerekiyor
    • İsim çözümleme
    • Yüksek seviyeli türlerin devreye alınması
    • Yan etkilerin kaldırılması
  • Bu aşamaları ayrı ayrı ele almak gelecekteki iyileştirme yönü olacak

İlgili okumalar

1 yorum

 
GN⁺ 2024-05-16
Hacker News yorumları

  • Gerçekten etkileyici
    Böyle bir otomatik çeviri, güvenilecek şeyi araca kaydırıyor. coq-of-rust’ın kendisi Coq ile değil Rust ile yazılmış olduğundan özyinelemeli yapı epey şaşırtıcı; ancak David A. Wheeler’ın “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0] çalışmasındaki gibi, Ken Thompson’ın Trusting Trust saldırısını ikinci bir derleyiciyle baypas etme yöntemine CompCert tarzı bir yaklaşım eklenirse doğruluk kanıtı mümkün görünüyor
    Doğrulamak için coq-of-rust ile coq-of-rust çeviricisini Rust’tan Coq’a dönüştürmek gerekir; bu çeviri Rust ile yapıldığı için ona güvenmesek bile, Coq içinde istenen doğruluk özellikleri, özellikle Rust programlarını Coq’a çevirirken semantiğin korunduğu kanıtlanabilir
    Makaledeki gibi, üretilen tanımlardan daha işlevsel tanımlar üzerinden kanıt yapmak muhtemelen daha kolay olacağından, standart kütüphanede yapıldığı gibi tanımlar arasında eşdeğerliği kanıtlama sürecinden geçilebilir. Mevcut coq-of-rust çeviricisi, özellikle lib/ [1], 6.350 satır Rust ise, çeviricinin tamamını Coq ile yazıp üretilenle eşdeğer olduğunu kanıtlamak da gerçekçi görünüyor
    Ardından kanıtlanmış Coq sürümü coq-of-rust çeviricisi, Rust ile yazılmış coq-of-rust kaynağı üzerinde çalıştırıldığında, çıkan Coq tanımları başlangıçta kullanılan Rust sürümü coq-of-rust çeviricisinin çıktısıyla eşleşmeli
    Bu arada, böyle işlere endüstri finansmanı gelmesini görmek güzel. Kripto paralara karşı alaycı sayılırım ama o taraftaki doğruluk ihtiyacının Rust, Coq ve tanıdığım yüksek lisans öğrencilerini destekleme gibi ilgi alanlarındaki iyileştirmeleri ittiği de bir gerçek
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • Yazarlardan biriyim; gerçekten de böyle bir prosedür coq-of-rust doğrulaması için iyi bir yöntem olabilir
      Ancak kodun kendisi kısa olsa da, girdi Rust kodunu ayrıştırmak ve tip denetiminden geçirmek için Rust derleyicisine dayanıyor. Dolayısıyla bu kısmı da doğrulamak ya da en azından kanıtsız da olsa biçimsel olarak belirtimlemek gerekir. rustc’nin API’sinin epey büyük ve kararsız olması bir engel, ama yine de güvenilirliği artırmanın bir yolu olabilir
    • Eskiden SPARK Ada ile çalıştığım zamanları hatırlattı. Desteklenen bir Ada hedefi olmayan projelerde, özellikle çok küçük cihazlarda, Ada’yı C’ye dönüştürüp ardından ilgili hedef için derlerdik; bu sayede SPARK tarafında çeşitli statik analizler yapabiliyorduk
      Elbette çıktıların veya dönüştürücünün doğrulanması sorunu ortaya çıkıyordu, ama sonuç C kodu doğrulama amacıyla oldukça okunabilirdi, stili de sınırlıydı ve araca duyulan güven de yüksekti. SPARK statik analizi tüm doğrulama ve onaylama sürecinin bir parçasıydı; testler ve diğer faaliyetler ek güven katmanları sağlıyordu. Genel olarak oldukça iyi işleyen bir yaklaşımdı
    • Kripto paranın bu tür işleri desteklemesinin nedeni yalnızca doğruluk kısıtları değil; bilgisayar bilimine ilgi duyan insanlara büyük miktarda servetin aktarılmış olması da önemli
      O parayı bilgisayar bilimi araştırmalarına harcamaları yalnızca kendi çıkarlarına olduğu için değil, hobileriyle örtüşen bir hayırseverlik faaliyeti olduğu için de oluyor
    • Bu yaklaşımın, ikili dosyayı üretmekte kullanılan Rust derleyicisinin kötü niyetli bir payload enjekte etmesini nasıl engellediğinden emin değilim. A’yı B’ye derleyip B’yi A’ya derledikten sonra ikili dosyaları karşılaştırabilirsiniz gerçi
      Başka bir yaklaşım da kanıt taşıyan kod. Rust derleyicisinin, yürütülebilir çıktıların girdi kaynak kodunun semantiğiyle eşleştiğine dair Coq kanıtını da birlikte üretmesi
      Elbette Rust’ın bir alt kümesi için derleyiciyi, örneğin ödünç alma denetleyicisi veya optimizasyon olmadan belirli bir mimarinin makine koduna yazıp, oradan her şeyi bootstrap etmek de mümkün

  • Coq gibi yarı otomatik tümdengelimli kanıt sistemleriyle baştan sona doğrulanmış programların boyutu küçüktür. Kütüphaneler, kodun birbiriyle etkileşim derecesi daha düşük olduğu için daha kolay olabilir; ancak genel programlar için durum böyle değildir
    Gerçekte, bu yöntemle doğrulanabilir programların boyutundaki artış, tüm programların ortalama boyutundaki artıştan daha yavaş kaldı. Sağlam yazılım doğrulaması, yani belirtimle %100 uyumlu olduğunu göstermek, çekirdek algoritmaların doğruluk kanıtı gibi yerlerde kesinlikle faydalıdır ama iyi ölçeklenmez
    Bu yüzden araştırmanın sağlam olmayan yöntemlere kaydığı bir yön var. %100 garantinin maliyeti, %99,9999 garantinin 10 katı olabilir ve bu olasılık farkı yazılım dışı arıza olasılığından daha küçük hale gelebilir. Fiziksel sistemlerin zaten belirtimle uyumlu olduğu kanıtlanamaz; belirtimin kendisinin gerçeklikle yeterince örtüşmeme olasılığı da vardır

    • Asıl nokta şu: standart kütüphanenin unsafe kısımları ve Rust’ın güvenlik garantileri kanıtlanırsa, yalnızca standart kütüphaneyi kullanan tüm güvenli Rust kodları için bellek güvenliği, veri yarışı olmaması vb. özellikler geçişli olarak kanıtlanabilir
      Yalnızca unsafe kodun doğru olduğunu kanıtlamak, tüm Rust kodunu kanıtlamaktan çok daha az çabayla mümkün. Bu, Rust’ın güvenlik garantileri konuşulurken sıkça dile getirilen “peki unsafe kod ne olacak” eleştirisine bir yanıt oluyor. Rust tip sisteminin tek başına ele almak için yeterince güçlü olmadığı boşluklar, Coq gibi daha güçlü bir sistemle doldurulabilir

  • Bu tür bir girişimde tam anlayamadığım bir nokta var. Kodu Coq'ya elle ya da yarı elle dönüştürmek gerekiyorsa, bu süreçte hata yapma olasılığı biçimsel doğrulamadan elde edilen faydadan çok daha büyük değil mi?
    Başka bir deyişle, kanıtladığımız şeyin hâlâ orijinal kod için geçerli olduğunu nasıl bilebiliriz?

    • Bilemeyiz. Sonuçta donanıma, derleyiciye, spesifikasyona, Coq'nun güvenilir çekirdeğine vb. bir şeye güvenmek gerekir
      Biçimsel doğrulama çoğu zaman hata olasılığını tamamen ortadan kaldırıyormuş gibi tartışılıyor, ama pratikte daha çok hata olasılığını ciddi ölçüde düşürmeye yakındır. Yine de Rust ile Coq arasında otomatik çeviri, güvenilmesi gereken şeyin karmaşıklığını büyük ölçüde azalttığı için elle çeviriye tercih edilmelidir
    • Geçerli bir sınır, ama o kadar da kötü bir sınır değil
      Çoğu durumda çevirideki hata, kanıtı basitçe imkânsız hale getirir. O zaman biri kanıtın neden geçmediğini araştırırken çeviri hatasını bulur
      Asıl sorun, çeviri hatasının orijinal koddaki hatayı tam olarak dengelemesi durumudur. Sistematik bir risk yoksa iki hatanın bu şekilde birbirini silmesi oldukça düşük olasılıklıdır
    • Kod coq-of-rust ile otomatik çevriliyor. Çeviride bir sorun bulunursa coq-of-rust aracında bir kez düzeltilir ve tüm çeviri çıktıları güncellenir

  • İlgilenen okurlara: Bu blog yazısı, aynı blogdaki diğer yazılara göre kripto para ile daha az doğrudan ilgili olduğu için gönderdim; ama orada teknik açıdan daha ilginç pek çok yazı var
    Özellikle son iki yazı, aynı yaklaşımı Rust'a değil Python'a uygulamayı ele alıyor

  • Eskiden biçimsel olarak doğrulanmış bir C derleyicisinde fuzzer'ın hata bulduğuna dair bir ders [1] hatırlıyorum. Bunun nedeni, biçimsel doğrulamanın frontend ve backend'i kapsamamasıydı
    Coq'nun kendisine ya da çeviriye ne kadar güvenilebileceği sorusunun ortaya çıktığını da biliyorum; Rust güncellemeleriyle nasıl senkronize olacağı da soru işareti, ama kusursuz bir biçimsel doğrulama bile baştan sona %100 doğruluk anlamına gelmez
    [1] https://youtu.be/Ux0YnVEaI6A

  • Biçimsel doğrulama uzmanı hiç değilim ama Rust'ın temel kütüphanesi biçimsel olarak doğrulanır ve unsafe kod kullanmazsa, biçimsel olarak doğrulanmış kütüphaneyi kullanan tüm Rust programları bellek işleme açısından fiilen biçimsel doğrulama düzeyinde kaliteye sahip mi olur?

    • Rust'ın güvenliği bug'larla pek ilgili değildir
      Rust'ın kendi “safe” tanımı vardır ve bu, bellek güvenliğinin bir alt kümesi olarak görülebilir. Tamamen güvenli Rust kodunda bile veri yarışları, deadlock'lar, belleğin tükenmesi vb. mümkündür; mantık hatalarından bahsetmiyorum bile
    • Bir ölçüde hayalin bu olduğunu düşünüyorum, ama çok fazla koşul var ve birkaç şeyin yerine oturması gerekiyor
      Birincisi, unsafe Rust'ın semantiğini biçimselleştirmek gerekir. Ralf Jung'un öncü RustBelt[1] çalışması büyük bir ilerlemeydi ama henüz tamamlanmış değil. Özellikle işaretçi kökeni zorlu bir unsur olarak ortaya çıkıyor
      İkincisi, bunun bir parçası olarak borrow checker'ın biçimsel modeline ihtiyaç var. Stacked borrows[2] iyi bir denemeydi ama kusurları var; Tree borrows[3] bunu düzeltebilir, ancak daha incelikli bir şeyin ortaya çıkması da mümkün
      Üçüncüsü, biçimsel bir bellek modeline ihtiyaç var. Bu esas olarak atomik işlemlerin ve senkronizasyonun davranışıyla ilgilidir; dolayısıyla Arc gibi standart kütüphane bileşenleri için çok önemlidir. Rust'ın bellek modelinin C++'a benzemesi ve onunla birlikte çalışması gerektiği geniş ölçüde kabul görüyor, ancak “out of thin air” sorunu ve seqlock gibi eksik özellikler hâlâ duruyor. Linux kernel'ının hâlâ kendi modelini kullanmasının nedenlerinden biri de bu
      Dördüncüsü, güvenlik garantilerinin iyi biçimde bileşime girdiğinin kanıtlanması gerekir. Özellikle unsafe Rust ile yazılmış sound kod ile safe Rust kodu birleştirildiğinde de güvenlik garantisi korunmalıdır. Şimdiye kadar iyi sonuçlar var, ancak tüm sistem için kanıtlanması gerekir
      Beşincisi, böyle bir kanıtın tüm kodlar için geçerli olabilmesi için Rust'ta kalan tüm soundness bug'larının[1] kapatılması gerekir. Bu sorunların çoğu teoriktir ya da ancak saldırgan kodda[5] pratikte önemli hale gelir, bu yüzden ilerleme yavaştır
      Bütün bunlar tamamlandığında bile hâlâ yalnızca kısmi bir garanti olur. Sistemle temas eden yüzeyin muazzam bir kısmı unsafe koda dayanır. Yalnızca saf hesaplama yapıyorsanız belki, ama örneğin grafik arayüz geliştiriyorsanız hâlâ ters gidebilecek çok şey vardır
      Yine de pratik bir ilerleme yolu var ve bu, bugünün güvenlik açıklarıyla dolu sistemlerinin genel durumundan çok daha iyi bir noktaya götürür
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • Rust uzmanı değilim ama core kodunda epey unsafe var gibi görünüyor. Olması da doğal
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      Burada önerilen türden Coq'nun tüm unsafe çağrılarını doğrulayabileceğini sanmıyorum

  • Bu yaklaşımın Aeneas veya RustHornBelt ile nasıl farklılaştığını karşılaştırabilir misiniz? İşaretçiler ve değiştirilebilir ödünç almalar nasıl ele alınıyor?

    • RustHornBelt’in nasıl çalıştığını bilmiyorum. Biz güvenli koda odaklanıyoruz, ancak unsafe bloklar için de “eldeki en iyi çabayla” çeviri üretiyoruz.
      Aeneas ile karşılaştırınca hedefler çok benzer. Çünkü ikisi de etkileşimli teorem kanıtlayıcılarla Rust programlarını doğrulamayı amaçlıyor. Ancak coq-of-rust’ta kanıtın hedefi olan saf işlevsel kod sürümünü elle yazıyoruz ya da tekrar eden bir iş olduğu için GitHub Copilot’tan yardım alarak yazıyoruz ve bunun otomatik çeviri sonucuyla eşdeğer olduğunu kanıtlıyoruz. Aeneas ise işlevsel sürümü doğrudan üretmeyi hedefliyor.
      İşaretçilerin hepsini değiştirilebilir işaretçi, yani * türündeymiş gibi ele alıyoruz. Rust’ın ödünç alma denetleyicisi bilgisini kullanmıyoruz; bu çeviriyi basitleştiriyor ama bedelini kanıt aşamasında ödüyoruz.
      Kanıtta işaretçiler üzerinde akıl yürütmek için, kullanıcının belleğin nasıl kullanılacağına göre tasarlayabileceği özel bir ayırıcı sağlamasına izin veriyoruz. Örneğin program üç global değiştirilebilir değişken kullanıyorsa, belleği üç öğeli bir kayıt olarak ele alabiliriz. Bu öğeler, henüz ayrılmamış durumu göstermek için başlangıçta None olur.
      Bu tekniğin ne kadar ölçekleneceğini henüz bilmiyoruz, ama en azından şimdilik ayrık mantıkla akıl yürütmekten kaçınabiliyoruz. Doğrulamak istediğimiz çoğu programın, özellikle de uygulama tarafındakilerin, nispeten “basit” bir bellek disiplinine sahip olmasını bekliyoruz.

  • Biçimsel doğrulama belirtimleri yazmak, daha karmaşık özellik tabanlı test kullanmaya benziyor mu? Çok basit olmayan programların ötesine geçince özellik tabanlı test yazmak da oldukça zor ve zaman alıcı oluyor.

    • Benzer, ama her zaman aynı değil. Özellik tabanlı testler genellikle sistemin arayüzü, işlev ya da prosedür düzeyi veya daha yüksek bir düzeyde girdinin tanımını belirtir ve çıktının belirli bir özelliği ya da özellik kümesini sağlayıp sağlamadığını test eder.
      Aynı düzeyde biçimsel doğrulama yaparken de oldukça benzer görünebilir. Ancak biçimsel doğrulama araçları daha derine inebilir. Örneğin hesaplamanın içindeki sistem durumu hakkında “bu döngü değişmezi var; bunun her iterasyonda gerçekten korunduğunu kanıtlayabilir miyiz?” veya “bu hesaplama sırasında hiçbir ara hesaplamada asla underflow/overflow oluşmadığını kanıtlayabilir miyiz?” gibi sorulara yanıt verebilir.
      İlki, döngünün çekirdeğini ayrı bir prosedüre çıkarıp çok sayıda ara durumla çalıştırarak değişmezlik özelliğini test ederseniz özellik tabanlı testle de mümkün olabilir. İkincisi ise programı satır satır ayrı çalıştırılabilir hale getirecek kadar aşırı parçalamadığınız sürece çok daha zordur.

  • Böyle bir şeyin mümkün olduğunu bile bilmiyordum.
    Bu tür girişimlerin, çekirdeğe alma sürecinin kritik kısımlarında Rust benimsenmesini hızlandırıp hızlandıramayacağını merak ediyorum.

  • Biri “doğrulama” kavramını çok basitçe açıklayabilir mi? Neden yalnızca bu amaç için Coq gibi başlı başına bir dilin var olduğunu ve bunun daha geniş toplum açısından ne gibi pratik anlamı olduğunu merak ediyorum.