Rust सत्यापन तकनीक को लो-लेवल सिस्टम कोड पर लागू किया गया

 (github.com/verus-lang)
1 पॉइंट द्वारा GN⁺ 2024-05-06 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Verus Rust में लिखे कोड की correctness verify करने वाला tool है। डेवलपर कोड को क्या करना चाहिए, इसे specification के रूप में लिखते हैं, और Verus static रूप से जाँचता है कि executable Rust code हर संभव execution में उस specification को पूरा करता है या नहीं
  • यह runtime checks जोड़ने के बजाय powerful solver का उपयोग करके यह prove करता है कि code सही है, और फिलहाल Rust के केवल एक हिस्से को support करता है
  • कुछ मामलों में यह standard Rust type system से आगे जाकर raw pointer manipulate करने वाले code की correctness भी static रूप से check कर सकता है
  • project actively developed हो रहा है, इसलिए features टूटे हुए या missing हो सकते हैं और documentation भी अभी पूरी नहीं है; users को Zulip पर help माँगने के लिए तैयार रहना पड़ सकता है
  • सीखने और experiment करने के लिए browser-based Verus Playground, installation guide, tutorial और reference, standard library API docs, concurrency code verification guide, examples और tests उपलब्ध हैं

Verus क्या verify करता है

  • Verus Rust code की correctness verify करने वाला tool है
  • डेवलपर code से अपेक्षित behavior को specification के रूप में लिखते हैं
  • Verus static रूप से check करता है कि executable Rust code हर possible execution में हमेशा उस specification को satisfy करता है या नहीं
  • runtime checks जोड़ने के बजाय, यह solver का उपयोग करके prove करता है कि code सही है
  • current support scope Rust का एक subset है, और support scope बढ़ाने पर काम चल रहा है
  • कुछ मामलों में यह standard Rust type system से आगे जाकर, उदाहरण के लिए raw pointer manipulate करने वाले code की correctness को static रूप से verify कर सकता है

development status और उपयोग करते समय सावधानियाँ

  • Verus एक actively developed project है
  • features broken या missing हो सकते हैं
  • documentation अभी complete नहीं है
  • Verus try करने के लिए Zulip पर help माँगने के लिए तैयार रहना पड़ सकता है
  • Verus community ने कई research papers publish किए हैं, और industry व academia के अलग-अलग projects Verus का उपयोग कर रहे हैं
  • संबंधित list publications and projects page पर देखी जा सकती है

शुरू करने का तरीका और development tools

  • browser में Verus try करने के लिए Verus Playground का उपयोग किया जा सकता है
  • अधिक serious development के लिए installation instructions follow करने होंगे
  • सीखना Tutorial and reference से शुरू किया जा सकता है
  • Verus code के लिए automatic formatter verusfmt भी support किया जाता है

documentation और learning resources

examples और community participation

  • Verus उपयोग के examples, documentation के अलावा भी कई starting points देते हैं
    • Publications and projects: Verus का उपयोग करने वाले publications और projects
    • Videos, slides, and exercises: एक-दिन के Verus tutorial के videos, slides और exercises
    • Standalone examples: छोटे और specific tasks में Verus का उपयोग करने वाले standalone examples
    • Small and medium-sized examples: अलग-अलग Verus features दिखाने वाले examples
    • Unit tests: Verus syntax और feature examples वाले tests
  • issue reporting और discussions GitHub या Zulip पर किए जा सकते हैं
  • feature requests और open conversations के लिए GitHub discussions का उपयोग, और existing features के executable bugs के लिए GitHub issues का उपयोग करने की operating approach अपनाई जाती है
  • code contribution करना चाहें तो Contributing to Verus के instructions देखे जा सकते हैं

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2024-05-06
Hacker News रायें

  • Verus से formal verification किया हुआ Kubernetes controller लिखकर देखा
    मूल रूप से “किसी न किसी समय controller cluster को मांगी गई target state में reconcile कर देगा” जैसी liveness property साबित की जा सकती है
    हालांकि target state तेज़ी से बदलने, asynchrony, failures वगैरह को सोचें तो “correctness” को specify करना ही कई subtle पहलू रखता है
    कोड: https://github.com/vmware-research/verifiable-controllers/, संबंधित paper OSDI 2024 में आने वाला है

    • Unit tests से ज़्यादा यह क्या देता है, यह जानना चाहूंगा

  • Verus की ओर एक छोटे stepping stone के तौर पर Rust के debug_assert को preconditions और postconditions पर लगाया जा सकता है
    Rust compiler default रूप से production builds में इन्हें हटा देता है
    Verus tutorial के verification example में requires और ensures से input range और result conditions लिखते हैं, और runtime check version में debug_assert(-16 <= x1), debug_assert(x8 == 8 * x1) की तरह वही conditions execution के दौरान check की जाती हैं

    • अभी Verus syntax की एक समस्या यह है कि पूरे code को procedure macro में wrap करना पड़ता है
      Creusot जैसे दूसरे Rust proof/verification/contract-style design tools attribute-based syntax इस्तेमाल करते हैं, जो आम तौर पर हल्का और Rust-जैसा महसूस होता है
      अच्छा होगा अगर भविष्य के Verus releases में यह तरीका भी संभव हो जाए
    • काश ऐसे assert और लोग इस्तेमाल करें
      documentation tool के रूप में यह शानदार है, और type system व tests को बहुत अच्छी तरह complement करता है
    • "contracts" crate भी आज़मा सकते हैं: https://docs.rs/contracts/latest/contracts/
    • Verus example उस तरीके जैसा है जिसमें मैं Clojure code लिखता हूं
      ज़्यादातर functions में preconditions और postconditions लगाता हूं, और JVM में production build से इन्हें आसानी से हटाने के लिए flag होता है

  • ज़्यादा असली computer science experience न होने के नाते पूछना चाहता हूं: README में “code की correctness verify करता है” में verification और दूसरी जगह कही जाने वाली “proof” में क्या फर्क है?
    computer science/math background मजबूत न रखने वाले working programmer के लिए code के बारे में “proof” सीखने की अच्छी सामग्री भी जानना चाहूंगा
    साथ ही zero-knowledge proof इतना important और relevant क्यों है, यह भी ठीक से समझ नहीं आता। जैसे x.com/ZorpZK जैसी बातें सुनी हैं, लेकिन यह cool क्यों है समझ नहीं आता

    • code verification और functional programming साथ में सीखने के लिए अच्छी सामग्री Software Foundations है: https://softwarefoundations.cis.upenn.edu
      हालांकि Verus और Software Foundations में इस्तेमाल होने वाले Coq के approaches अलग हैं
      Verus SMT solver नाम के automated constraint-solving system से properties को automatically prove करने की कोशिश करता है, जबकि Coq में काफी अधिक हिस्सा manually prove करना पड़ता है और automation सीमित है
      दोनों के अपने pros और cons हैं; automation जब काम करे तो अच्छा है, लेकिन जब न करे तो frustrating होता है
      zero-knowledge proof को कुछ अलग क्षेत्र मानना बेहतर है, और formal verification/proof पर काम करने वाले कई लोग भी zero-knowledge proof को नहीं छूते। इसे cryptographic primitive समझना बेहतर है
    • यहां verification और proof को synonyms की तरह इस्तेमाल किया गया है, और पहले paragraph के बाद वाले हिस्से में यह और साफ हो जाता है
      zero-knowledge proof में overhead ज्यादा है और तथाकथित “killer app” की कमी है, इसलिए practical uses, importance या relevance अभी बहुत बड़ी नहीं है, लेकिन conceptually यह दिलचस्प है
    • इस context में “verification” और “proof” एक ही हैं
      learning resources तो मैं भी चाहता हूं। Dafny docs काफी अच्छे हैं, लेकिन formal software verification अभी non-CS/math PhD वाले ordinary programmers के इस्तेमाल लायक stage तक नहीं पहुंची लगती
      examples देखने पर यह comparatively आसान लगता है, लेकिन जल्द ही “prove नहीं कर सकते” से टकराते हैं, और क्यों ऐसा है इसका जवाब अक्सर ऐसे deep implementation details में चला जाता है जो शायद author ही जानता हो
    • मेरी जानकारी में zero-knowledge proof आपको यह साबित करने देता है कि आप कुछ जानते हैं, बिना उस चीज़ की content reveal किए
      उदाहरण के लिए password server को भेजे बिना भी यह verify किया जा सकता है कि आप password जानते हैं, जिससे malicious server या man-in-the-middle attacker के लिए password चुराकर देखना कठिन होता है
      identity verification में भी यह बेहतर विकल्प दे सकता है। आप prove कर सकते हैं कि आपके पास government-issued ID है, लेकिन document खुद server को नहीं देना पड़ता, इसलिए “अधिकतम 2 साल/3 साल/6 महीने रखेंगे” और आखिर में leak हो जाने वाली स्थितियां कम हो सकती हैं
    • “working programmer code के बारे में proof करता है” यह expression अभी contradiction के करीब लगता है
      code के लिए proofs अभी working programmer का काम नहीं है
      Hoare logic अच्छा starting point है, और introductory computer science classes में भी कभी-कभी पढ़ाया जाता है
      Coq की learning curve steep है, और OCaml या ऐसी भाषा से परिचित न हों तो खास तौर पर और कठिन है। Why3 ज्यादा beginner-friendly हो सकता है: https://www.why3.org
      proof और verification का मतलब एक हो सकता है, लेकिन proof ज्यादा interactive लगता है और verification में model checking या annotations वाले program की SMT solving जैसी automation संभव होने का भाव है

  • अगर किसी को similar projects के बारे में पता नहीं था, तो Dafny एक “verification-aware programming language” है जिसे Rust में compile किया जा सकता है: https://github.com/dafny-lang/dafny

  • वाकई शानदार लगता है। मौजूदा codebase में proofs जोड़ने का तरीका बताने वाली कोई guide या examples हों तो लोगों के लिए उपयोगी होगा
    उदाहरण के लिए, मान लें एक minimal GUI app है जिसमें सिर्फ एक text box है। वह HTTP request से एक ऐसा array लाता है जिसे compile time पर जाना नहीं जा सकता और जिस पर भरोसा नहीं किया जा सकता, फिर उसे bubble sort करके दिखाता है
    bubble sort में off-by-one error की वजह से आखिरी element जस का तस रह जाने जैसा एक जानबूझकर डाला गया bug है, और unit tests किसी वजह से उस bug को पकड़ नहीं पाते। tests अधूरे हैं या नहीं, इसकी चिंता proof की ओर जाने की मुख्य प्रेरणा हो सकती है
    फिर unit tests को proofs से replace करते हुए bug खोजने और ठीक करने की प्रक्रिया दिखाना अच्छा होगा
    proof code को खुद विस्तार से समझाने की जरूरत नहीं है; साबित किए गए mathematical code और साबित न किए गए input/output code की boundary, proof और build के लिए इस्तेमाल होने वाली command line, और खुद आज़माने के लिए zip archive जैसी practical details पर focus करना काफी होगा
    दरअसल standard input से पढ़कर standard output पर लिखना ही शायद पर्याप्त होगा

  • मुख्य contributors में से एक ने Zürich Rust meetup में Verus पर बेहतरीन talk दी थी: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
    यह “ghost” code program के अंदर कितनी साफ-सुथरी तरह फिट बैठता है, यह प्रभावशाली था, और Ada की थोड़ी याद आई

  • सोच रहा हूं कि Rust के लिए भी C/C++, Common Lisp, Ada/SPARK2014 जैसे कोई standards पहले से हैं या नहीं
    अगर ऐसा कुछ नहीं है, तो Ada/SPARK2014 के लिए विकसित verification tools की तुलना में यह moving target बन जाता है
    bare metal से लेकर high-integrity safety-critical applications तक फैली Ada/SPARK2014 की विरासत को भी नजरअंदाज करना मुश्किल है

  • इसके और Kani के बीच क्या relation है, यह जानना चाहता हूं। क्या ये अलग तरह से काम करते हैं?
    https://github.com/model-checking/kani

    • model checkers आम तौर पर सीमित संख्या में states ही explore करते हैं, इसलिए bugs खोजने में efficient होते हैं, और कई बार program में अतिरिक्त annotations की जरूरत भी नहीं होती
      Verus, Dafny, F* और मेरे VCC जैसे automated SMT-based verifiers में लगभग हर function और loop पर annotations लगाने पड़ते हैं, लेकिन ये program correctness के बारे में ज्यादा व्यापक guarantees देते हैं
      Coq या Lean जैसे interactive prover-based tools को आम तौर पर user की ज्यादा guidance चाहिए होती है, लेकिन ये ज्यादा complex properties तक guarantee कर सकते हैं

  • Verus की SPARK से तुलना कैसी है, यह जानना चाहता हूं
    क्या यह उसी general category का verifier है? Ada के बजाय Rust के लिए verifier होने के अलावा Verus किस तरह अलग है?

  • अगर कोई Verus को अच्छी तरह जानता हो तो Verus और Lean4 की performance और expressiveness के अंतर समझा दे तो अच्छा होगा
    मेरी समझ है कि Verus SMT-based verification tool है, और Lean एक interactive prover होने के साथ-साथ SMT-based tool भी है
    हालांकि formal verification field की मेरी समझ सीमित है, इसलिए software formal methods को अच्छी तरह जानने वाले किसी व्यक्ति की राय जानना चाहूंगा

    • Lean, Coq जैसा है
      उदाहरण के लिए Coq की “Software Foundations” किताब की तरह C code के बारे में propositions बनाकर उन्हें prove किया जा सकता है, लेकिन Lean में लगभग कोई ऐसा करता नहीं दिखता और tooling भी कम है
      Lean4 में program लिखकर उस program के बारे में proofs भी किए जा सकते हैं, और कुछ लोग थोड़ा-थोड़ा ऐसा कर रहे हैं
      pure mathematics को formalize करना और उस पर papers publish करना ही फिलहाल Lean4 और Coq का मुख्य उपयोग है
      Lean/Coq वास्तव में जिस तरह की चीजें state और prove कर सकते हैं, वे ज्यादा general हैं, लेकिन real-world programs के लिए शायद इतनी generality हमेशा जरूरी न हो