Rust doğrulama teknolojisi, düşük seviyeli sistem koduna uygulanıyor

 (github.com/verus-lang)
1 puan yazan GN⁺ 2024-05-06 | 1 yorum | WhatsApp'ta paylaş
  • Verus, Rust ile yazılmış kodun doğruluğunu doğrulayan bir araçtır; geliştirici kodun ne yapması gerektiğini bir spesifikasyon olarak yazar, araç da çalıştırılabilir Rust kodunun olası tüm yürütmelerde bu spesifikasyonu karşılayıp karşılamadığını statik olarak kontrol eder
  • Çalışma zamanı denetimleri eklemek yerine güçlü bir çözücü kullanarak kodun doğru olduğunu kanıtlama yaklaşımını kullanır; şu anda Rust’ın yalnızca bir bölümünü destekler
  • Bazı durumlarda, standart Rust tip sisteminin ötesine geçerek raw pointer işleyen kodun doğruluğunu bile statik olarak denetleyebilir
  • Proje aktif olarak geliştirilmektedir; özellikler bozuk ya da eksik olabilir, belgeler de henüz tam değildir. Bu nedenle kullanıcıların Zulip’te yardım istemeye hazır olması gerekir
  • Tarayıcı için Verus Playground, kurulum yönergeleri, öğretici ve referans, standart kütüphane API belgeleri, eşzamanlılık kodu doğrulama rehberi, örnekler ve testler öğrenme ve deneme yolları olarak sunuluyor

Verus’un doğruladıkları

  • Verus, Rust kodunun doğruluğunu doğrulayan bir araçtır
  • Geliştirici, kodun gerçekleştirmesi gereken davranışı bir spesifikasyon olarak yazar
  • Verus, çalıştırılabilir Rust kodunun olası tüm yürütmelerde bu spesifikasyonu her zaman karşılayıp karşılamadığını statik olarak kontrol eder
  • Çalışma zamanı denetimleri eklemek yerine, kodun doğru olduğunu kanıtlamak için bir çözücü kullanır
  • Mevcut destek kapsamı Rust’ın bir alt kümesidir; bu kapsamı genişletme çalışmaları sürmektedir
  • Bazı durumlarda, standart Rust tip sisteminin ötesinde, örneğin raw pointer işleyen kodun doğruluğunu statik olarak doğrulayabilir

Geliştirme durumu ve kullanımda dikkat edilmesi gerekenler

  • Verus aktif olarak geliştirilen bir projedir
  • Özellikler bozuk ya da eksik olabilir
  • Belgeler henüz tam değildir
  • Verus’u denemek istiyorsanız Zulip üzerinde yardım istemeye hazır olmanız gerekir
  • Verus topluluğu çeşitli araştırma makaleleri yayımlamıştır; sanayi ve akademideki farklı projeler Verus’u kullanmaktadır
  • İlgili listeye publications and projects sayfasından ulaşılabilir

Başlama yöntemi ve geliştirme araçları

  • Verus’u tarayıcıda denemek için Verus Playground kullanılabilir
  • Daha ciddi geliştirme için kurulum yönergelerini izlemek gerekir
  • Öğrenmeye Tutorial and reference üzerinden başlanabilir
  • Verus kodu için otomatik biçimlendirici verusfmt de desteklenir

Belgeler ve öğrenme materyalleri

Örnekler ve topluluk katılımı

  • Verus kullanım örnekleri, belgelerin dışında da çeşitli başlangıç noktaları sunar
    • Publications and projects: Verus kullanan yayınlar ve projeler
    • Videos, slides, and exercises: Bir günlük Verus öğreticisinin videoları, slaytları ve alıştırmaları
    • Standalone examples: Küçük ve somut görevlerde Verus kullanımını gösteren bağımsız örnekler
    • Small and medium-sized examples: Çeşitli Verus özelliklerini gösteren örnekler
    • Unit tests: Verus söz dizimi ve özellik örneklerini içeren testler
  • Sorun bildirimleri ve tartışmalar GitHub veya Zulip üzerinden yürütülebilir
  • Özellik istekleri ve açık uçlu sohbetler için GitHub discussions, mevcut özelliklerde yeniden üretilebilir hatalar için ise GitHub issues kullanıldığı bir işleyiş uygulanır
  • Koda katkıda bulunmak isterseniz Contributing to Verus yönergelerine başvurabilirsiniz

İlgili okumalar

1 yorum

 
GN⁺ 2024-05-06
Hacker News yorumları

  • Verus ile biçimsel olarak doğrulanmış Kubernetes controller’ları yazmayı denedim
    Temelde “controller eninde sonunda kümeyi istenen hedef duruma uzlaştırır” gibi liveness özelliklerini kanıtlayabiliyorsunuz
    Ancak hedef durumun hızla değişmesi, asenkronluk, hatalar vb. düşünüldüğünde “doğruluğu” belirtmenin kendisinde bile pek çok incelik var
    Kod: https://github.com/vmware-research/verifiable-controllers/, ilgili makalenin OSDI 2024’te yayımlanması planlanıyor

    • Birim testlerinden daha fazlasını ne şekilde sağladığını merak ediyorum

  • Verus’a doğru küçük bir basamak olarak Rust’ın debug_assert’ini önkoşul ve sonkoşullara ekleyebilirsiniz
    Rust derleyicisi varsayılan olarak production build’lerde bunları kaldırır
    Verus öğreticisindeki doğrulama örneği requires ve ensures ile girdi aralığını ve sonuç koşulunu yazar; runtime kontrol sürümü ise debug_assert(-16 <= x1), debug_assert(x8 == 8 * x1) gibi aynı koşulları çalışma sırasında denetler

    • Mevcut Verus söz diziminin bir sorunu, tüm kodun bir prosedürel makronun içine alınmak zorunda olması
      Creusot gibi diğer Rust kanıtlama/doğrulama/sözleşme tarzı tasarım araçları attribute tabanlı söz dizimi kullanıyor; bu genellikle daha hafif ve Rust’a daha uygun hissettiriyor
      Gelecekteki Verus sürümlerinde bu yaklaşımın da mümkün olması güzel olurdu
    • Bu tür assert kullanımını daha fazla kişinin benimsemesini isterdim
      Harika bir dokümantasyon aracı ve tip sistemi ile testleri çok iyi tamamlıyor
    • "contracts" crate’i de denenebilir: https://docs.rs/contracts/latest/contracts/
    • Verus örneği benim Clojure kodu yazma tarzıma benziyor
      Çoğu fonksiyona önkoşul ve sonkoşul ekliyorum; JVM’de bunları production build’lerde kolayca kaldırmaya yarayan bir flag var

  • Gerçek bilgisayar bilimi deneyimi fazla olmayan biri olarak merak ediyorum: README’deki “kodun doğruluğunu doğrular” ifadesindeki doğrulama ile başka yerlerde söylenen “kanıt” arasında ne fark var?
    Bilgisayar bilimi/matematik geçmişi güçlü olmayan profesyonel bir programcının kod hakkında “kanıt” öğrenmesi için iyi kaynakları da merak ediyorum
    Ayrıca sıfır bilgi kanıtlarının neden bu kadar önemli ve ilgili olduğunu da pek anlamıyorum. Örneğin x.com/ZorpZK gibi şeyleri duydum ama neden havalı olduğunu kavrayamıyorum

    • Kod doğrulama ile fonksiyonel programlamayı birlikte öğrenmek için iyi bir kaynak olarak Software Foundations var: https://softwarefoundations.cis.upenn.edu
      Ancak Verus ile Software Foundations’ta kullanılan Coq’nun yaklaşımları farklı
      Verus, SMT çözücü denen otomatik bir kısıt çözme sistemiyle özellikleri otomatik kanıtlamaya çalışır; Coq’ta ise çok daha fazla kısmı elle kanıtlamak gerekir ve otomasyon sınırlıdır
      İkisinin de artıları ve eksileri var; otomasyon iyi çalıştığında güzeldir ama çalışmadığında sinir bozucudur
      Sıfır bilgi kanıtlarını biraz farklı bir alan olarak görmek daha doğru; biçimsel doğrulama/kanıt işleri yapan birçok kişi bile sıfır bilgi kanıtlarıyla uğraşmaz. Bunu kriptografik bir ilkel öğe olarak düşünmek daha iyi
    • Burada doğrulama ve kanıt eşanlamlı kullanılıyor; ilk paragrafın sonlarına doğru bu daha da netleşiyor
      Sıfır bilgi kanıtları yüksek ek yük getiriyor ve sözde “killer app” eksikliği var; bu yüzden pratik kullanım alanı, önemi ve ilgisi henüz büyük değil, ama kavramsal olarak ilginç
    • Bu bağlamda “doğrulama” ve “kanıt” aynı şey
      Öğrenme kaynakları keşke bende de olsa. Dafny dokümanları oldukça iyi, ancak biçimsel yazılım doğrulama henüz bilgisayar bilimi/matematik doktorası olmayan sıradan programcıların rahatça kullanabileceği aşamaya gelmiş gibi görünmüyor
      Örneklere bakınca nispeten kolay görünüyor ama kısa süre sonra “kanıtlanamıyor” duvarına çarpıyorsunuz; bunun nedenine dair yanıtlar da çoğu zaman yalnızca yazarın bilebileceği derin uygulama ayrıntılarına iniyor
    • Bildiğim kadarıyla sıfır bilgi kanıtları, bir şeyi bildiğinizi, o şeyin içeriğini açığa çıkarmadan kanıtlamanızı sağlar
      Örneğin parolayı sunucuya göndermeden parolayı bildiğiniz doğrulanabilir; böylece kötü niyetli bir sunucunun veya aradaki saldırganın parolayı görüp çalması zorlaşır
      Kimlik doğrulama için de daha iyi seçenekler sunabilir. Devlet tarafından verilmiş bir kimliğe sahip olduğunuzu kanıtlayıp belgenin kendisini sunucuya vermek zorunda kalmazsınız; böylece “en fazla 2 yıl/3 yıl/6 ay saklanıp” sonunda sızdırılma riskleri azalır
    • “Profesyonel programcının kod hakkında kanıt yapması” ifadesinin şimdilik neredeyse çelişki olduğunu düşünüyorum
      Kod hakkında kanıt üretmek henüz profesyonel programcıların yaptığı bir iş değil
      Hoare mantığı iyi bir başlangıç noktasıdır ve giriş seviyesi bilgisayar bilimi derslerinde de bazen öğretilir
      Coq’nun öğrenme eğrisi diktir; OCaml veya benzeri dillere aşina değilseniz özellikle daha da zordur. Why3 yeni başlayanlar için daha dostça olabilir: https://www.why3.org
      Kanıt ve doğrulama aynı anlama gelebilir, ancak kanıt daha etkileşimli bir izlenim verir; doğrulama ise model checking ya da açıklama eklenmiş programların SMT ile çözülmesi gibi otomatikleştirilebilir bir şey hissi verir

  • Benzer projeleri bilmeyenler için, Dafny Rust’a derlenebilen “doğrulama farkındalıklı bir programlama dili”dir: https://github.com/dafny-lang/dafny

  • Gerçekten harika görünüyor. Mevcut bir kod tabanına kanıt eklemenin nasıl yapılacağına dair bir rehber ya da örnekler olsa insanlar için faydalı olur gibi
    Örneğin yalnızca bir metin kutusu olan minimal bir GUI uygulamasının, HTTP isteğiyle derleme zamanında bilinmeyen ve güvenilmeyen bir dizi aldığını, bunu bubble sort ile sıralayıp gösterdiğini düşünelim
    Bubble sort’ta off-by-one hatası nedeniyle son elemanın olduğu gibi kalması türünden kasıtlı bir bug olsun ve birim testleri tesadüfen bu bug’ı yakalayamasın. Testlerin eksik olabileceğinden endişe etmek, kanıta yönelmenin başlıca motivasyonu olabilir
    Ardından birim testlerini kanıtla değiştirirken bug’ı bulup düzeltme sürecini göstermek iyi olurdu
    Kanıt kodunun kendisini ayrıntılı açıklamaya gerek yok; kanıtlanmış matematiksel kod ile kanıtlanmamış giriş/çıkış kodu arasındaki sınır, kanıt ve build için kullanılan komut satırı, elle denenebilecek bir zip arşivi gibi gerçekçi ayrıntılara odaklanmak yeterli olur
    Aslında standart girdiden okuyup standart çıktıya yazmak bile yeterli olabilir

  • Başlıca katkı verenlerden biri Zürich Rust buluşmasında Verus hakkında mükemmel bir sunum yaptı: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
    Bu “ghost” kodun programın içine ne kadar temiz oturduğu etkileyiciydi; biraz Ada’yı hatırlattı

  • Rust’ta da C/C++, Common Lisp, Ada/SPARK2014 gibi bir standart zaten var mı merak ediyorum
    Eğer yoksa, Ada/SPARK2014 için geliştirilmiş doğrulama araçlarıyla karşılaştırıldığında hareketli bir hedef oluyor
    Bare metal’den yüksek bütünlük gerektiren güvenlik-kritik uygulamalara uzanan Ada/SPARK2014 mirasını da göz ardı etmek zor

  • Bununla Kani arasında nasıl bir ilişki var merak ediyorum. Farklı mı çalışıyorlar?
    https://github.com/model-checking/kani

    • Model denetleyiciler genellikle yalnızca sınırlı sayıda durumu araştırır; bu yüzden bug bulmada etkilidirler ve çoğu zaman programa ek açıklama gerektirmezler
      Verus, Dafny, F* ve benim VCC’m gibi otomatik SMT tabanlı doğrulayıcılar neredeyse her fonksiyona ve döngüye açıklama eklemeyi gerektirir, ancak program doğruluğu hakkında daha geniş güvenceler sağlar
      Coq veya Lean gibi etkileşimli kanıtlayıcı tabanlı araçlar genellikle kullanıcıdan daha fazla yönlendirme ister, ama daha karmaşık özellikleri de garanti edebilir

  • Verus’un SPARK ile nasıl karşılaştırıldığını merak ediyorum
    Aynı genel doğrulayıcı sınıfına mı giriyor? Ada için değil Rust için bir doğrulayıcı olması dışında Verus nasıl farklı?

  • Verus’u iyi bilen biri Verus ile Lean4 arasındaki performans ve ifade gücü farklarını açıklayabilirse iyi olur
    Verus’un SMT tabanlı bir doğrulama aracı, Lean’in ise hem etkileşimli bir kanıtlayıcı hem de SMT tabanlı bir araç olduğunu anlıyorum
    Ancak biçimsel doğrulama alanına dair anlayışım sınırlı; bu yüzden yazılım biçimsel yöntemlerini iyi bilen birinin görüşünü merak ediyorum

    • Lean, Coq’a benzer
      Örneğin Coq’un “Software Foundations” kitabındaki gibi C kodu hakkında önermeler kurup bunları kanıtlayabilirsiniz, ama Lean ile bunu neredeyse kimse yapmıyor gibi ve araçlar da yetersiz
      Lean4 ile program yazıp o program hakkında kanıtlar da oluşturabilirsiniz; bunu küçük küçük yapan bazıları var
      Saf matematiği biçimselleştirmek ve bunun üzerine makale yayımlamak, şu anda Lean4 ve Coq’un başlıca kullanım biçimi
      Lean/Coq’un gerçekten ifade edip kanıtlayabildiği şeylerin türü daha genel, ancak gerçek dünya programları için bu kadar genellik şart olmayabilir