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

 (kirancodes.me)
1 पॉइंट द्वारा GN⁺ 15 일 전 | अभी कोई टिप्पणी नहीं है. | 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)”

संदर्भ लिंक

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

अभी कोई टिप्पणी नहीं है.

अभी कोई टिप्पणी नहीं है.