Lean ने प्रोग्राम की शुद्धता साबित की, लेकिन उसके भीतर बग मिला

 (kirancodes.me)
1 पॉइंट द्वारा GN⁺ 17 일 전 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • औपचारिक रूप से सत्यापित zlib implementation को fuzzing करने पर Lean 4 runtime के lean_alloc_sarray में heap buffer overflow मिला
  • AI fuzzer Claude, AFL++, AddressSanitizer आदि का उपयोग कर 10 करोड़ से अधिक बार test करने के बाद 4 crash और 1 memory vulnerability की पुष्टि हुई
  • मिली समस्याएँ दो प्रकार की थीं: runtime overflow और Archive.lean में Out-of-Memory आधारित denial of service (DoS)
  • सत्यापित compression·decompression algorithm सुरक्षित थे, लेकिन असत्यापित archive parser और runtime layer में vulnerabilities मौजूद थीं
  • नतीजतन, formal verification शक्तिशाली है, लेकिन Trusted Computing Base (TCB) की सुरक्षा सुनिश्चित किए बिना पूरे system की स्थिरता की गारंटी नहीं दी जा सकती

Lean verification पास कर चुके प्रोग्राम में मिला बग

  • Lean से औपचारिक रूप से सत्यापित zlib implementation को fuzzing करने पर Lean 4 runtime में heap buffer overflow मिला
    • सत्यापित application code में memory vulnerability नहीं थी
    • लेकिन Lean runtime की lean_alloc_sarray function में overflow हुआ, जिससे Lean 4 के सभी version प्रभावित होते हैं
  • AI-आधारित fuzzer Claude, AFL++, AddressSanitizer, Valgrind, UBSan आदि का उपयोग कर 10 करोड़ से अधिक fuzzing runs किए गए
    • lean-zip के compression, decompression, archive processing सहित 6 attack surface पर 16 parallel fuzzer चलाए गए
    • 19 घंटे में 4 crash input और 1 memory vulnerability मिली
  • दो प्रमुख बग की पुष्टि हुई
    • Lean runtime की lean_alloc_sarray में heap buffer overflow
    • lean-zip के Archive.lean module में Out-of-Memory आधारित denial of service (DoS)
  • formal verification की सीमाएँ सामने आईं
    • lean-zip के compression·decompression algorithm पूरी तरह सत्यापित थे, लेकिन archive parser (Archive.lean) सत्यापित नहीं था, इसलिए DoS vulnerability मौजूद थी
    • runtime bug Trusted Computing Base के भीतर की समस्या है, इसलिए यह सभी Lean program को प्रभावित करती है
  • निष्कर्षतः, Lean की formal verification ने application code की स्थिरता साबित की, लेकिन verification के दायरे के बाहर के components में अब भी vulnerabilities मौजूद हैं
    • verification केवल उसी दायरे में शक्तिशाली है जहाँ यह लागू की गई हो, और मूल trust layer की सुरक्षा सुनिश्चित करना अनिवार्य है

fuzzing प्रयोग का अवलोकन

  • लक्षित codebase lean-zip की सत्यापित zlib implementation थी
    • सभी theorem, specification, documentation और C FFI binding हटा दिए गए ताकि केवल pure Lean code बचे
    • Claude को यह पता न चले कि code सत्यापित है, इसके लिए bias रोका गया

  • प्रयोग का वातावरण

    • 16 parallel fuzzer ने ZIP, gzip, DEFLATE, tar, tar.gz, compression सहित 6 attack surface पर काम किया
    • AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck, flawfinder आदि साथ में चलाए गए
    • 48 manual exploit files सहित कुल 105,823,818 runs, और 359 seed files का उपयोग हुआ
    • 19 घंटे में 4 crash input और 1 memory vulnerability मिली

बग 1: Lean runtime में heap buffer overflow

  • vulnerable function: lean_alloc_sarray
    • यह ByteArray, FloatArray जैसी सभी scalar array allocate करने वाली function है
    • sizeof(lean_sarray_object) + elem_size * capacity की गणना में integer overflow हो सकता है

  • समस्या का कारण

    • जब capacity SIZE_MAX के करीब हो, तो जोड़ overflow होकर छोटा buffer allocate हो जाता है
    • इसके बाद caller n bytes पढ़ता है, जिससे heap buffer overflow होता है

  • trigger condition

    • lean_io_prim_handle_read में nbytes बहुत बड़ा होने पर यह होता है
    • compressedSize को 0xFFFFFFFFFFFFFFFF बताने वाली 156-byte ZIP64 header file से इसे reproduce किया जा सकता है
    • Lean 4 के सभी version (नवीनतम nightly सहित) प्रभावित हैं
    • reproduction code example
    def main : IO Unit := do
  IO.FS.writeFile "test.bin" "hello"
  let h ← IO.FS.Handle.mk "test.bin" .read
  let n : USize := (0 : USize) - (1 : USize)
  let _ ← h.read n
    • ऊपर का code चलाने पर lean_alloc_sarray में overflow होता है
    • fix PR सबमिट किया जा चुका है

बग 2: lean-zip archive parser में denial of service (DoS)

  • vulnerable function: readExact (Archive.lean)
    • यह ZIP central directory के compressedSize field का बिना validation सीधे उपयोग करता है
    • h.read call करते समय असामान्य रूप से बड़ा size माँगता है, जिससे excessive memory allocation और OOM होता है

  • समस्या का पुनरुत्पादन

    • यदि 156-byte ZIP file अपने आकार को कई exabyte बताती है, तो process INTERNAL PANIC: out of memory के साथ बंद हो जाता है
    • system unzip header size को validate करता है, लेकिन lean-zip ऐसा नहीं करता

वे हिस्से जिन्हें formal verification नहीं पकड़ सकी

  • DoS vulnerability का कारण

    • Archive.lean module असत्यापित क्षेत्र है
    • compression·decompression pipeline (जैसे DEFLATE, Huffman, CRC32) पूरी तरह सत्यापित थी, इसलिए वहाँ समस्या नहीं थी
    • vulnerability उसी हिस्से में उत्पन्न हुई जहाँ verification लागू नहीं थी

  • runtime overflow की प्रकृति

    • Lean runtime Trusted Computing Base (TCB) का हिस्सा है
    • सभी Lean proofs runtime की शुद्धता को पूर्वधारणा मानते हैं
    • इसलिए runtime bug सभी Lean program की सुरक्षा को प्रभावित करता है

सत्यापित code की स्थिरता

  • 10.5 करोड़ runs के परिणाम

    • Lean द्वारा generate किए गए C code में heap overflow, use-after-free, stack overflow, UB, array out-of-bounds कुछ भी नहीं मिला
    • Claude के आकलन के अनुसार इसे “सबसे memory-safe codebase में से एक” माना गया

  • Lean type system का प्रभाव

    • dependent types और well-founded recursion संरचना C/C++ आधारित zlib implementation में आम vulnerabilities (CVE class) को संरचनात्मक रूप से रोकती है

  • निष्कर्ष

    • सत्यापित code क्षेत्र बहुत मजबूत था और fuzzer के लिए error ढूँढना कठिन था
    • लेकिन असत्यापित हिस्सों और runtime layer में अब भी vulnerabilities मौजूद हैं
    • verification की सीमा उसके लागू दायरे और trust base की सुरक्षा से तय होती है

मुख्य सीख

  • formal verification जहाँ लागू की गई है वहाँ अत्यंत शक्तिशाली है, लेकिन असत्यापित सहायक components या runtime layer पूरी स्थिरता को खतरे में डाल सकते हैं
  • Trusted Computing Base की सुरक्षा सुनिश्चित करना अनिवार्य है, और सत्यापित system में भी यह सवाल बना रहता है: “कौन पहरेदारों की निगरानी करेगा (Quis custodiet ipsos custodes)”

संदर्भ लिंक

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

1 टिप्पणियां

 
GN⁺ 17 일 전
Hacker News टिप्पणियाँ

  • इस लेख का शीर्षक और फ्रेमिंग कुछ अजीब लगा
    दरअसल लेखक ने साफ़ लिखा है कि प्रमाणित कोड के भीतर उसे कोई bug या error नहीं मिला
    मिले दो bug प्रमाण के दायरे से बाहर थे; एक specification omission था, और दूसरा C++ runtime का heap overflow
    मैं यह रेखांकित करना चाहता हूँ कि bug Lean के runtime में मिला था, verification करने वाले kernel में नहीं
    Lean दस्तावेज़ लिंक देखें

    • मुझे लगता है कि verified system में bug की बात करते समय पूरे binary को देखना चाहिए
      अगर buffer overflow की वजह से आपके Bitcoin खो जाएँ, तो यह जानकर तसल्ली नहीं मिलेगी कि bug runtime में था
      और अगर program crash हो जाए, तो ज़्यादातर users उसे bug ही मानेंगे
      Lean को वास्तविक production environment में चलाने वाले लोग भी काफ़ी होंगे
    • सिर्फ़ शीर्षक देखकर मुझे लगा था कि Lean kernel में bug है, लेकिन असल में समस्या Lean runtime और lean-zip में मिली
      अगर kernel में नहीं है, तो proof की विश्वसनीयता पर इसका बड़ा असर नहीं पड़ता
    • lean-zip में specification omission verification के दर्शन के हिसाब से एक अहम समस्या है
      “Hello world” program को verify करते समय भी सिर्फ़ output नहीं, बल्कि side effects भी specification में होने चाहिए
      अगर runtime और kernel की सीमा पर memory corruption हो सकती है, तो proof की विश्वसनीयता घट सकती है
      आखिरकार असली मुद्दा यह स्पष्ट परिभाषित करना है कि “क्या verify किया जाना चाहिए”
    • इस साइट की पोस्ट सूची देखकर मज़ेदार लगा कि यह धीरे-धीरे और ज़्यादा clickbait होती जा रही है
      संबंधित पोस्ट सूची
    • Lean runtime के bug को lean-zip का bug कहना वैसा ही है जैसे JRE के bug को Java app का bug कहना
      ऐसा लगा जैसे लेखक ने जानबूझकर गलतफ़हमी पैदा की हो

  • मुझे भी प्रमाणित कोड में ऐसा ही अनुभव हुआ है
    मेरे मामले में overflow नहीं, बल्कि spec bug समस्या थी
    अगर specification ही गलत हो, तो code और proof दोनों perfect होने पर भी व्यवहार इच्छित तरीके से नहीं होगा
    आख़िर में verification की कठिनाई इंसानी इरादे को ठीक-ठीक व्यक्त करने में है
    यह विश्वास कि AI verification को पूरी तरह हल कर देगा, झूठा भरोसा दे सकता है

    • मेरा भी ऐसा ही अनुभव रहा है
      Lean, TLA+, Z3 जैसे tools से prove की जा सकने वाली specifications सरल की हुई होती हैं और उनमें बहुत-सी assumptions चाहिए होती हैं
      फिर भी यह एक शक्तिशाली tool है
      यह complex algorithm के bug को सीमित करके specification boundary साफ़ देखने में मदद करता है
      AI की वजह से ऐसा proof work बहुत आसान हो गया है
    • मेरे मन में हमेशा सवाल उठता है, “verification system पर भरोसा कैसे किया जा सकता है?”
      program को verify करने वाला दूसरा program भी आखिर bug वाला हो सकता है
      complete self-verification असंभव होने की बात Heisenberg uncertainty principle की याद दिलाती है
      अंततः verification “दूसरे स्वतंत्र implementation” के ज़रिए भरोसा बढ़ाने की प्रक्रिया है
    • मेरे code के bug दो तरह के होते हैं
      (1) जब वह इच्छित व्यवहार से अलग काम करे
      (2) जब वह इच्छित अनुसार काम करे, लेकिन वही इरादा गलत हो
      proof assistant (1) को रोक सकता है, लेकिन (2) को नहीं
      यानी design soundness को prove नहीं किया जा सकता
      seL4 की तरह सब कुछ verify करना बहुत महँगा और समय लेने वाला है
    • मुझे लगता है कि specification को verify करने का तरीका चाहिए
      formal logic + adversarial thinking को जोड़कर, program को क्या करना चाहिए और क्या नहीं करना चाहिए, इसकी पूरी सूची बनाना आदर्श होगा

  • शीर्षक clickbait जैसा लगा
    प्रमाणित हिस्से में bug नहीं था, फिर इसे ऐसे क्यों लिखा गया समझ नहीं आया
    HN पर मैं तथ्य-आधारित पोस्ट देखना चाहता हूँ, यह समय की बर्बादी लगी

    • क्या verified software में “सिर्फ़ वही bug bug है जो proof का उल्लंघन करे” कहना निष्पक्ष है?
      “bug नहीं” कहकर प्रचार किया जाता है, लेकिन असल में मतलब होता है “सिर्फ़ उस दायरे में जहाँ specification पूरी तरह व्यक्त की गई हो”
      पूरी तरह सही होते हुए भी वास्तविक दुनिया में मरा हुआ सही हो सकता है — यानी सिद्धांत में सही, पर व्यवहार में टूटा हुआ
    • शीर्षक तकनीकी रूप से सही हो सकता है, लेकिन उसने lean-zip के non-verified code की समस्या को ऐसे पेश किया जैसे वह प्रमाणित हिस्से का bug हो
    • नतीजतन “प्रमाणित हिस्से की सीमा को स्पष्ट करो” वाला संदेश दिलचस्प और उचित है
    • दूसरा bug बिना आधार के गढ़ा हुआ लगा
      कोई code reference नहीं था, और असली code देखने पर समझ आता है कि यह गलतफ़हमी है
    • आखिरकार lean-zip सिर्फ़ एक Zlib binding है

  • यह समस्या distributed systems verification में भी अक्सर दिखती है
    proof सिर्फ़ खास शर्तों, यानी operating envelope, के भीतर ही वैध होता है, और दिलचस्प failures उसी सीमा पर होते हैं
    TLA+ में भी यही बात है; जैसे ही वास्तविक दुनिया assumptions से बाहर जाती है, proof अर्थहीन हो जाता है
    मैं चाहता हूँ कि operating envelope को machine-readable तरीके से घोषित किया जाए और runtime में उसकी निगरानी हो

    • मैंने भी CPU के hardware bug सीधे खोजे हैं
      लेकिन ज़्यादातर bug hardware में नहीं, बल्कि लोगों के docs न पढ़ने से पैदा होते हैं
      सिर्फ़ formal modeling से भी bugs की संख्या बहुत कम की जा सकती है

  • यह अपेक्षित, लेकिन अच्छी खबर है
    इसका मतलब है कि LLM ऐसा code बना सकता है जो formal verification पास कर जाए
    आगे चलकर bug धीरे-धीरे hardware layer की तरफ़ शिफ्ट होंगे
    अंततः hardware specification के formalization की ज़रूरत पड़ेगी
    अगर manufacturer इसे सार्वजनिक नहीं करेंगे, तो community के साथ टकराव हो सकता है
    लंबी अवधि में रास्ता दो तरफ़ जाएगा: vulnerabilities का extinction या जानबूझकर insertion

  • शुरुआत में मुझे लगा कि लेखक ने प्रमाणित हिस्से का test नहीं किया
    लेकिन पढ़ते-पढ़ते समझ आया कि bug प्रमाण के दायरे के बाहर मिला था
    इसलिए शीर्षक कुछ बढ़ा-चढ़ाकर कहा गया लगा

    • पोस्ट का लेखक खुद सामने आया
      उसने कहा कि अगर verified system के bug की बात है, तो पूरे binary को शामिल करना चाहिए
      और उसने बताया कि Archive.lean के compressed header parsing हिस्से में crash कराने वाला input वास्तव में मिला था

  • Donald Knuth की मशहूर बात याद आ गई
    “चेतावनी: ऊपर दिए गए code में bug हो सकते हैं। मैंने सिर्फ़ यह prove किया है कि यह सही है, इसे चलाकर नहीं देखा।”

  • parser को verify न करना एक बड़ी गलती लगता है
    binary format parsing हमेशा जोखिम भरा क्षेत्र है

  • असली बात यह है कि AI agent ने fuzzer के साथ मिलकर Lean में heap buffer overflow खोजा
    यह काफ़ी बड़ी उपलब्धि है

    • मुझे लगता है कि यह वाकई उपयोगी खोज है

  • Claude का यह कहना दिलचस्प लगा कि “यह उन सबसे memory-safe codebase में से एक है जिनका मैंने analysis किया है”
    लेकिन यह ऐसे मज़ाक जैसा लगा मानो यह Claude का पहला analyzed code हो

    • RL के साथ व्यापक रूप से trained Claude के लिए यह पहली code analysis नहीं हो सकती
      वह इतना अच्छा इसी वजह से है
    • शायद Claude कोई ऐसी चीज़ चुपचाप कर रहा है जिसके बारे में हमें पता नहीं 😄