Công nghệ xác minh Rust, áp dụng cho mã hệ thống mức thấp

Công cụ Verus để xác minh tính đúng đắn của mã Rust

• Verus là công cụ để xác minh tính đúng đắn của mã viết bằng Rust.
• Nhà phát triển mô tả đặc tả mà mã cần thực hiện, và Verus sẽ kiểm tra tĩnh xem mã Rust có thể chạy có luôn đáp ứng đúng đặc tả đó trong mọi trường hợp thực thi có thể hay không.
• Thay vì thêm kiểm tra tại thời gian chạy, Verus dựa vào một bộ giải mạnh mẽ để chứng minh mã có đúng hay không.
• Verus hiện tại hỗ trợ một tập con của Rust (đang mở rộng), và trong một số trường hợp cho phép nhà phát triển kiểm tra tĩnh độ đúng đắn của mã vượt ra ngoài hệ thống kiểu chuẩn của Rust (ví dụ: thao tác con trỏ thô).

Tình trạng hiện tại của Verus

• Verus đang được phát triển tích cực.
• Các tính năng có thể bị hỏng hoặc bị thiếu, và tài liệu vẫn còn chưa hoàn chỉnh.
• Nếu muốn thử Verus, bạn nên chuẩn bị tinh thần để nhận hỗ trợ trên Zulip.

Dùng thử Verus

• Để thử Verus trong trình duyệt, hãy truy cập Verus Playground.
• Đối với phát triển phức tạp hơn, hãy làm theo hướng dẫn cài đặt, bắt đầu bằng hướng dẫn và tham khảo, sau đó xem các tài liệu bên dưới.

Tài liệu của Verus

• Hướng dẫn và tài liệu tham khảo
• Tài liệu API cho thư viện chuẩn Verus
• Hướng dẫn xác minh mã song song
• Mục tiêu dự án
• Đóng góp cho Verus
• Giấy phép

Liên hệ, báo cáo issue, bắt đầu thảo luận

• Hãy báo cáo issue, bắt đầu thảo luận trên GitHub, hoặc tham gia Zulip để thảo luận trực tiếp và nhận hỗ trợ khi cần.
• Sử dụng issue trên GitHub cho các lỗi đã xác nhận của tính năng hiện có; hãy dùng GitHub Discussions cho các cuộc trao đổi mở hơn về yêu cầu tính năng và tính năng dự kiến.
• Sự đóng góp được chào đón, nếu bạn muốn đóng góp mã hãy xem các mẹo đóng góp cho Verus.

Ý kiến của GN+

• Rust vốn là ngôn ngữ nổi tiếng phù hợp với lập trình hệ thống, bảo đảm an toàn và hiệu năng, và Verus có vẻ là một dự án có thể tăng cường thêm những ưu điểm đó của Rust. Đặc biệt, khả năng xác minh lập trình song song của dự án trông cực kỳ thú vị.

• Tuy nhiên đây vẫn dường như là giai đoạn đầu và cú pháp Rust được hỗ trợ có vẻ còn hạn chế, vì vậy áp dụng vào môi trường production thực tế có vẻ cần thêm thời gian phát triển. Nhưng vì tầm quan trọng của việc bảo đảm an toàn mã thông qua phân tích tĩnh trước, triển vọng phát triển tiếp theo nhìn chung vẫn rất khả quan.

• Vì đang ở giai đoạn đầu nên vẫn còn thiếu tài liệu và cú pháp được hỗ trợ còn hạn chế, và cần được cải thiện thêm; nhưng về dài hạn, đây có vẻ sẽ là dự án giữ vai trò quan trọng trong hệ sinh thái Rust. Đặc biệt, dự kiến sẽ có mức độ ứng dụng cao trong các lĩnh vực cần độ tin cậy cao như lập trình hệ thống hoặc blockchain.

[GN⁺]

Bình luận Hacker News

• Đã viết một Kubernetes controller được xác minh chính thức bằng Verus
  • Có thể chứng minh tính liveness rằng controller cuối cùng sẽ điều phối cluster về desired state đã yêu cầu
  • Việc chỉ định tính chính xác có nhiều điểm tinh tế và sắc thái (desired state thay đổi nhanh, tính bất đồng bộ, lỗi, v.v.)
  • Mã nằm tại GitHub link và liên kết với một bài báo dự kiến đăng tại OSDI 2024
• Bước đi nhỏ hướng tới Verus: có thể thêm precondition và postcondition bằng debug_assert của Rust
  • Trình biên dịch Rust mặc định loại bỏ chúng trong bản dựng production
  • Có ví dụ trong hướng dẫn Verus và ví dụ kiểm tra runtime dùng debug_assert
• Một câu hỏi cho người mới về khác biệt giữa "xác minh độ đúng của code" và "chứng minh độ đúng của code"
  • Tò mò có tài liệu học tập tốt nào về việc "chứng minh" code cho lập trình viên thực hành có nền tảng CS/toán học không mạnh mẽ không
  • Rất tò mò tại sao "zero-knowledge" lại quan trọng và tại sao nó lại liên quan nhiều như vậy
• Rust chưa có chuẩn này như C/C++, Common Lisp, Ada/SPARK2014
  • Đây là một mục tiêu vẫn đang thay đổi khi so sánh với các công cụ verification được xây dựng cho Ada/SPARK2014, v.v.
• Dafny là một ngôn ngữ lập trình "verification-aware" có thể biên dịch sang Rust (GitHub link)
• Một trong những contributor chính đã có một bài nói rất hay về Verus tại Rust meetup ở Zurich (YouTube link)
  • Code kiểu "ghost" khớp rất gọn gàng với chương trình (gợi nhớ chút về Ada)
• So sánh Verus và SPARK
  • Có phải cùng một loại verifier thông dụng không? Ngoài việc Verus là verifier cho Rust chứ không phải cho Ada, ngoài ra còn khác gì nữa?
• Có ai giỏi Verus có thể so sánh hiệu năng và khả năng biểu đạt giữa Verus và Lean4 không?
  • Tôi hiểu rằng Verus là công cụ verification dựa trên SMT và Lean là proof assistant tương tác, đồng thời cũng là công cụ dựa trên SMT
  • Tuy nhiên vì tôi hiểu về verification hình thức còn hạn chế, tốt hơn là nghe ý kiến của người giỏi formal methods cho phần mềm
• Verus và Kani có liên quan gì không? Hoặc có hoạt động khác nhau không? (Kani GitHub link)
• Có cách nào triển khai để code đầu ra vẫn là một mã Rust hợp lệ có thể biên dịch bằng bộ công cụ Rust vanilla không?