Rust के core और alloc crates को Coq में अनुवाद कर औपचारिक सत्यापन

 (formal.land)
1 पॉइंट द्वारा GN⁺ 2024-05-16 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Rust प्रोग्रामों को Coq में ले जाने वाला coq-of-rust अब standard library के core·alloc crates तक संभालने लगा है, जिससे primitive functions के लिए अलग-अलग Coq definitions हाथ से लिखने का बोझ कम हुआ है
  • ये दोनों crates unsafe और उन्नत Rust कोड से भरे बड़े codebase हैं, इसलिए स्वचालित अनुवाद के नतीजों को compile और verify किए जा सकने वाले units में संभालना मुख्य चुनौती बन गया
  • आउटपुट को input Rust file के आधार पर बाँटने के बाद alloc 54 files और 171,783 lines, तथा core 190 files और 592,065 lines का हो गया, जिससे parallel compilation और debugging आसान हुई
  • impl blocks में module name collisions को where clause की जानकारी शामिल करके कम किया गया, लेकिन अभी भी कुल files में से 4% ऐसे हैं जो Coq में compile नहीं होते
  • Option::unwrap_or_default का उदाहरण इस तरह इस्तेमाल किया गया कि स्वचालित अनुवादित definition और एक सरल functional definition की समानता सिद्ध की जाए; इसके लिए automation पर भरोसे और proof समय की जाँच, दोनों की ज़रूरत है

Rust standard library में primitive handling

  • Formal Land, Rust प्रोग्रामों को Coq formal proof system में अनुवाद करने वाला coq-of-rust विकसित कर रहा है
  • पहले Rust standard library के primitive components को संभालने के लिए हर function के व्यवहार को दर्शाने वाली Coq definition अलग से बनानी पड़ती थी
    • उदाहरण: Option::unwrap_or_default
    • हाथ से लिखी definitions दोहराव वाली होती थीं और उनमें गलती आना आसान था
  • इस बोझ को घटाने के लिए Rust के core और alloc crates को coq-of-rust से अनुवादित किया गया
  • अनुवाद के नतीजे इन paths पर देखे जा सकते हैं

शुरुआती translation run के नतीजे

  • coq-of-rust को alloc और core पर पहली बार चलाने पर, हर crate के पूरे हिस्से के लिए लाखों के करीब lines वाले Coq files 2 बने
  • इससे यह तो साबित हुआ कि tool बड़े codebase पर चल सकता है, लेकिन बना हुआ Coq code तुरंत compile नहीं हुआ
  • errors कम थे, लेकिन लगभग हर कुछ हज़ार lines पर एक error आ जाती थी
  • cloc के अनुसार input Rust code का आकार यह था
    • alloc: Rust code 26,299 lines
    • core: Rust code 54,192 lines
  • translation के दौरान macro expansion होता है, इसलिए वास्तविक translation target मूल line count से बड़ा होता है

बने हुए Coq code का विभाजन

  • सबसे बड़ा बदलाव यह था कि coq-of-rust के output को हर input Rust file के लिए एक Coq file में बाँटा गया
  • यह विभाजन इसलिए संभव हुआ क्योंकि translation definition order के प्रति insensitive और context-free है
  • Rust files के बीच आम तौर पर circular dependencies होती हैं, जिन्हें Coq अनुमति नहीं देता, लेकिन इस translation approach में file-level separation संभव रहा
  • विभाजन के बाद output का आकार यह बना
    • alloc: 54 Coq files, 171,783 lines of Coq code
    • core: 190 Coq files, 592,065 lines of Coq code
  • files बाँटने से generated code को देखना और maintain करना आसान हुआ
    • compilation को parallelize करना आसान हुआ
    • एक-एक file पर ध्यान देकर debugging की जा सकती है
    • जो files compile नहीं होतीं उन्हें अलग रखना आसान है
    • single-file diff को ट्रैक करना आसान है

module name collision fixes और बची हुई files

  • कुछ bugs impl blocks में module name collisions से आए थे
  • समाधान यह था कि module name में और जानकारी जोड़कर uniqueness बढ़ाई जाए
    • पहले छूटी हुई where clause की जानकारी जोड़ी गई
    • उदाहरण के लिए, Mapping<K, V> के लिए Default trait implementation में यह शर्त कि K और V दोनों Default implement करें, module name में दिखाई जाती है
  • अभी Coq में compile न होने वाली files ये हैं
    • 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
  • यह कुल files का 4% है
  • compile होने वाली files के अंदर भी कुछ Rust constructs अभी axiomatized हैं, इसलिए सिर्फ इस अनुपात से पूरे unsupported area का आकलन करना कठिन है

Option::unwrap_or_default translation example

  • Rust का Option::unwrap_or_default, Some(x) होने पर x लौटाता है और None होने पर T::default() को call करता है
  • coq-of-rust इसे monadic form की Coq definition में अनुवादित करता है
    • input arguments और types को match करता है
    • Some branch में tuple field लेकर copy करता है
    • None branch में core::default::Default trait की default method को call करता है
  • वास्तविक verification में auto-generated definition की जगह एक सरल functional definition इस्तेमाल की जाती है
    • None होने पर core.simulations.default.Default.default लौटाया जाता है
    • Some x होने पर x लौटाया जाता है
  • auto-generated definition और सरल definition की समानता का proof CoqOfRust/core/proofs/option.v में है
  • अगर मूल Rust code बदलता है, तो यह proof उस बदलाव को पकड़ लेता है
  • core library का translation अपने-आप हुआ था, इसलिए हाथ से लिखी definitions की तुलना में generated definitions पर अधिक भरोसा किया जा सकता है
  • फिर भी coq-of-rust में गलती या अपूर्णता हो सकती है, इसलिए proof के समय code की वैधता जाँचना ज़रूरी है

बाकी चुनौतियाँ

  • Rust प्रोग्राम verification में standard library formalization पर भरोसा बढ़ा है
  • अगला लक्ष्य अब भी उबाऊ proof process को सरल बनाना है
  • खासकर यह दिखाने के लिए कि simulation मूल Rust code के बराबर है, ये काम ज़रूरी हैं
    • name resolution
    • high-level types का परिचय
    • side effects हटाना
  • इन चरणों को अलग-अलग संभालना आगे के सुधार की दिशा है

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

1 टिप्पणियां

 
GN⁺ 2024-05-16
Hacker News की राय

  • वाकई प्रभावशाली
    ऐसा automatic translation भरोसे के लक्ष्य को tool की ओर शिफ्ट कर देता है। coq-of-rust खुद Coq में नहीं, बल्कि Rust में लिखा गया है, इसलिए इसकी recursive संरचना काफी हैरान करने वाली है। लेकिन David A. Wheeler के “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0] की तरह, दूसरे compiler के जरिए Ken Thompson के Trusting Trusting attack को bypass करने के तरीके में CompCert-स्टाइल approach मिलाई जाए, तो correctness proof संभव लगता है
    verify करने के लिए coq-of-rust से coq-of-rust translator को Rust से Coq में बदलना होगा। और चूंकि वह translation Rust से की गई है, भले उस पर भरोसा न करें, Coq के अंदर वांछित correctness properties—खासकर यह कि Rust program को Coq में translate करते समय semantics preserve होते हैं—prove कर देना पर्याप्त होगा
    paper की तरह generated definitions की बजाय अधिक functional definitions पर proof करना आसान होने की संभावना है, इसलिए standard library में जैसे definitions के बीच equivalence prove किया जाता है, वैसी प्रक्रिया अपनाई जा सकती है। अगर मौजूदा coq-of-rust translator, खासकर lib/ [1], Rust की 6,350 lines का है, तो पूरा translator Coq में लिखना और generated version के साथ उसकी equivalence prove करना भी व्यावहारिक लगता है
    इसके बाद proven Coq-version coq-of-rust translator को Rust में लिखे coq-of-rust source पर चलाएँ, तो output होने वाली Coq definitions शुरू में इस्तेमाल किए गए Rust-version coq-of-rust translator के output से match करनी चाहिए
    वैसे, ऐसे काम को industry funding मिलते देखना अच्छा है। मैं cryptocurrency को लेकर थोड़ा cynical हूं, लेकिन यह सच है कि उस तरफ की correctness requirements Rust, Coq और परिचित master's students को support करने जैसे रुचि क्षेत्रों में सुधार को आगे बढ़ा रही हैं
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • मैं authors में से एक हूं, और सच में ऐसी प्रक्रिया coq-of-rust verification के लिए अच्छा तरीका हो सकती है
      हालांकि code खुद छोटा है, फिर भी input Rust code को parse और type-check करने के लिए Rust compiler पर निर्भर करता है। इसलिए उस हिस्से को भी verify करना होगा, या कम से कम बिना proof के formal specification देनी होगी। rustc का API काफी बड़ा और unstable है, यह एक बाधा है, लेकिन फिर भी भरोसा बढ़ाने का एक तरीका हो सकता है
    • यह मुझे उस समय की याद दिलाता है जब मैं SPARK Ada के साथ काम करता था। जिन projects के लिए supported Ada target नहीं होता था, खासकर बहुत छोटे devices में, हम Ada को C में convert करके फिर उस target के लिए compile करते थे, और इसकी वजह से SPARK side पर कई तरह की static analysis की जा सकती थी
      बेशक output या converter को verify करने की समस्या आती थी, लेकिन resulting C code verification के लिहाज से काफी readable होता था और उसका style भी constrained था, और tools पर trust भी ज्यादा था। SPARK static analysis पूरी verification/validation प्रक्रिया का हिस्सा थी, और tests व दूसरी activities अतिरिक्त trust layers देती थीं। कुल मिलाकर यह approach काफी अच्छी तरह काम करती थी
    • cryptocurrency ऐसी चीजों में मदद इसलिए करती है क्योंकि correctness constraints तो हैं ही, लेकिन एक बड़ी वजह यह भी है कि बहुत सारी wealth computer science में रुचि रखने वाले लोगों के पास transfer हुई है
      वे वह पैसा computer science research पर सिर्फ इसलिए नहीं खर्च करते कि इससे उन्हें फायदा होता है, बल्कि इसलिए भी कि यह उनके hobby से जुड़ी philanthropy है
    • मुझे ठीक से समझ नहीं आता कि यह approach binaries बनाने में इस्तेमाल होने वाले Rust compiler को malicious payload inject करने से कैसे रोकती है। A को B से build करके और B को A से build करके binaries compare किए जा सकते हैं, लेकिन
      दूसरा approach proof-carrying code है। इसमें Rust compiler executable output के साथ एक Coq proof भी emit करता है कि output input source code की semantics से मेल खाता है
      बेशक Rust के subset compiler को, उदाहरण के लिए borrow checker या optimization के बिना, किसी specific architecture के machine code में लिखकर, वहां से सब कुछ bootstrap भी किया जा सकता है

  • Coq जैसे semi-automatic deductive proof system से शुरू से अंत तक verified programs का आकार छोटा होता है। Libraries आसान हो सकती हैं क्योंकि code के हिस्से आपस में कम interact करते हैं, लेकिन general programs में ऐसा नहीं होता
    असल में इस तरह verify किए जा सकने वाले programs के size में बढ़ोतरी, पूरे programs के average size में बढ़ोतरी से धीमी रही है। Sound software verification, यानी specification से 100% match दिखाना, core algorithms की correctness proof जैसी जगहों पर जरूर उपयोगी है, लेकिन यह अच्छी तरह scale नहीं करता
    इसलिए research कुछ हद तक unsound methods की ओर गई है। 100% guarantee की cost, 99.9999% guarantee की cost से 10 गुना हो सकती है, और probability का वह फर्क software से बाहर की failure probability से भी छोटा हो सकता है। Physical systems के बारे में तो शुरू से ही यह prove नहीं किया जा सकता कि वे specification से match करते हैं, और specification खुद reality से पर्याप्त रूप से match न करे, इसकी भी संभावना होती है

    • मुख्य बात यह है कि standard library के unsafe हिस्सों और Rust की safety guarantees को prove कर दिया जाए, तो सिर्फ standard library इस्तेमाल करने वाले सभी safe Rust code की memory safety, data races न होना आदि transitively prove किए जा सकते हैं
      सिर्फ unsafe code को correct prove करना, सभी Rust code को prove करने की तुलना में बहुत कम effort में संभव है। यह Rust की safety guarantees पर बात करते समय अक्सर उठने वाली “unsafe code का क्या?” वाली criticism का जवाब है। Rust type system अकेले जिन gaps को संभालने के लिए पर्याप्त powerful नहीं है, उन्हें Coq जैसे stronger system से भरा जा सकता है

  • इस तरह की कोशिशों में एक बात ठीक से समझ नहीं आती। अगर code को Coq में manually या semi-manually बदलना पड़े, तो क्या उस प्रक्रिया में गलती होने की संभावना formal verification से मिलने वाले फ़ायदे से कहीं ज़्यादा नहीं होगी?
    यानी हमें कैसे पता चलेगा कि हमने जो prove किया है वह अब भी original code पर लागू है?

    • पता नहीं चल सकता। आखिरकार hardware, compiler, specification, Coq के trusted kernel वगैरह में से किसी न किसी चीज़ पर भरोसा करना ही पड़ता है।
      formal verification पर अक्सर ऐसे चर्चा होती है जैसे यह bug की संभावना को पूरी तरह खत्म कर देती हो, लेकिन असल में यह bug की संभावना को काफी कम करने के ज्यादा करीब है। फिर भी Rust और Coq के बीच automatic translation उन चीज़ों की complexity को बहुत घटा देता है जिन पर भरोसा करना पड़ता है, इसलिए इसे manual translation से बेहतर माना जाना चाहिए।
    • यह एक सही सीमा है, लेकिन इतनी खराब सीमा नहीं है।
      कई मामलों में translation का bug बस proof को असंभव बना देता है। तब कोई यह जांचते हुए कि proof pass क्यों नहीं हो रहा, translation bug ढूंढ लेता है।
      असली समस्या तब है जब translation bug original code के bug को बिल्कुल ठीक-ठीक cancel कर दे। अगर कोई systematic risk न हो, तो दो bugs का इस तरह एक-दूसरे को मिटा देना काफी कम संभावित है।
    • code coq-of-rust से automatically translate किया जाता है। translation में कोई समस्या मिले तो coq-of-rust tool में एक बार fix कर देने से सभी translation results update हो जाते हैं।

  • इच्छुक readers के लिए: मैंने यह blog post इसलिए submit की क्योंकि उसी blog की दूसरी posts की तुलना में इसमें cryptocurrency से जुड़ी बात कम directly है, लेकिन वहां technically और भी interesting posts हैं।
    खासकर हाल की दो posts इसी approach को Rust के बजाय Python पर apply करने के बारे में हैं।

  • मुझे पहले की एक lecture [1] याद है जिसमें formally verified C compiler में fuzzer ने bug ढूंढा था। वजह यह थी कि formal verification में frontend और backend शामिल नहीं थे।
    मुझे पता है कि Coq खुद या translation पर कितना भरोसा किया जा सकता है, यह सवाल भी उठता है, और यह भी सवाल है कि Rust updates के साथ sync कैसे होगा, लेकिन perfect formal verification भी शुरू से अंत तक 100% correctness का मतलब नहीं होती।
    [1] https://youtu.be/Ux0YnVEaI6A

  • मैं formal verification expert बिल्कुल नहीं हूं, लेकिन अगर Rust की basic library formally verified हो और unsafe code का इस्तेमाल न करे, तो क्या formally verified library इस्तेमाल करने वाले सभी Rust programs memory handling के लिहाज से practically formal verification-level quality के हो जाएंगे?

    • Rust की safety का bugs से लगभग कोई संबंध नहीं है।
      Rust की अपनी “safe” definition है, जिसे memory safety का subset माना जा सकता है। पूरी तरह safe Rust code में भी data races, deadlocks, memory exhaustion वगैरह संभव हैं, logical errors की तो बात ही अलग है।
    • कुछ हद तक मुझे लगता है कि यही सपना है, लेकिन इसमें कई caveats हैं और कुछ चीज़ों का सही बैठना ज़रूरी है।
      पहला, unsafe Rust की semantics को formalize करना होगा। Ralf Jung का pioneering RustBelt[1] काम बड़ा कदम था, लेकिन अभी complete नहीं है। खासकर pointer provenance एक मुश्किल factor साबित हो रहा है।
      दूसरा, इसके हिस्से के रूप में borrow checker का formal model चाहिए। Stacked borrows[2] एक अच्छा प्रयास था, लेकिन उसमें flaws हैं, और Tree borrows[3] शायद इसे ठीक कर सकता है, हालांकि और भी refined कुछ आने की संभावना है।
      तीसरा, formal memory model चाहिए। यह मुख्यतः atomic operations और synchronization के behavior से जुड़ा है, इसलिए Arc जैसे standard library components के लिए बहुत अहम है। यह व्यापक रूप से माना जाता है कि Rust का memory model C++ जैसा होना चाहिए और उसके साथ interoperable होना चाहिए, लेकिन “out of thin air” problem और seqlock जैसी missing capabilities बाकी हैं। Linux kernel के अभी भी अपना model इस्तेमाल करने की एक वजह यही है।
      चौथा, यह proof चाहिए कि safety guarantees अच्छी तरह compose होती हैं। खास तौर पर, unsafe Rust में लिखे sound code और safe Rust code को compose करने पर भी safety guarantees बनी रहनी चाहिए। अब तक अच्छे results हैं, लेकिन पूरे system के लिए इसे prove करना होगा।
      पांचवां, ऐसे proofs सभी code पर लागू हों, इसके लिए Rust में बचे सभी soundness bugs[1] बंद करने होंगे। इनमें से कई issues theoretical हैं या adversarial code[5] में ही practically important होते हैं, इसलिए progress slow है।
      यह सब हो जाने के बाद भी guarantee अभी भी partial ही होगी। system से जुड़ने वाली surface का बहुत बड़ा हिस्सा unsafe code पर आधारित है। अगर आप सिर्फ pure computation कर रहे हों तो अलग बात है, लेकिन उदाहरण के लिए graphics UI बना रहे हों, तो अब भी बहुत कुछ गलत हो सकता है।
      फिर भी practical आगे बढ़ने का रास्ता है, और वह आज की vulnerability-भरी systems की सामान्य स्थिति से कहीं बेहतर स्थिति तक ले जाता है।
      [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 expert नहीं हूं, लेकिन core code में unsafe काफी ज्यादा दिखता है। होना भी चाहिए।
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      मुझे नहीं लगता कि यहां सुझाए गए तरीके वाला Coq सभी unsafe calls को verify कर सकता है।

  • क्या इस approach की तुलना Aeneas या RustHornBelt से की जा सकती है? pointers और mutable borrows को कैसे handle किया जाता है?

    • RustHornBelt कैसे काम करता है, यह नहीं पता। हम safe code पर focus कर रहे हैं, लेकिन unsafe blocks के लिए भी “best effort” के तौर पर translation generate करते हैं
      Aeneas से तुलना करें तो लक्ष्य काफी मिलता-जुलता है, क्योंकि दोनों interactive theorem prover में Rust programs को verify करना चाहते हैं। हालांकि coq-of-rust में proof का target बनने वाले code का pure functional version हाथ से लिखा जाता है, या दोहराए जाने वाले काम के लिए GitHub Copilot की मदद से लिखा जाता है, और फिर साबित किया जाता है कि यह automatically translated result के equivalent है। Aeneas का लक्ष्य functional version को सीधे generate करना है
      pointers को सभी mutable pointers, यानी * type की तरह treat किया जाता है। Rust के borrow checker की जानकारी इस्तेमाल नहीं की जाती; इससे translation सरल हो जाती है, लेकिन इसकी कीमत proof के समय चुकानी पड़ती है
      proofs में pointers के बारे में reasoning करने के लिए user को custom allocator देने दिया जाता है, जिसे memory कैसे इस्तेमाल होगी उसके हिसाब से design किया जा सकता है। उदाहरण के लिए, अगर program तीन global mutable variables इस्तेमाल करता है, तो memory को तीन items वाले record के रूप में रखा जा सकता है। ये items शुरुआत में None होते हैं, ताकि यह दिखाया जा सके कि वे अभी allocated नहीं हैं
      यह technique कितनी scale करेगी, यह अभी नहीं पता, लेकिन कम से कम फिलहाल इससे separation logic reasoning से बचा जा सकता है। हम उम्मीद करते हैं कि verify किए जाने वाले ज्यादातर programs, खासकर application side वाले, अपेक्षाकृत “simple” memory discipline रखेंगे

  • क्या formal verification specification लिखना ज्यादा complex property-based testing इस्तेमाल करने जैसा है? साधारण programs से आगे बढ़ने पर property-based tests लिखना भी काफी मुश्किल और समय लेने वाला हो जाता है

    • मिलता-जुलता है, लेकिन हमेशा एक जैसा नहीं। property-based testing में आम तौर पर system के interface, function या procedure level पर, या उससे ऊंचे level पर, inputs का description specify किया जाता है और test किया जाता है कि output कोई property या properties का set satisfy करता है या नहीं
      उसी level पर formal verification करने पर यह काफी वैसा ही दिख सकता है। लेकिन formal verification tools और गहराई तक जा सकते हैं। उदाहरण के लिए, वे computation के अंदर system state को लेकर ऐसे सवालों के जवाब दे सकते हैं: “यह loop invariant है, क्या साबित किया जा सकता है कि यह हर iteration में सच में बना रहता है?” या “क्या साबित किया जा सकता है कि इस computation के दौरान किसी भी intermediate calculation में underflow/overflow कभी नहीं होता?”
      पहला काम property-based testing से भी संभव है, अगर loop के core को अलग procedure में निकालकर कई intermediate states के साथ चलाया जाए और invariant property test की जाए। दूसरा कहीं ज्यादा कठिन है, जब तक कि program को इतना ज्यादा न तोड़ा जाए कि उसे line-by-line अलग से execute किया जा सके

  • मुझे पता ही नहीं था कि ऐसा भी संभव है
    सोच रहा हूं कि क्या ऐसी कोशिशें kernel adoption के core हिस्सों में Rust adoption को तेज कर सकती हैं

  • क्या कोई “verification” concept को बहुत आसान तरीके से समझा सकता है? जानना चाहता हूं कि सिर्फ इसी उद्देश्य के लिए Coq जैसी पूरी language क्यों मौजूद है, और व्यापक समाज के लिए इसका practically क्या मतलब है