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

 (github.com/verus-lang)
1 điểm bởi GN⁺ 2024-05-06 | 1 bình luận | Chia sẻ qua WhatsApp
  • Verus là công cụ xác minh tính đúng đắn của mã viết bằng Rust; khi nhà phát triển đặc tả điều mà mã cần thực hiện, công cụ sẽ kiểm tra tĩnh xem mã Rust có thể thực thi đó có thỏa mãn đặc tả trong mọi khả năng thực thi hay không
  • Thay vì thêm kiểm tra ở thời gian chạy, công cụ dùng solver mạnh để chứng minh mã là đúng, và hiện mới chỉ hỗ trợ một phần của Rust
  • Trong một số trường hợp, công cụ còn có thể kiểm tra tĩnh cả tính đúng đắn của mã thao tác với raw pointer, vượt ra ngoài hệ thống kiểu chuẩn của Rust
  • Dự án hiện đang được phát triển tích cực; có thể có tính năng bị hỏng hoặc còn thiếu, và tài liệu cũng chưa hoàn chỉnh, nên người dùng cần sẵn sàng nhờ hỗ trợ trên Zulip
  • Verus Playground trên trình duyệt, hướng dẫn cài đặt, tutorial và tài liệu tham chiếu, tài liệu API thư viện chuẩn, hướng dẫn xác minh mã đồng thời, cùng các ví dụ và bài kiểm thử được cung cấp như lộ trình học tập và thử nghiệm

Verus xác minh điều gì

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

Trạng thái phát triển và lưu ý khi sử dụng

  • Verus là dự án đang được phát triển tích cực
  • Có thể có tính năng bị hỏng hoặc còn thiếu
  • Tài liệu vẫn chưa hoàn chỉnh
  • Nếu muốn thử Verus, bạn nên sẵn sàng nhờ hỗ trợ trên Zulip
  • Cộng đồng Verus đã công bố nhiều bài nghiên cứu, và nhiều dự án trong công nghiệp lẫn học thuật đang sử dụng Verus
  • Có thể xem danh sách liên quan tại trang publications and projects

Cách bắt đầu và công cụ phát triển

  • Nếu muốn thử Verus trên trình duyệt, bạn có thể dùng Verus Playground
  • Để phát triển nghiêm túc hơn, bạn cần làm theo hướng dẫn cài đặt
  • Việc học có thể bắt đầu từ Tutorial and reference
  • Verus cũng hỗ trợ trình định dạng tự động cho mã Verus là verusfmt

Tài liệu và tài nguyên học tập

Ví dụ và tham gia cộng đồng

  • Các ví dụ sử dụng Verus cũng cung cấp nhiều điểm khởi đầu ngoài tài liệu
    • Publications and projects: các ấn phẩm và dự án sử dụng Verus
    • Videos, slides, and exercises: video, slide và bài tập của khóa tutorial Verus kéo dài một ngày
    • Standalone examples: các ví dụ độc lập dùng Verus cho những tác vụ nhỏ và cụ thể
    • Small and medium-sized examples: các ví dụ cho thấy nhiều tính năng khác nhau của Verus
    • Unit tests: các bài kiểm thử có chứa ví dụ về cú pháp và tính năng của Verus
  • Có thể báo cáo vấn đề và thảo luận trên GitHub hoặc Zulip
  • Với yêu cầu tính năng và thảo luận mở, dự án dùng GitHub discussions; còn các lỗi có thể tái hiện của chức năng hiện có thì được đưa vào GitHub issues
  • Nếu muốn đóng góp mã, bạn có thể tham khảo hướng dẫn trong Đóng góp cho Verus

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-05-06
Ý kiến trên Hacker News

  • Đã thử viết một Kubernetes controller được kiểm chứng hình thức bằng Verus
    Về cơ bản có thể chứng minh các thuộc tính sống như “cuối cùng controller sẽ điều chỉnh cluster về trạng thái mục tiêu đã được yêu cầu”
    Tuy vậy, nếu trạng thái mục tiêu thay đổi nhanh, cộng thêm tính bất đồng bộ, lỗi, v.v. thì ngay cả việc đặc tả thế nào là “đúng” cũng có nhiều điểm tinh tế
    Mã nguồn: https://github.com/vmware-research/verifiable-controllers/, bài báo liên quan dự kiến sẽ được trình bày tại OSDI 2024

    • Tò mò không biết nó làm được gì hơn so với unit test

  • Có thể dùng debug_assert của Rust như một bước đệm nhỏ trước khi sang Verus, bằng cách gắn nó vào tiền điều kiện và hậu điều kiện
    Trình biên dịch Rust mặc định sẽ loại bỏ chúng trong bản build production
    Ví dụ kiểm chứng trong tutorial của Verus viết phạm vi đầu vào và điều kiện kết quả bằng requires và ensures, còn bản kiểm tra lúc chạy thì xác nhận các điều kiện tương tự trong quá trình thực thi như debug_assert(-16 <= x1), debug_assert(x8 == 8 * x1)

    • Một vấn đề hiện tại của cú pháp Verus là phải bọc toàn bộ mã trong procedural macro
      Các công cụ Rust khác cho chứng minh/kiểm chứng/thiết kế theo hợp đồng như Creusot dùng cú pháp dựa trên attribute, nhìn chung nhẹ hơn và mang cảm giác đúng chất Rust hơn
      Sẽ rất tốt nếu các bản phát hành Verus sau này cũng hỗ trợ cách đó
    • Mong là sẽ có nhiều người dùng assert kiểu này hơn
      Nó là công cụ tài liệu hóa rất tốt, và bổ sung cực kỳ hiệu quả cho hệ thống kiểu cùng với test
    • Cũng có thể thử crate "contracts": https://docs.rs/contracts/latest/contracts/
    • Ví dụ của Verus khá giống cách tôi viết code Clojure
      Tôi gắn tiền điều kiện và hậu điều kiện cho hầu hết các hàm, và JVM có cờ cho phép dễ dàng loại bỏ chúng trong bản build production

  • Với người không có nhiều kinh nghiệm khoa học máy tính thực tế như tôi thì hơi thắc mắc: trong câu “kiểm chứng tính đúng đắn của mã” ở README, kiểm chứng khác gì với “chứng minh” ở chỗ khác?
    Tôi cũng muốn biết có tài liệu nào phù hợp cho lập trình viên đi làm, không có nền tảng khoa học máy tính/toán học quá mạnh, để học cách “chứng minh” về code không
    Ngoài ra tôi cũng chưa hiểu vì sao zero-knowledge proof lại quan trọng và có tính liên quan lớn đến vậy. Ví dụ tôi có nghe những câu chuyện như x.com/ZorpZK nhưng không hiểu vì sao nó lại hay

    • Có Software Foundations là tài liệu tốt để học song song kiểm chứng mã và lập trình hàm: https://softwarefoundations.cis.upenn.edu
      Tuy nhiên Coq dùng trong Verus và Software Foundations có cách tiếp cận khác nhau
      Verus cố tự động chứng minh các thuộc tính bằng SMT solver, tức hệ thống tự động giải ràng buộc, còn Coq đòi hỏi phải chứng minh thủ công nhiều hơn và mức độ tự động hóa hạn chế hơn nhiều
      Cả hai đều có ưu và nhược điểm; tự động hóa thì rất tuyệt khi nó hoạt động, nhưng lúc không hoạt động thì khá bực bội
      Zero-knowledge proof đúng hơn nên xem là lĩnh vực khác; nhiều người làm kiểm chứng/chứng minh hình thức cũng không đụng đến nó. Hãy xem nó như một primitive mật mã thì hợp lý hơn
    • Ở đây kiểm chứng và chứng minh đang được dùng như từ đồng nghĩa, và nửa sau của đoạn đầu cũng cho thấy khá rõ điều đó
      Zero-knowledge proof có overhead lớn và thiếu cái gọi là “killer app”, nên về ứng dụng thực tiễn, tầm quan trọng và mức độ liên quan thì hiện vẫn chưa lớn lắm, dù xét về mặt ý tưởng thì rất thú vị
    • Trong ngữ cảnh này, “kiểm chứng” và “chứng minh” là như nhau
      Tôi cũng ước có tài liệu học tốt hơn. Tài liệu của Dafny khá ổn, nhưng kiểm chứng phần mềm hình thức dường như vẫn chưa đến mức đủ dễ dùng cho lập trình viên bình thường không phải tiến sĩ khoa học máy tính/toán học
      Nhìn các ví dụ thì thấy tương đối dễ, nhưng rồi nhanh chóng đụng phải tình huống “không thể chứng minh”, và câu trả lời vì sao lại thường chui sâu vào các chi tiết cài đặt mà có lẽ chỉ tác giả mới hiểu
    • Theo tôi hiểu thì zero-knowledge proof cho phép chứng minh rằng bạn biết một thứ gì đó mà không cần tiết lộ nội dung của thứ đó
      Ví dụ, có thể xác minh rằng bạn biết mật khẩu mà không cần gửi mật khẩu cho máy chủ, nhờ vậy máy chủ độc hại hay kẻ tấn công trung gian sẽ khó đánh cắp mật khẩu hơn
      Nó cũng có thể đem lại lựa chọn tốt hơn cho xác minh danh tính. Bạn có thể chứng minh mình có giấy tờ do chính phủ cấp mà không cần gửi cả tài liệu cho máy chủ, từ đó giảm chuyện dữ liệu bị giữ “tối đa 2 năm/3 năm/6 tháng” rồi cuối cùng vẫn bị rò rỉ
    • Tôi cho rằng cụm “lập trình viên đi làm chứng minh về code” hiện vẫn gần như là một nghịch lý
      Chứng minh về code vẫn chưa phải việc mà lập trình viên đi làm thường làm
      Hoare logic là điểm khởi đầu tốt, và đôi khi còn được dạy trong các môn nhập môn khoa học máy tính
      Coq có đường cong học tập rất dốc, đặc biệt nếu bạn chưa quen OCaml hay ngôn ngữ tương tự. Why3 có thể thân thiện hơn với người mới: https://www.why3.org
      Chứng minh và kiểm chứng có thể mang cùng nghĩa, nhưng “chứng minh” gợi cảm giác tương tác hơn, còn “kiểm chứng” gợi cảm giác có thể được tự động hóa, như model checking hay giải SMT trên chương trình có chú thích

  • Nếu ai chưa biết các dự án tương tự, Dafny là một “ngôn ngữ lập trình có nhận thức về kiểm chứng” có thể biên dịch sang Rust: https://github.com/dafny-lang/dafny

  • Trông thực sự rất hay. Sẽ hữu ích cho mọi người nếu có hướng dẫn hoặc ví dụ về cách bổ sung chứng minh vào một codebase hiện có
    Ví dụ, giả sử một ứng dụng GUI tối thiểu chỉ có một hộp văn bản nhận một mảng không đáng tin cậy mà tại thời điểm biên dịch không thể biết trước qua một yêu cầu HTTP, rồi sắp xếp nổi bọt và hiển thị nó
    Trong bubble sort có một lỗi cố ý kiểu off-by-one khiến phần tử cuối cùng vẫn còn nguyên, còn unit test thì tình cờ không bắt được lỗi đó. Việc lo lắng rằng test không đầy đủ có thể là động lực chính để đi đến chứng minh
    Sau đó, sẽ hay nếu cho thấy quá trình thay thế unit test bằng chứng minh, phát hiện lỗi và sửa nó
    Không cần giải thích quá chi tiết về chính phần mã chứng minh; chỉ cần tập trung vào các chi tiết thực tế như ranh giới giữa mã toán học đã được chứng minh và mã vào/ra chưa được chứng minh, các dòng lệnh dùng cho chứng minh và build, hay một tệp zip để có thể tự tay thử nghiệm
    Thực ra chỉ cần đọc từ standard input và ghi ra standard output cũng có lẽ là đủ

  • Một trong những người đóng góp chính đã có một bài trình bày rất hay về Verus tại buổi meetup Rust ở Zürich: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
    Tôi thấy rất ấn tượng về mức độ gọn gàng mà mã “ghost” này hòa vào chương trình, và nó khiến tôi hơi liên tưởng đến Ada

  • Tôi tự hỏi liệu Rust cũng đã có một tiêu chuẩn như C/C++, Common Lisp, Ada/SPARK2014 hay chưa
    Nếu chưa có thì so với các công cụ kiểm chứng được phát triển cho Ada/SPARK2014, đây sẽ là một mục tiêu luôn thay đổi
    Cũng khó mà bỏ qua di sản của Ada/SPARK2014, trải từ bare metal cho đến các ứng dụng bắt buộc an toàn có tính toàn vẹn cao

  • Tôi thắc mắc mối quan hệ giữa cái này và Kani là gì. Chúng hoạt động khác nhau à?
    https://github.com/model-checking/kani

    • Model checker thường chỉ khám phá một số lượng trạng thái hữu hạn, nên hiệu quả trong việc tìm lỗi, và nhiều khi cũng không cần thêm chú thích vào chương trình
      Các trình kiểm chứng tự động dựa trên SMT như Verus, Dafny, F* và VCC của tôi thì cần chú thích gần như mọi hàm và vòng lặp, nhưng đổi lại cung cấp các bảo đảm rộng hơn về tính đúng đắn của chương trình
      Các công cụ dựa trên interactive prover như Coq hay Lean thường cần người dùng dẫn dắt nhiều hơn, nhưng có thể bảo đảm cả những thuộc tính phức tạp hơn

  • Tôi tò mò Verus so với SPARK thì thế nào
    Nó có thuộc cùng một nhóm trình kiểm chứng tổng quát không? Ngoài chuyện nó là trình kiểm chứng cho Rust thay vì cho Ada, Verus còn khác ở điểm nào?

  • Sẽ rất hay nếu ai đó hiểu rõ Verus có thể giải thích sự khác biệt về hiệu năng và khả năng biểu đạt giữa Verus và Lean4
    Tôi hiểu Verus là công cụ kiểm chứng dựa trên SMT, còn Lean là interactive prover đồng thời cũng là công cụ dựa trên SMT
    Tuy vậy, hiểu biết của tôi về lĩnh vực formal verification còn hạn chế, nên tôi muốn nghe góc nhìn từ người thực sự am hiểu các phương pháp hình thức trong phần mềm

    • Lean khá giống Coq
      Ví dụ, bạn có thể phát biểu và chứng minh các mệnh đề về mã C như trong sách “Software Foundations” của Coq, nhưng có vẻ gần như không ai làm điều đó với Lean và công cụ hỗ trợ cũng còn thiếu
      Bạn cũng có thể viết chương trình bằng Lean4 và chứng minh về chính chương trình đó, và đã có một số người làm theo hướng này ở mức độ nhỏ
      Việc hình thức hóa toán học thuần túy và công bố bài báo về nó hiện là cách Lean4 và Coq chủ yếu được sử dụng
      Những gì Lean/Coq thực sự có thể phát biểu và chứng minh thì tổng quát hơn, nhưng với các chương trình ngoài đời thực thì có thể không nhất thiết cần mức độ tổng quát đó