Rust Borrow Checker बग: Soundness का असली मतलब

Rust का type system एक पक्का वादा करता है: अगर आपका safe code compile हो गया, तो उसमें dangling pointers, data races या use-after-free नहीं हो सकते। इसलिए जब एक GitHub issue में perfectly safe दिखने वाला Rust snippet सामने आया, जो एक मरे हुए stack frame से कचरा मान प्रिंट करता था, और पता चला कि यह छेद Rust borrow checker में ग्यारह साल से पड़ा था, तो कई लोगों को लगा जैसे ज़मीन खिसक गई हो। यह बग covariant field assignment के ज़रिए struct की lifetime requirements को फिसलने देता है, और एक malicious Drop impl के साथ आप किसी local variable का reference एक global में रख सकते हैं और variable खत्म होने के बाद उसे पढ़ सकते हैं। AddressSanitizer इसे stack-use-after-scope कहता है। कंपाइलर ने इसे ठीक बताया था।

प्रतिक्रियाएँ अनुमान के मुताबिक आईं। कुछ लोगों ने Rust की safety कहानी को खत्म घोषित कर दिया। दूसरों ने कंधे उचकाए कि बग तो होते ही हैं। दोनों ही असली दिलचस्प बात को मिस करते हैं। यह बग इस बात का एक साफ़ natural experiment है कि static guarantees की असली कीमत क्या है, informal reasoning कहाँ टूटता है, और “type system sound है” और “कंपाइलर एक sound type system लागू करता है” के बीच का फ़ासला ही वह जगह है जहाँ सबसे दिलचस्प बग रहते हैं। तो चलिए इस कहानी से उठी आम मान्यताओं में से हर एक को परखते हैं।

मिथक 1: Unsoundness बग का मतलब है कि Rust का safety model फेल हो गया

पहली प्रतिक्रिया यह होती है कि इसे थ्योरी में दरार मान लिया जाए। ऐसा नहीं है। किसी ने lifetimes के नियम दोबारा नहीं लिखे। किसी को यह पता नहीं चला कि ownership और borrowing मूल रूप से टूटे हुए हैं। Rust का type system, जैसा वह व्हाइटबोर्ड और RFCs में डिज़ाइन हुआ था, साफ़ कहता है कि यह program रद्द होना चाहिए। कंपाइलर बस उसे रद्द करने में नाकाम रहा।

specification और implementation के बीच का यह फ़र्क हमारे क्षेत्र की सबसे पुरानी दरारों में से एक है। Tony Hoare ने communicating sequential processes की एक खूबसूरत थ्योरी दी; उसके बाद दशकों तक C compilers ऐसे कोड को गलत compile करते रहे जो standard के हिसाब से पूरी तरह valid था। थ्योरी ठीक रहती है और artifact लीक करता रहता है। हम पहले भी लिख चुके हैं कि specification-implementation gap ही वह जगह है जहाँ बग रहते हैं, और यह उसका एक क्लासिक उदाहरण है। lifetime के नियम गलत नहीं थे। rustc में variance inference का कोड, यानी वह हिस्सा जो तय करता है कि कब &'a T की जगह &'static T रखना कानूनी है, उस जगह एक छेद था जहाँ assignment एक covariant field से होकर गुज़रती थी।

exploit का ढाँचा, सरल करके, ऐसा है। आप एक wrapper बनाते हैं जिसकी Drop impl अपने payload को एक global 'static store में कॉपी करती है। आम तौर पर कंपाइलर payload को 'static होने पर मजबूर करता है, इसलिए locals के references अंदर नहीं जा सकते। यह बग एक covariant assignment के ज़रिए छोटी उम्र वाले reference को “धो” देता है, और wrapper के अंदर &l आ जाता है, जहाँ l एक local String है:

struct Q<T: 'static + Send>(Option<T>);
impl<T: 'static + Send> Drop for Q<T> {
fn drop(&mut self) {
if let Some(t) = self.0.take() {
KEPT.lock().unwrap().push(Box::new(t)); // escapes to 'static!
}
}
}
fn main() {
{
let l = String::from("hello world, this is long enough");
let mut q = Q(None);
q.0 = Some(&l); // should be rejected; 'static required
} // <- drop runs here, stashing &l in KEPT
// l is gone; KEPT now holds a dangling &'static String
}

हर अलग लाइन मासूम दिखती है। असर सिर्फ़ उनके मेल में है: एक covariant field, एक assignment जो lifetime bound को ढीला करता है, और एक Drop जो payload को ऐसी जगह ले जाता है जहाँ वह अपने referent से ज़्यादा जीता है। checkers में implementation बग का यही पैटर्न होता है: invariant global होता है, पर enforcement local होता है, और कोई एक code path जाँच करना भूल जाता है।

तो नहीं, safety model फेल नहीं हुआ। safety model का enforcement फेल हुआ। यह छोटी विफलता है, पर जैसा हम आगे देखेंगे, यह मामूली भी नहीं है।

मिथक 2: ग्यारह साल तक न पकड़ा जाना मतलब बग हानिरहित है

Rust टीम का अपना triage तर्क कुछ ऐसा था: अगर लोग इसकी चपेट में आ रहे होते तो यह P-critical होता, पर ग्यारह साल तक कोई रिपोर्ट न होने का मतलब है कि इसे ट्रिगर करना आसान नहीं है, इसलिए यह P-high है। इसमें कुछ सच्चाई है। असल में memory unsafety पैदा करने के लिए आपको एक जानबूझकर खतरनाक Drop implementation चाहिए जो डेटा को 'static जगह में ले जाए। ऐसा लगभग कोई नहीं लिखता। गलती से उजागर होने की सतह बहुत छोटी है।

लेकिन इस वाक्य में “गलती से कम ही ट्रिगर होता है” बहुत भारी काम कर रहा है। Safety guarantees सिर्फ़ गलतियों के बारे में नहीं होतीं; वे इस बारे में होती हैं कि जब आसपास का कोड दोस्ताना न हो, तब आप किस पर भरोसा कर सकते हैं। sound type system का पूरा मकसद यही है कि आप modularly reason कर सकें: मुझे आपकी Drop impl का audit करने की ज़रूरत नहीं, क्योंकि कंपाइलर पहले ही साबित कर चुका है कि कुछ बुरे मेल लिखे ही नहीं जा सकते। एक बार छेद हो जाए, तो यह modularity खत्म हो जाती है। कोई malicious dependency, या किसी नेक इरादे वाले लेखक की गलत dependency, अब वह कर सकती है जिसे भाषा ने असंभव बताया था।

इतिहास “अव्यवहारिक” बगों से भरा पड़ा है, जो सही gadget आते ही बेहद exploitable हो गए। जैसा एक कमेंट करने वाले ने कहा, व्यावहारिक सवाल यह है कि इसे ठीक करने से इकोसिस्टम का कोई असली crate टूटेगा या नहीं, और जवाब शायद “बहुत कम या कोई नहीं” है, जो अच्छी खबर है। पर ग्यारह शांत सालों से सही सबक यह नहीं है कि “बग हानिरहित था।” सबक यह है कि सबूत का न मिलना असल में अनुपस्थिति का सबूत नहीं होता, खासकर उन failure modes के लिए जिन्हें संयोग नहीं बल्कि इरादा चाहिए।

मिथक 3: ज़्यादा आँखें सारे बगों को सतही बना देती हैं

यह वह मिथक है जो हमें सबसे ज़्यादा शर्मिंदा करना चाहिए। rustc अब तक लिखे गए सबसे ज़्यादा जाँचे जाने वाले compilers में से एक है। यह open source है, इसकी एक समर्पित types टीम है, एक सक्रिय academic community है (RustBelt ने कुछ साल पहले Rust के core का formal model दिया था), और रोज़ लाखों उपयोगकर्ता इसे ठोंकते-पीटते हैं। फिर भी lifetime inference में एक soundness छेद दशक से ज़्यादा समय तक पड़ा रहा, आसपास की पूरी मशीनरी के कई बार पूरी तरह दोबारा लिखे जाने के बावजूद।

Linus's Law मानता है कि आँखें सही जगह देख रही हैं और उनके दिमाग में सही मॉडल है। type system की unsoundness इन दोनों मान्यताओं को तोड़ देती है। ये कई features के चौराहे पर रहती हैं: variance, drop order, coercion, trait bounds, और हर feature अपनी जगह सही होता है। reviewers कोड पढ़ते हैं और इरादतन invariant देख लेते हैं, क्योंकि कोड भी उन्हीं लोगों ने लिखा था जिन्होंने वही invariant सोचा था। प्रक्रिया में ही confirmation bias बैठा है। counterexample खोजने के लिए आपको attacker की तरह सोचना पड़ता है, और अपनी ही abstractions के बारे में attacker की तरह सोचना सचमुच कठिन है।

counterexamples.org नाम की एक पूरी वेबसाइट है जो इस बात का कैटलॉग रखती है कि सही दिखने वाले type rules कैसे टूटते हैं, और उनका साझा धागा mutability का किसी और चालाक चीज़ के साथ मेल है, बिल्कुल इसी बग जैसा। ये नए सबक नहीं हैं। ML के type system में mutable references और polymorphism के बीच एक मशहूर unsoundness थी, जिसे value restriction से ठीक किया गया। Java के arrays covariant हैं और runtime पर ArrayStoreException फेंक सकते हैं, क्योंकि भाषा के डिज़ाइनरों ने soundness की जगह सुविधा चुनी। चीज़ें बदलती हैं, पर वही तीन features, यानी subtyping, mutation और generics, मिलकर किसी न किसी को फँसाते रहते हैं। अगर आपको इस तरह की पुरातत्व-खुदाई पसंद है, तो Lisp का साठ साल का इतिहास दिखाता है कि ये विचार कितने समय से विकसित हो रहे हैं, और Rob Pike के पुराने नियम सादगी के बारे में अलग तरह से पढ़े जाते हैं, जब आप समझते हैं कि जटिलता ही वह जगह है जहाँ soundness के छेद पनपते हैं।

आँखें मदद करती हैं। वे काफ़ी नहीं हैं। ईमानदार स्थिति, जो मैंने अपनी भाषा बनाने वाले एक व्यक्ति से सुनी, कुछ ऐसी है: कोई भी review हर समस्या हल नहीं करता, इसलिए आपको ऐसे mechanical तरीकों की ज़रूरत है जो थकते नहीं और आपकी मान्यताओं को साझा नहीं करते।

मिथक 4: Informal reasoning मूल रूप से एक proof है

जब Rust के lifetime नियम डिज़ाइन हुए, तो उन पर समझदार लोगों ने बहुत सावधानी से, बहुत सारे उदाहरणों के साथ बहस की। यह informal reasoning है, और लगभग हर production compiler इसी तरह बनता है। नतीजा एक ऐसी प्रणाली है जो जहाँ तक किसी को पता है sound है, और जैसा हमने अब दो बार सीखा है, यह “sound” होने जैसा नहीं है।

इन दोनों के बीच का फ़ासला ही RustBelt जैसे प्रोजेक्ट और next-generation trait solver पर चल रहे काम का कारण है। RustBelt, Iris separation-logic framework पर Coq (अब Rocq) में बना, Rust के core typing rules के मॉडल को machine-check करता है, जिसमें unsafe abstraction boundaries जैसे डरावने हिस्से भी शामिल हैं। यह एक मील का पत्थर था। पर ध्यान दें कि उसने क्या साबित किया: Rust का एक मॉडल, rustc नहीं। यह proof λRust calculus को कवर करता है, और production compiler इस बीच बदलता रहा है, नई features उगती रही हैं, और ऐसे implementation फ़ैसले जमा होते रहे हैं जिन्हें किसी ने दोबारा verify नहीं किया। यह issue उसी बदलाव का बिल है जो अब चुकाना पड़ रहा है।

पूरे production compiler को formalize करना बेहद महँगा है। CompCert, जो formally verified C compiler है, एक ऐसी भाषा के लिए वर्षों की विशेषज्ञ मेहनत ले गया जो Rust से कहीं छोटी है, और वह compilation passes को verify करता है, न कि यह साबित करता है कि source type system हर बुरे program को पकड़ लेता है। कोई भी rustc के बीस लाख लाइनों का Coq proof नहीं लिखने वाला। व्यावहारिक रास्ता defense in depth जैसा दिखता है:

• Core rules के machine-checked मॉडल (RustBelt जैसे), ताकि थ्योरी में ही कोई छेद न रहे।
• Systematic fuzzing और case-analysis tooling जो adversarial programs बनाए, यानी feature-interaction के वे कोने जिन्हें इंसान टेस्ट करने की सोचते ही नहीं।
• Checker की mutation और property-based testing: अगर किसी bound को पलटने से program फेल होना चाहिए, तो जाँचें कि वह होता है। SQLite की testing संस्कृति यहाँ मॉडल है।
• Known unsound issues की एक maintained सूची, Rust में इनमें से सौ से ज़्यादा टैग किए गए हैं, जिसे लोककथा नहीं बल्कि इंजीनियरिंग प्राथमिकता वाले backlog की तरह देखा जाए।

दिलचस्प बात यह है कि LLM-आधारित search यहाँ शुद्ध लाभ साबित हो सकता है: एक tool जो थके बिना features को टेढ़े तरीकों से जोड़ता रहे, वही adversary है जिसकी informal reasoning में कमी है। जिस अंतिम लक्ष्य की उम्मीद हममें से कई लोग करते हैं, वह एक formally specified Rust है, जिसका checker spec के खिलाफ साबित हो। पर यहाँ से वहाँ तक का काम थकाऊ है, बिना ग्लैमर वाली constraint-solving।

मिथक 5: अगर soundness पूर्ण नहीं है, तो static safety एक धोखा है

निंदक पढ़त यह कहती है: Rust ने safety का वादा किया, वादे में एक लूपहोल था, इसलिए वादा मार्केटिंग था और हम वापस C में बेतरतीब pointers चलाने पर जा सकते हैं। यह बिल्कुल उल्टा है, और यह थोड़ी सटीकता से समझाने लायक है।

type system में soundness एक गणितीय वस्तु के बारे में theorem है। एक production भाषा जो देती है, वह एक सांख्यिकीय और आर्थिक गारंटी है: बग की पूरी श्रेणियाँ, जैसे use-after-free, data races, iterator invalidation, “आपके codebase की लगातार पृष्ठभूमि विकिरण” से निकलकर ऐसी घटनाओं में बदल जाती हैं जो ग्यारह साल बाद मिलने पर भी फ्रंट पेज पर आ जाएँ। base rates की तुलना करें। बड़े C और C++ codebases के memory-safety बग साल दर साल गंभीर CVEs का अधिकांश हिस्सा होते हैं, और अब किसी एक पर किसी को हैरानी नहीं होती। Rust के unsoundness बग इतने दुर्लभ हैं कि हर एक को अपना GitHub issue, अपना discussion thread और अपनी postmortem संस्कृति मिलती है। जिस दुर्लभता को आप गिन सकते हैं, वह उस दुर्लभता से अलग दुनिया है जिसे आप गिन नहीं सकते।

इस बात में भी फ़र्क है कि विफलताएँ कैसे जमा होती हैं। C में हर लाइन memory-safety का संभावित खतरा है, इसलिए सतर्कता की लागत कोड के आकार के साथ हमेशा बढ़ती है। Rust में सतर्कता कुछ किनारों पर केंद्रित होती है: unsafe blocks, FFI, और (जैसा अब हम जानते हैं) कंपाइलर का अपना checker। यही केंद्रीकरण audit, Miri जैसे tooling और formal methods को व्यावहारिक बनाता है। गारंटी बाइनरी नहीं है; यह इस बात का बड़ा पुनर्गठन है कि आपका जोखिम कहाँ रहता है।

एक type system जिसमें एक ज्ञात बग है और जिसे ग्यारह साल के production ट्रैफिक ने कभी नहीं छुआ, फिर भी उस भाषा से अनंत गुना मज़बूत है जिसमें बग ही डिज़ाइन है।

असल में आपको क्या सीखना चाहिए

अगर आप Rust लिखते हैं, तो आपको कुछ भी बदलने की ज़रूरत नहीं है। इस issue के दर्ज होने से पहले आपका कोड चुपचाप unsafe नहीं था; व्यावहारिक exploit के लिए इरादा ज़रूरी था। अगर आप libraries maintain करते हैं, तो ईमानदार कदम वही है जो हमेशा था: unsafe सतह छोटी रखें, मुश्किल हिस्सों पर Miri चलाएँ, और borrow checker को दूसरों के दुर्भावनापूर्ण कोड का oracle न मानें। उसे अपनी गलतियाँ पकड़ने का एक बेहद भरोसेमंद tool मानें।

अगर आप भाषाएँ या compilers बनाते हैं, तो यह बग एक तोहफ़ा है: production में soundness कैसे असल में फेल होती है, इसका एक दुर्लभ, अच्छी तरह दर्ज नमूना। यह थ्योरी में नहीं, enforcement में है; किसी एक feature में नहीं, feature के चौराहे पर है; समीक्षा से नहीं, adversarial निर्माण से पकड़ में आया। जो टीमें इसे गंभीरता से लेती हैं, यानी trait-solver के दोबारा लिखे जाने, region-constraint के काम और verification-adjacent tooling में निवेश करती हैं, उनकी गारंटियाँ दस साल बाद मायने रखेंगी।

और सबके लिए: गारंटी क्या होती है, इसे फिर से परखें। हमने दशकों तक “साबित” को “ठोस तर्क से समझाया गया और अब तक नकारा नहीं गया” के साथ मिलाया है, type systems, cryptographic protocols और distributed consensus में। भरोसे की परिपक्व समझ यह मानना नहीं है कि पुल परफेक्ट है। यह जानना है कि पुल के निरीक्षक हैं जो अपनी खोजें प्रकाशित करते हैं, जो मिलता है उसे ठीक करते हैं, और दरारों की एक सार्वजनिक सूची रखते हैं जिन्हें उन्होंने अभी ठीक नहीं किया। इस मापदंड पर, छेद खोजने में ग्यारह साल कोई आरोप नहीं है। यह इस बात का सबूत है कि कंपाइलर के आसपास की मानवीय व्यवस्था लगभग वैसे ही काम कर रही है जैसे उसे करना चाहिए।