Lean đã chứng minh tính đúng đắn của chương trình, nhưng vẫn phát hiện lỗi bên trong

(kirancodes.me)

1 điểm bởi GN⁺ 6 ngày trước | 1 bình luận | Chia sẻ qua WhatsApp

Kết quả fuzzing một bản triển khai zlib đã được kiểm chứng hình thức cho thấy tràn bộ đệm heap trong lean_alloc_sarray của runtime Lean 4
Sau hơn 100 triệu lần kiểm thử bằng AI fuzzer Claude, AFL++, AddressSanitizer và các công cụ khác, đã xác nhận 4 crash và 1 lỗ hổng bộ nhớ
Các vấn đề được phát hiện chia thành hai loại: tràn trong runtime và từ chối dịch vụ (DoS) dựa trên Out-of-Memory trong Archive.lean
Thuật toán nén/giải nén đã được kiểm chứng là an toàn, nhưng lỗ hổng vẫn tồn tại trong trình phân tích archive và lớp runtime chưa được kiểm chứng
Kết quả cho thấy kiểm chứng hình thức rất mạnh, nhưng không thể đảm bảo độ ổn định của toàn hệ thống nếu chưa bảo đảm an toàn cho Trusted Computing Base (TCB)

Lỗi được phát hiện trong chương trình đã vượt qua kiểm chứng của Lean

Kết quả fuzzing một bản triển khai zlib được kiểm chứng hình thức bằng Lean đã phát hiện tràn bộ đệm heap trong runtime Lean 4
- Mã ứng dụng đã được kiểm chứng không có lỗ hổng bộ nhớ
- Tuy nhiên, tràn xảy ra trong hàm lean_alloc_sarray của runtime Lean và ảnh hưởng đến mọi phiên bản Lean 4
Đã thực hiện hơn 100 triệu lần fuzzing bằng AI-based fuzzer Claude, AFL++, AddressSanitizer, Valgrind, UBSan và các công cụ khác
- Chạy 16 fuzzer song song trên 6 bề mặt tấn công của lean-zip, gồm nén, giải nén và xử lý archive
- Trong 19 giờ, phát hiện 4 đầu vào gây crash và 1 lỗ hổng bộ nhớ
Xác nhận hai lỗi chính
- Tràn bộ đệm heap trong lean_alloc_sarray của runtime Lean
- Từ chối dịch vụ (DoS) dựa trên Out-of-Memory trong module Archive.lean của lean-zip
Giới hạn của kiểm chứng hình thức đã bộc lộ
- Thuật toán nén/giải nén của lean-zip được kiểm chứng hoàn toàn, nhưng trình phân tích archive (Archive.lean) không được kiểm chứng nên tồn tại lỗ hổng DoS
- Lỗi runtime là vấn đề bên trong Trusted Computing Base, nên ảnh hưởng đến mọi chương trình Lean
Kết luận, kiểm chứng hình thức của Lean đã chứng minh được độ ổn định của mã ứng dụng, nhưng các thành phần nằm ngoài phạm vi kiểm chứng vẫn có thể chứa lỗ hổng
- Kiểm chứng chỉ mạnh trong đúng phạm vi được áp dụng, và việc bảo đảm an toàn cho tầng tin cậy nền tảng là bắt buộc

Tổng quan thí nghiệm fuzzing

Codebase mục tiêu là bản triển khai zlib đã được kiểm chứng của lean-zip
- Loại bỏ toàn bộ định lý (theorem), đặc tả (specification), tài liệu và C FFI binding để chỉ giữ lại mã Lean thuần
- Không để Claude biết rằng mã đã được kiểm chứng nhằm tránh thiên lệch
Môi trường thí nghiệm
- 16 fuzzer song song được chạy trên 6 bề mặt tấn công gồm ZIP, gzip, DEFLATE, tar, tar.gz, compression
- Kết hợp AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck, flawfinder và các công cụ khác
- Bao gồm 48 tệp exploit thủ công, tổng cộng 105,823,818 lần thực thi, sử dụng 359 tệp seed
- Trong 19 giờ, phát hiện 4 đầu vào gây crash và 1 lỗ hổng bộ nhớ

Lỗi 1: Tràn bộ đệm heap trong runtime Lean

Hàm bị ảnh hưởng: lean_alloc_sarray
- Hàm cấp phát mọi mảng scalar như ByteArray, FloatArray v.v.
- Có thể xảy ra tràn số nguyên khi tính sizeof(lean_sarray_object) + elem_size * capacity
Nguyên nhân
- Khi capacity tiến sát SIZE_MAX, phép cộng bị tràn khiến chỉ một bộ đệm nhỏ được cấp phát
- Sau đó, bên gọi đọc vào n byte, dẫn tới tràn bộ đệm heap
Điều kiện kích hoạt
- Xảy ra khi nbytes trong lean_io_prim_handle_read có giá trị cực lớn
- Có thể tái hiện bằng một tệp 156 byte với compressedSize trong header ZIP64 là 0xFFFFFFFFFFFFFFFF
- Ảnh hưởng đến mọi phiên bản Lean 4, bao gồm cả nightly mới nhất
- Ví dụ mã tái hiện
```
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
```
- Khi chạy đoạn mã trên, tràn xảy ra trong lean_alloc_sarray
- Đã có PR sửa lỗi được gửi lên

Lỗi 2: Từ chối dịch vụ (DoS) trong trình phân tích archive của lean-zip

Hàm bị ảnh hưởng: readExact (Archive.lean)
- Sử dụng trực tiếp trường compressedSize của ZIP central directory mà không kiểm tra
- Khi gọi h.read, nó yêu cầu một kích thước lớn bất thường, gây cấp phát bộ nhớ quá mức và dẫn đến OOM
Tái hiện lỗi
- Nếu một tệp ZIP 156 byte tự khai báo kích thước tới hàng exabyte, tiến trình sẽ kết thúc với INTERNAL PANIC: out of memory
- unzip của hệ thống có kiểm tra kích thước trong header, nhưng lean-zip thì không

Những gì kiểm chứng hình thức đã bỏ sót

Nguyên nhân của lỗ hổng DoS
- Module Archive.lean nằm ngoài vùng được kiểm chứng
- Pipeline nén/giải nén như DEFLATE, Huffman, CRC32 đều được kiểm chứng hoàn toàn và không có vấn đề
- Lỗ hổng phát sinh ở phần không được kiểm chứng
Bản chất của lỗi tràn trong runtime
- Runtime Lean thuộc Trusted Computing Base (TCB)
- Mọi chứng minh trong Lean đều giả định runtime là chính xác
- Vì vậy, lỗi runtime ảnh hưởng đến độ an toàn của mọi chương trình Lean

Độ ổn định của mã đã được kiểm chứng

Kết quả của 105 triệu lần thực thi
- Trong mã C do Lean sinh ra, không có tràn heap, use-after-free, tràn stack, UB hay vượt chỉ số mảng
- Theo đánh giá của Claude, đây là “một trong những codebase an toàn bộ nhớ nhất”
Tác động của hệ thống kiểu trong Lean
- Dependent types và cấu trúc well-founded recursion giúp chặn về mặt cấu trúc các kiểu lỗ hổng CVE thường gặp trong các bản triển khai zlib viết bằng C/C++
Kết luận
- Vùng mã đã được kiểm chứng rất vững chắc và fuzzer khó tìm ra lỗi
- Tuy nhiên, các phần chưa được kiểm chứng và lớp runtime vẫn còn lỗ hổng
- Kiểm chứng bị giới hạn bởi phạm vi áp dụng và độ an toàn của nền tảng tin cậy

Bài học cốt lõi

Kiểm chứng hình thức rất mạnh trong phần mã đã được áp dụng, nhưng các thành phần ngoại vi chưa được kiểm chứng hoặc lớp runtime vẫn có thể đe dọa độ ổn định tổng thể
Bảo đảm an toàn cho Trusted Computing Base là điều bắt buộc, và ngay cả với hệ thống đã được kiểm chứng, câu hỏi “ai sẽ giám sát những người giám sát (Quis custodiet ipsos custodes)” vẫn còn đó

Liên kết tham khảo

1 bình luận

GN⁺ 6 ngày trước

Ý kiến trên Hacker News

Tiêu đề và cách giật tít của bài này có vẻ hơi kỳ
Thực ra tác giả nói rõ rằng họ không tìm thấy bug hay lỗi nào trong phần mã đã được chứng minh
Hai bug được phát hiện đều nằm ngoài phạm vi chứng minh: một là thiếu đặc tả, cái còn lại là tràn bộ nhớ heap trong runtime C++
Cần nhấn mạnh rằng bug được tìm thấy ở runtime của Lean, chứ không phải kernel thực hiện việc kiểm chứng
Xem tài liệu Lean
- Khi bàn về bug trong một hệ thống đã được kiểm chứng, tôi nghĩ phải xét toàn bộ binary
  Nếu bạn mất bitcoin vì tràn bộ đệm, thì việc bug đó nằm ở runtime cũng chẳng an ủi được gì
  Và nếu chương trình bị crash, đa số người dùng vẫn sẽ xem đó là bug
  Cũng sẽ có khá nhiều người chạy Lean trong môi trường production thực tế
- Chỉ đọc tiêu đề thì tôi tưởng Lean kernel có bug, nhưng thực tế vấn đề được tìm thấy ở Lean runtime và lean-zip
  Nếu không phải kernel thì độ tin cậy của bản thân chứng minh không bị ảnh hưởng nhiều
- Việc thiếu đặc tả trong lean-zip là một vấn đề quan trọng về mặt triết lý kiểm chứng
  Ngay cả khi kiểm chứng một chương trình “Hello world”, bạn cũng phải đặc tả không chỉ đầu ra mà cả tác dụng phụ
  Nếu hư hỏng bộ nhớ xảy ra ở ranh giới giữa runtime và kernel, độ tin cậy của chứng minh có thể bị suy giảm
  Cuối cùng, điều cốt lõi là phải định nghĩa rõ “cần kiểm chứng cái gì”
- Nhìn danh sách bài trên site này, thấy nó ngày càng mang tính câu view cũng khá buồn cười
  Danh sách bài liên quan
- Gọi bug trong Lean runtime là bug của lean-zip cũng giống như gọi bug trong JRE là bug của một ứng dụng Java
  Có vẻ như tác giả cố tình dẫn người đọc hiểu sai
Tôi cũng từng có trải nghiệm tương tự với mã đã được chứng minh
Trường hợp của tôi không phải tràn số mà là lỗi đặc tả (spec bug)
Nếu đặc tả sai, thì dù mã và chứng minh có hoàn hảo, chương trình vẫn hoạt động khác với ý định ban đầu
Cuối cùng, cái khó của kiểm chứng là diễn đạt chính xác ý định của con người
Niềm tin rằng AI sẽ giải quyết hoàn toàn bài toán kiểm chứng có thể tạo ra sự tự tin sai lầm
- Tôi cũng có trải nghiệm tương tự
  Những đặc tả có thể chứng minh bằng Lean, TLA+, Z3 thường đã được đơn giản hóa và cần rất nhiều giả định
  Dù vậy đây vẫn là công cụ rất mạnh
  Nó giúp thu hẹp bug trong các thuật toán phức tạp và nhìn rõ ranh giới của đặc tả
  Nhờ AI mà kiểu công việc chứng minh này đã dễ hơn rất nhiều
- Điều tôi luôn băn khoăn là “làm sao tin được chính hệ thống kiểm chứng”
  Một chương trình dùng để kiểm chứng chương trình khác thì rốt cuộc cũng có thể có bug
  Việc tự kiểm chứng hoàn toàn là bất khả thi khiến tôi liên tưởng đến nguyên lý bất định của Heisenberg
  Cuối cùng, kiểm chứng là quá trình tăng độ tin cậy bằng “một triển khai độc lập thứ hai”
- Bug trong mã của tôi chia thành hai loại
  (1) hoạt động khác với điều tôi định làm
  (2) hoạt động đúng như ý định, nhưng bản thân ý định đó lại sai
  Trợ lý chứng minh có thể ngăn (1), nhưng không thể ngăn (2)
  Nói cách khác, tính đúng đắn của thiết kế thì không thể chứng minh được
  Việc kiểm chứng mọi thứ như seL4 là quá tốn kém và mất nhiều thời gian
- Tôi nghĩ cần có cách kiểm chứng chính bản thân đặc tả
  Lý tưởng nhất là kết hợp logic hình thức + tư duy đối kháng (adversarial thinking) để liệt kê đầy đủ chương trình phải làm gì và không được làm gì
Tiêu đề này tạo cảm giác như câu view
Phần đã được chứng minh thì không có bug, vậy mà lại viết như thế này thì tôi không hiểu nổi
Trên HN tôi muốn đọc những bài dựa trên sự thật, còn bài này chỉ tốn thời gian
- Có công bằng không khi nói rằng trong phần mềm đã được kiểm chứng, “chỉ những bug vi phạm chứng minh mới được tính là bug”?
  Người ta quảng bá là “không có bug”, nhưng thực tế chỉ là “trong phạm vi mà đặc tả đã diễn đạt hoàn chỉnh”
  Dù hoàn toàn đúng đi nữa thì trong thực tế vẫn có thể đúng nhưng chết — tức là đúng về lý thuyết nhưng ngoài đời thì vẫn hỏng
- Tiêu đề đúng về mặt kỹ thuật, nhưng lại diễn tả sự cố trong mã chưa được kiểm chứng của lean-zip như thể đó là bug ở phần đã được chứng minh
- Xét cho cùng, thông điệp “hãy làm rõ phạm vi của phần đã được chứng minh” là điều vừa thú vị vừa hợp lý
- Bug thứ hai có vẻ như bị dựng lên mà không có căn cứ
  Không có tham chiếu mã nguồn nào, và nếu xem mã thật thì sẽ thấy đó là hiểu nhầm
- Cuối cùng thì lean-zip chỉ đơn giản là binding cho Zlib
Vấn đề này cũng thường gặp trong kiểm chứng hệ thống phân tán
Chứng minh chỉ có hiệu lực trong một số điều kiện nhất định (phạm vi vận hành), còn các lỗi thú vị thì lại xảy ra ở ranh giới đó
TLA+ cũng vậy: khi thực tế lệch khỏi các giả định, chứng minh trở nên vô nghĩa
Điều tôi muốn là khả năng khai báo phạm vi vận hành một cách cơ giới và giám sát nó lúc runtime
- Tôi cũng từng tự mình phát hiện bug phần cứng của CPU
  Nhưng phần lớn bug không đến từ phần cứng mà do con người không đọc tài liệu
  Chỉ cần mô hình hóa hình thức thôi cũng có thể giảm số bug đi rất nhiều
Đây là một tin tốt theo kiểu có thể đoán trước
Điều đó có nghĩa là LLM có thể tạo ra mã vượt qua kiểm chứng hình thức
Trong tương lai, bug sẽ dần chuyển xuống tầng phần cứng
Rốt cuộc sẽ cần đến đặc tả hình thức cho phần cứng
Nếu nhà sản xuất không công khai chúng, có thể sẽ phát sinh xung đột với cộng đồng
Về dài hạn, có lẽ sẽ tách thành hai hướng: sự tuyệt chủng của lỗ hổng hoặc việc cài cắm có chủ đích
Lúc đầu tôi nghĩ tác giả đã không kiểm thử phần được chứng minh
Nhưng đọc tiếp thì thấy bug được phát hiện ở ngoài phạm vi chứng minh
Vì thế tiêu đề mang lại cảm giác hơi cường điệu
- Chính tác giả bài viết đã vào bình luận
  Họ lập luận rằng nếu nói đến bug trong một hệ thống đã được kiểm chứng thì phải xét toàn bộ binary
  Họ cũng nói rằng thực sự đã tìm được một đầu vào gây crash ở phần phân tích header nén của Archive.lean
Tôi nhớ đến câu nói nổi tiếng của Donald Knuth
“Hãy cẩn thận, đoạn mã trên có thể có bug; tôi chỉ mới chứng minh nó đúng thôi, chứ chưa chạy thử”
Việc không kiểm chứng parser có vẻ là một sai lầm lớn
Phân tích định dạng nhị phân lúc nào cũng là khu vực nguy hiểm
Điểm cốt lõi là tác nhân AI đã phối hợp với fuzzer để phát hiện tràn bộ đệm heap trong Lean
Đây là một thành tựu khá lớn
- Tôi nghĩ đây là một phát hiện thực sự hữu ích
Phần Claude nói rằng “đây là một trong những codebase an toàn bộ nhớ nhất mà tôi từng phân tích” khá ấn tượng
Nhưng nghe cũng như một câu đùa kiểu đây là code đầu tiên Claude từng phân tích
- Claude được huấn luyện rất rộng bằng RL thì khó mà đây là code đầu tiên nó phân tích
  Đó cũng chính là lý do nó làm tốt như vậy
- Biết đâu Claude đang âm thầm làm gì đó mà chúng ta không biết 😄

Lean đã chứng minh tính đúng đắn của chương trình, nhưng vẫn phát hiện lỗi bên trong

Lỗi được phát hiện trong chương trình đã vượt qua kiểm chứng của Lean

Tổng quan thí nghiệm fuzzing

Môi trường thí nghiệm

Lỗi 1: Tràn bộ đệm heap trong runtime Lean

Nguyên nhân

Điều kiện kích hoạt

Lỗi 2: Từ chối dịch vụ (DoS) trong trình phân tích archive của lean-zip

Tái hiện lỗi

Những gì kiểm chứng hình thức đã bỏ sót

Nguyên nhân của lỗ hổng DoS

Bản chất của lỗi tràn trong runtime

Độ ổn định của mã đã được kiểm chứng

Kết quả của 105 triệu lần thực thi

Tác động của hệ thống kiểu trong Lean

Kết luận

Bài học cốt lõi

Liên kết tham khảo

Bài viết liên quan

1 bình luận

Ý kiến trên Hacker News