Lean พิสูจน์ความถูกต้องของโปรแกรมได้ แต่กลับพบบั๊กอยู่ภายในนั้น

 (kirancodes.me)
1 คะแนน โดย GN⁺ 14 일 전 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • จากการทำ fuzzing กับอิมพลีเมนเทชัน zlib ที่ผ่านการตรวจพิสูจน์เชิงรูปแบบ พบ heap buffer overflow ใน lean_alloc_sarray ของ Lean 4 runtime
  • หลังทดสอบมากกว่า 100 ล้านครั้งด้วย AI fuzzer Claude, AFL++, AddressSanitizer ฯลฯ ยืนยันได้ว่าเกิด 4 crash และ 1 ช่องโหว่ด้านหน่วยความจำ
  • ปัญหาที่พบแบ่งได้เป็น 2 ประเภท คือ runtime overflow และ การปฏิเสธการให้บริการ (DoS) จาก Out-of-Memory ใน Archive.lean
  • แม้อัลกอริทึมบีบอัด·คลายบีบอัดที่ผ่านการพิสูจน์แล้วจะปลอดภัย แต่ยังมีช่องโหว่อยู่ใน archive parser และชั้น runtime ที่ไม่ได้ผ่านการพิสูจน์
  • สุดท้ายแล้ว แม้การตรวจพิสูจน์เชิงรูปแบบจะทรงพลัง แต่ก็ไม่อาจรับประกันเสถียรภาพของทั้งระบบได้ หากยังไม่ทำให้ Trusted Computing Base (TCB) ปลอดภัย

บั๊กที่พบในโปรแกรมซึ่งผ่านการตรวจพิสูจน์ด้วย Lean

  • เมื่อทำ fuzzing กับอิมพลีเมนเทชัน zlib ที่ผ่านการตรวจพิสูจน์เชิงรูปแบบด้วย Lean ก็พบ heap buffer overflow ใน Lean 4 runtime
    • ในโค้ดแอปพลิเคชันที่ผ่านการพิสูจน์แล้วไม่พบช่องโหว่ด้านหน่วยความจำ
    • แต่เกิด overflow ในฟังก์ชัน lean_alloc_sarray ของ Lean runtime และส่งผลกับ Lean 4 ทุกเวอร์ชัน
  • ทำการ fuzzing มากกว่า 100 ล้านครั้งโดยใช้ AI-based fuzzer Claude, AFL++, AddressSanitizer, Valgrind, UBSan ฯลฯ
    • รัน fuzzer แบบขนาน 16 ตัวกับพื้นผิวโจมตี 6 จุดของ lean-zip เช่น การบีบอัด·คลายบีบอัด·การจัดการ archive
    • ภายใน 19 ชั่วโมง พบอินพุตที่ทำให้ crash 4 รายการ และช่องโหว่ด้านหน่วยความจำ 1 รายการ
  • ยืนยันได้ว่ามี บั๊กหลัก 2 รายการ
    • heap buffer overflow ใน lean_alloc_sarray ของ Lean runtime
    • การปฏิเสธการให้บริการ (DoS) จาก Out-of-Memory ในโมดูล Archive.lean ของ lean-zip
  • เห็นได้ถึง ข้อจำกัดของการตรวจพิสูจน์เชิงรูปแบบ
    • แม้อัลกอริทึมบีบอัด·คลายบีบอัดของ lean-zip จะผ่านการพิสูจน์ครบถ้วน แต่ archive parser (Archive.lean) ไม่ได้ผ่านการพิสูจน์ จึงมีช่องโหว่ DoS อยู่
    • บั๊กรันไทม์เป็นปัญหาภายใน Trusted Computing Base และกระทบทุกโปรแกรม Lean
  • โดยสรุป การตรวจพิสูจน์เชิงรูปแบบของ Lean แสดงให้เห็นถึงเสถียรภาพของโค้ดแอปพลิเคชันได้ แต่ใน องค์ประกอบที่อยู่นอกขอบเขตการพิสูจน์ ก็ยังมีช่องโหว่อยู่
    • การพิสูจน์มีพลังเฉพาะในขอบเขตที่นำไปใช้เท่านั้น และ การทำให้ชั้นฐานที่ต้องเชื่อถือปลอดภัย เป็นสิ่งจำเป็น

ภาพรวมของการทดลอง fuzzing

  • โค้ดเบสเป้าหมาย คืออิมพลีเมนเทชัน zlib ที่ผ่านการพิสูจน์แล้วของ lean-zip
    • ลบ theorem, specification, เอกสาร และ C FFI binding ทั้งหมดออกเพื่อ ให้เหลือเฉพาะโค้ด Lean ล้วน
    • ทำให้ Claude ไม่รับรู้ว่าโค้ดนี้ผ่านการพิสูจน์แล้ว เพื่อลดอคติ

  • สภาพแวดล้อมการทดลอง

    • fuzzer แบบขนาน 16 ตัว รันกับพื้นผิวโจมตี 6 จุด ได้แก่ ZIP, gzip, DEFLATE, tar, tar.gz, compression
    • ใช้งาน AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck, flawfinder ควบคู่กัน
    • รวมการรันทั้งหมด 105,823,818 ครั้ง โดยใช้ไฟล์ seed 359 ไฟล์ รวมถึงไฟล์ exploit ที่สร้างด้วยมือ 48 ไฟล์
    • ภายใน 19 ชั่วโมง พบอินพุตที่ทำให้ crash 4 รายการ และช่องโหว่ด้านหน่วยความจำ 1 รายการ

บั๊ก 1: heap buffer overflow ใน Lean runtime

  • ฟังก์ชันที่มีช่องโหว่: lean_alloc_sarray
    • เป็นฟังก์ชันสำหรับจัดสรร scalar array ทั้งหมด เช่น ByteArray, FloatArray
    • อาจเกิด integer overflow ระหว่างคำนวณ sizeof(lean_sarray_object) + elem_size * capacity

  • สาเหตุของปัญหา

    • เมื่อ capacity เข้าใกล้ SIZE_MAX การบวกจะ overflow ทำให้จัดสรรบัฟเฟอร์ขนาดเล็กเกินจริง
    • หลังจากนั้น caller จะอ่าน n ไบต์เข้าไป จึงเกิด heap buffer overflow

  • เงื่อนไขที่ทำให้เกิดปัญหา

    • เกิดขึ้นเมื่อ nbytes ใน lean_io_prim_handle_read มีค่ามหาศาลผิดปกติ
    • สามารถทำซ้ำได้ด้วยไฟล์ขนาด 156 ไบต์ที่มีค่า compressedSize ใน ZIP64 header เป็น 0xFFFFFFFFFFFFFFFF
    • ส่งผลกับ Lean 4 ทุกเวอร์ชัน รวมถึง nightly ล่าสุด
    • ตัวอย่างโค้ดสำหรับทำซ้ำ
    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
    • เมื่อรันโค้ดข้างต้นจะเกิด overflow ใน lean_alloc_sarray
    • มีการส่ง PR แก้ไข แล้ว

บั๊ก 2: การปฏิเสธการให้บริการ (DoS) ใน archive parser ของ lean-zip

  • ฟังก์ชันที่มีช่องโหว่: readExact (Archive.lean)
    • ใช้ค่าฟิลด์ compressedSize ของ ZIP central directory โดยไม่ตรวจสอบ แล้วนำไปใช้ตรง ๆ
    • เมื่อเรียก h.read ด้วยขนาดที่ใหญ่ผิดปกติ จะทำให้ มีการจัดสรรหน่วยความจำมากเกินไปและเกิด OOM

  • การทำซ้ำปัญหา

    • หากไฟล์ ZIP ขนาด 156 ไบต์อ้างว่ามีขนาดระดับ exabyte หลายหน่วย โปรเซสจะจบการทำงานด้วย INTERNAL PANIC: out of memory
    • unzip ของระบบจะตรวจสอบขนาดใน header แต่ lean-zip ไม่ได้ทำเช่นนั้น

ส่วนที่การตรวจพิสูจน์เชิงรูปแบบมองข้าม

  • สาเหตุของช่องโหว่ DoS

    • โมดูล Archive.lean เป็นพื้นที่ที่ไม่ได้ผ่านการพิสูจน์
    • pipeline การบีบอัด·คลายบีบอัด (เช่น DEFLATE, Huffman, CRC32) ผ่านการพิสูจน์ครบถ้วนและไม่มีปัญหา
    • ช่องโหว่จึงเกิดขึ้นในส่วนที่ไม่ได้มีการพิสูจน์

  • แก่นของปัญหา runtime overflow

    • Lean runtime อยู่ใน Trusted Computing Base (TCB)
    • การพิสูจน์ทั้งหมดของ Lean ตั้งอยู่บนสมมติฐานว่า runtime ถูกต้อง
    • ดังนั้นบั๊กใน runtime จึงส่งผลต่อความปลอดภัยของทุกโปรแกรม Lean

เสถียรภาพของโค้ดที่ผ่านการพิสูจน์แล้ว

  • ผลจากการรัน 105 ล้านครั้ง

    • ในโค้ด C ที่ Lean สร้างขึ้น ไม่พบ heap overflow, use-after-free, stack overflow, UB, การเข้าถึง array เกินขอบเขต เลย
    • ตามการประเมินของ Claude วิเคราะห์ได้ว่าเป็น “หนึ่งในโค้ดเบสที่ปลอดภัยด้านหน่วยความจำมากที่สุด”

  • ผลของระบบชนิดข้อมูลของ Lean

    • ด้วย dependent types และโครงสร้าง well-founded recursion ทำให้สามารถปิดกั้นช่องโหว่ที่พบบ่อยในอิมพลีเมนเทชัน zlib แบบ C/C++ (คลาส CVE) ได้ในระดับโครงสร้าง

  • บทสรุป

    • พื้นที่โค้ดที่ผ่านการพิสูจน์แล้วมีความแข็งแรงมาก และ fuzzer หา error ได้ยาก
    • แต่ในส่วนที่ไม่ได้ผ่านการพิสูจน์และในชั้น runtime ก็ยังมีช่องโหว่อยู่
    • การพิสูจน์ถูกจำกัดด้วยขอบเขตที่นำไปใช้และความปลอดภัยของฐานที่ต้องเชื่อถือ

บทเรียนสำคัญ

  • การตรวจพิสูจน์เชิงรูปแบบ ทรงพลังมากภายในพื้นที่โค้ดที่นำไปใช้ แต่ องค์ประกอบรอบข้างที่ไม่ได้ผ่านการพิสูจน์หรือชั้น runtime อาจคุกคามเสถียรภาพโดยรวมได้
  • การทำให้ Trusted Computing Base ปลอดภัย เป็นสิ่งจำเป็น และ แม้จะเป็นระบบที่ผ่านการพิสูจน์แล้ว ก็ยังคงเหลือคำถามว่า “ใครจะเฝ้าผู้เฝ้ายาม (Quis custodiet ipsos custodes)”

ลิงก์อ้างอิง

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 14 일 전
ความเห็นจาก Hacker News

  • รู้สึกว่าชื่อเรื่องและการวางกรอบประเด็นของบทความนี้แปลก ๆ
    จริง ๆ แล้วผู้เขียนระบุชัดว่าเขาไม่พบบั๊กหรือข้อผิดพลาดในโค้ดที่ได้รับการพิสูจน์แล้ว
    บั๊กสองตัวที่พบนั้นอยู่นอกขอบเขตของการพิสูจน์ โดยตัวหนึ่งคือข้อกำหนดตกหล่น และอีกตัวคือheap overflow ใน C++ runtime
    อยากย้ำว่าบั๊กที่พบอยู่ใน runtime ของ Lean ไม่ใช่ใน kernel ที่ทำหน้าที่ตรวจการพิสูจน์
    ดูได้จากเอกสารของ Lean

    • เวลาพูดถึงบั๊กในระบบที่ผ่านการตรวจพิสูจน์แล้ว ผมคิดว่าควรมองทั้งไบนารีทั้งหมด
      ถ้าคุณเสียบิตคอยน์เพราะ buffer overflow การรู้ว่าบั๊กนั้นอยู่ใน runtime ก็ไม่ได้ช่วยให้สบายใจขึ้น
      อีกอย่าง ถ้าโปรแกรมแครช ผู้ใช้ส่วนใหญ่ก็น่าจะมองว่านั่นคือบั๊ก
      และก็น่าจะมีคนจำนวนไม่น้อยที่รัน Lean ในสภาพแวดล้อม production จริง
    • ตอนเห็นชื่อเรื่องครั้งแรกผมนึกว่ามีบั๊กใน Lean kernel แต่จริง ๆ แล้วปัญหาอยู่ใน Lean runtime และใน lean-zip
      ถ้าไม่ใช่ kernel ก็แทบไม่กระทบต่อความน่าเชื่อถือของตัวการพิสูจน์เอง
    • ข้อกำหนดตกหล่นของ lean-zip เป็นประเด็นสำคัญในเชิงปรัชญาของการตรวจพิสูจน์
      ต่อให้คุณพิสูจน์โปรแกรม “Hello world” คุณก็ต้องระบุข้อกำหนดไม่ใช่แค่ผลลัพธ์ แต่รวมถึงผลข้างเคียงด้วย
      ถ้าเกิด memory corruption ตรงรอยต่อระหว่าง runtime กับ kernel ความน่าเชื่อถือของการพิสูจน์ก็อาจลดลงได้
      สุดท้ายแล้วหัวใจสำคัญคือการนิยามให้ชัดว่า “อะไรคือสิ่งที่ต้องพิสูจน์”
    • ดูรายชื่อบทความในเว็บนี้แล้วตลกดีที่มันเริ่มดูเป็นแนวคลิกเบตมากขึ้นเรื่อย ๆ
      รายการบทความที่เกี่ยวข้อง
    • การเรียกบั๊กใน Lean runtime ว่าเป็นบั๊กของ lean-zip ก็เหมือนกับการเรียกบั๊กใน JRE ว่าเป็นบั๊กของแอป Java
      ดูเหมือนผู้เขียนจงใจชวนให้เข้าใจผิด

  • ผมเองก็เคยมีประสบการณ์คล้ายกันกับโค้ดที่พิสูจน์แล้ว
    ในกรณีของผม ปัญหาไม่ได้อยู่ที่ overflow แต่เป็นข้อบกพร่องของสเปก (spec bug)
    ถ้าสเปกผิด ต่อให้โค้ดและการพิสูจน์สมบูรณ์แบบ มันก็ยังทำงานไม่ตรงกับเจตนาที่ต้องการ
    สุดท้ายความยากของการตรวจพิสูจน์คือการถ่ายทอดเจตนาของมนุษย์ออกมาให้แม่นยำ
    ความเชื่อว่า AI จะมาแก้ปัญหาการตรวจพิสูจน์ได้อย่างสมบูรณ์อาจสร้างความมั่นใจผิด ๆ ได้

    • ผมก็มีประสบการณ์คล้ายกัน
      สเปกที่พิสูจน์ได้ด้วยเครื่องมืออย่าง Lean, TLA+, Z3 มักถูกทำให้ง่ายลงและต้องอาศัยสมมติฐานหลายอย่าง
      แต่ถึงอย่างนั้นมันก็ยังเป็นเครื่องมือที่ทรงพลัง
      มันช่วยบีบขอบเขตของบั๊กในอัลกอริทึมที่ซับซ้อน และทำให้มองเห็นขอบเขตของสเปกได้ชัดขึ้น
      AI ทำให้งานพิสูจน์แบบนี้ง่ายขึ้นมาก
    • คำถามที่ผมสงสัยเสมอคือ “แล้วเราจะเชื่อถือระบบตรวจพิสูจน์เองได้อย่างไร”
      เพราะโปรแกรมอีกตัวที่ใช้ตรวจพิสูจน์โปรแกรม ก็อาจมีบั๊กได้เหมือนกัน
      ความเป็นไปไม่ได้ของการพิสูจน์ตัวเองอย่างสมบูรณ์ทำให้นึกถึงหลักความไม่แน่นอนของไฮเซนเบิร์ก
      สุดท้ายการตรวจพิสูจน์ก็คือกระบวนการเพิ่มความเชื่อมั่นผ่าน “การมี implementation อิสระตัวที่สอง”
    • บั๊กในโค้ดของผมแบ่งได้เป็นสองประเภท
      (1) ทำงานไม่ตรงกับที่ตั้งใจ
      (2) ทำงานตรงตามที่ตั้งใจ แต่เจตนานั้นผิดตั้งแต่แรก
      proof assistant ช่วยป้องกันแบบ (1) ได้ แต่ป้องกันแบบ (2) ไม่ได้
      กล่าวคือ ความถูกต้องสมบูรณ์ของการออกแบบนั้นพิสูจน์ไม่ได้
      การตรวจพิสูจน์ทุกอย่างแบบ seL4 ทั้งแพงและใช้เวลามากเกินไป
    • ผมคิดว่าเราต้องมีวิธีตรวจพิสูจน์ตัวสเปกเอง
      วิธีที่เหมาะที่สุดคือการผสาน ตรรกะเชิงรูปนัย + การคิดแบบ adversarial เพื่อแจกแจงให้ครบทั้งสิ่งที่โปรแกรมควรทำและสิ่งที่ไม่ควรทำ

  • ชื่อเรื่องให้ความรู้สึกเหมือนคลิกเบต
    ส่วนที่พิสูจน์แล้วไม่มีบั๊ก แต่ไม่รู้ว่าทำไมถึงตั้งชื่อออกมาแบบนี้
    ใน HN ผมอยากเห็นโพสต์ที่ยึดข้อเท็จจริงมากกว่า อันนี้เลยรู้สึกเสียเวลา

    • ถ้าเป็นซอฟต์แวร์ที่ผ่านการตรวจพิสูจน์แล้ว การบอกว่า “นับเฉพาะบั๊กที่ขัดกับการพิสูจน์เท่านั้นถึงจะเรียกว่าบั๊ก” มันยุติธรรมหรือ?
      เขาโฆษณาว่า “ไม่มีบั๊ก” แต่ในความเป็นจริงหมายถึง “เฉพาะภายในขอบเขตที่สเปกถูกระบุไว้อย่างครบถ้วนเท่านั้น”
      ต่อให้ถูกต้องสมบูรณ์แบบ ในโลกจริงคุณก็อาจถูกต้องแบบตายคาที่ได้ — คือในทางทฤษฎีถูก แต่ในทางปฏิบัติยังพังได้
    • ชื่อเรื่องอาจจะถูกต้องในเชิงเทคนิค แต่ก็ทำให้ปัญหาที่เกิดในโค้ดที่ไม่ได้รับการพิสูจน์ของ lean-zip ดูเหมือนเป็นบั๊กในส่วนที่ผ่านการพิสูจน์แล้ว
    • โดยสรุป ข้อความที่ว่า “ควรระบุขอบเขตของส่วนที่ได้รับการพิสูจน์ให้ชัดเจน” นั้นน่าสนใจและสมเหตุสมผล
    • บั๊กตัวที่สองดูเหมือนเป็นการมโนขึ้นมาโดยไม่มีหลักฐานรองรับ
      ไม่มีการอ้างอิงโค้ด และถ้าไปดูโค้ดจริงจะเห็นว่าเป็นความเข้าใจผิด
    • สุดท้าย lean-zip ก็เป็นแค่ Zlib binding เท่านั้น

  • ปัญหานี้เจอบ่อยมากในการตรวจพิสูจน์ระบบกระจาย
    การพิสูจน์ใช้ได้เฉพาะภายใต้เงื่อนไขบางอย่างเท่านั้น และความล้มเหลวที่น่าสนใจมักเกิดตรงขอบเขตเหล่านั้น
    TLA+ ก็เหมือนกัน ถ้าความเป็นจริงหลุดออกจากสมมติฐาน การพิสูจน์ก็ไม่มีความหมาย
    สิ่งที่ผมอยากได้คือความสามารถในการระบุ operating envelope แบบกลไก และเฝ้าตรวจมันใน runtime

    • ผมเองก็เคยพบบั๊กของ ฮาร์ดแวร์ CPU โดยตรง
      แต่บั๊กส่วนใหญ่ไม่ได้เกิดจากฮาร์ดแวร์ เกิดจากคนไม่อ่านเอกสารมากกว่า
      แค่ทำ formal modeling ก็ช่วยลดจำนวนบั๊กได้มหาศาลแล้ว

  • นี่เป็นข่าวดีที่คาดเดาได้และเป็นข่าวดีจริง ๆ
    มันหมายความว่า LLM สามารถสร้างโค้ดที่ผ่านการตรวจพิสูจน์เชิงรูปนัยได้
    จากนี้บั๊กจะค่อย ๆ ย้ายไปอยู่ที่ชั้นฮาร์ดแวร์มากขึ้น
    สุดท้ายเราจะต้องมีการทำข้อกำหนดฮาร์ดแวร์ให้อยู่ในรูปแบบเชิงรูปนัย
    ถ้าผู้ผลิตไม่เปิดเผยสิ่งนี้ ก็อาจเกิดความขัดแย้งกับชุมชนได้
    ในระยะยาว มันอาจแตกออกเป็นสองทางคือ การสูญพันธุ์ของช่องโหว่ หรือ การใส่ช่องโหว่โดยเจตนา

  • ตอนแรกผมนึกว่าผู้เขียนไม่ได้ทดสอบส่วนที่ผ่านการพิสูจน์
    แต่พออ่านไปเรื่อย ๆ ก็พบว่าบั๊กถูกพบในส่วนนอกขอบเขตการพิสูจน์
    เพราะงั้นชื่อเรื่องเลยให้ความรู้สึกว่าพูดเกินจริงไปหน่อย

    • ตัวผู้เขียนบทความเข้ามาคอมเมนต์เอง
      เขายืนยันว่าถ้าจะพูดถึงบั๊กของระบบที่ตรวจพิสูจน์แล้ว ก็ควรนับทั้งไบนารีทั้งหมด
      และเขาเปิดเผยว่าพบอินพุตที่ทำให้เกิดแครชได้จริงในส่วน parse compressed header ของ Archive.lean

  • ทำให้นึกถึงคำพูดดังของ Donald Knuth
    “ระวังไว้ โค้ดข้างบนนี้อาจมีบั๊กได้ ฉันแค่พิสูจน์ว่ามันถูกต้อง แต่ยังไม่ได้ลองรันมัน” คือคำเตือนนั้นเอง

  • การไม่ได้ตรวจพิสูจน์ parser ดูเป็นความผิดพลาดครั้งใหญ่
    การ parse ฟอร์แมตไบนารีเป็นพื้นที่อันตรายเสมอ

  • ประเด็นสำคัญคือ AI agent ได้ร่วมงานกับ fuzzer เพื่อพบ heap buffer overflow ใน Lean
    นี่ถือเป็นความสำเร็จที่ค่อนข้างใหญ่

    • ผมคิดว่าเป็นการค้นพบที่มีประโยชน์มากจริง ๆ

  • ส่วนที่ Claude บอกว่า “นี่เป็นหนึ่งในโค้ดเบสที่ปลอดภัยด้านหน่วยความจำที่สุดเท่าที่ผมเคยวิเคราะห์” น่าประทับใจดี
    แต่ก็ฟังดูเหมือนมุกที่ว่าโค้ดนี้คือโค้ดแรกที่ Claude เคยวิเคราะห์

    • เป็นไปไม่ได้ที่ Claude ซึ่งผ่านการฝึกแบบ RL มาอย่างกว้างขวาง จะเพิ่งวิเคราะห์โค้ดเป็นครั้งแรก
      นั่นแหละคือเหตุผลที่มันเก่งแบบนี้
    • หรือบางที Claude อาจกำลังทำอะไรบางอย่างแบบลับ ๆ ที่เราไม่รู้ก็ได้ 😄