Dịch các crate `core` và `alloc` của Rust sang Coq để kiểm chứng hình thức

 (formal.land)
1 điểm bởi GN⁺ 2024-05-16 | 1 bình luận | Chia sẻ qua WhatsApp
  • coq-of-rust, công cụ chuyển chương trình Rust sang Coq, đã bắt đầu xử lý cả các crate core và alloc của thư viện chuẩn, giúp giảm gánh nặng phải tự viết tay định nghĩa Coq cho từng hàm primitive
  • Vì hai crate này là những codebase lớn với nhiều mã Rust nâng cao và unsafe, thách thức cốt lõi là xử lý kết quả dịch tự động thành các đơn vị có thể biên dịch và kiểm chứng được
  • Khi chia đầu ra theo từng tệp Rust đầu vào, alloc thành 54 tệp với 171.783 dòng, còn core thành 190 tệp với 592.065 dòng, giúp biên dịch song song và gỡ lỗi dễ hơn
  • Xung đột tên mô-đun trong các khối impl đã được giảm bớt bằng cách đưa cả thông tin mệnh đề where vào, nhưng hiện vẫn còn 4% số tệp chưa biên dịch được trong Coq
  • Ví dụ Option::unwrap_or_default được dùng bằng cách chứng minh định nghĩa dịch tự động tương đương với một định nghĩa hàm đơn giản hơn, nên cần cả độ tin cậy của tự động hóa lẫn việc kiểm tra tại thời điểm chứng minh

Xử lý primitive của thư viện chuẩn Rust

  • Formal Land đang phát triển coq-of-rust, công cụ dịch chương trình Rust sang hệ thống chứng minh hình thức Coq
  • Trước đây, để xử lý các thành phần primitive của thư viện chuẩn Rust, cần phải tạo riêng định nghĩa Coq mô tả hành vi cho từng hàm
  • Để giảm gánh nặng này, họ đã dịch các crate core và alloc của Rust bằng coq-of-rust
  • Có thể xem kết quả dịch tại các đường dẫn sau

Kết quả chạy dịch ban đầu

  • Khi chạy coq-of-rust lần đầu trên alloc và core, hệ thống tạo ra 2 tệp Coq quy mô hàng trăm nghìn dòng, tương ứng với toàn bộ từng crate
  • Điều này xác nhận công cụ có thể chạy trên các codebase lớn, nhưng mã Coq được tạo ra chưa thể biên dịch ngay
  • Lỗi xuất hiện không quá thường xuyên, ở mức khoảng một lỗi cho mỗi vài nghìn dòng
  • Theo cloc, quy mô mã Rust đầu vào như sau
    • alloc: 26.299 dòng mã Rust
    • core: 54.192 dòng mã Rust
  • Vì quá trình dịch có mở rộng macro, nên đối tượng thực tế được dịch còn lớn hơn số dòng gốc

Chia nhỏ mã Coq được tạo ra

  • Thay đổi lớn nhất là chia đầu ra của coq-of-rust thành một tệp Coq cho mỗi tệp Rust đầu vào
  • Việc chia này khả thi vì quá trình dịch không nhạy với thứ tự định nghĩa và mang tính context-free
  • Giữa các tệp Rust thường có phụ thuộc vòng, trong khi Coq không cho phép điều đó, nhưng với cách dịch này vẫn có thể tách theo từng tệp
  • Sau khi chia, quy mô đầu ra như sau
    • alloc: 54 tệp Coq, 171.783 dòng mã Coq
    • core: 190 tệp Coq, 592.065 dòng mã Coq
  • Việc tách tệp giúp việc khám phá và bảo trì mã sinh ra dễ hơn
    • Dễ song song hóa quá trình biên dịch
    • Có thể tập trung gỡ lỗi từng tệp một
    • Dễ loại trừ các tệp chưa biên dịch được
    • Dễ theo dõi diff của từng tệp riêng lẻ

Sửa xung đột tên mô-đun và các tệp còn lại

  • Một số lỗi bắt nguồn từ xung đột tên mô-đun trong các khối impl
  • Cách xử lý là đưa thêm thông tin vào tên mô-đun để tăng tính duy nhất
    • Bao gồm cả thông tin mệnh đề where, vốn trước đây bị bỏ qua
    • Ví dụ, trong phần cài đặt trait Default cho Mapping<K, V>, điều kiện cả K và V đều phải triển khai Default sẽ được phản ánh trong tên mô-đun
  • Các tệp hiện chưa biên dịch được trong Coq gồm
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • Số này chiếm 4% tổng số tệp
  • Tuy vậy, ngay cả trong các tệp biên dịch được vẫn còn những thành phần Rust chưa xử lý xong đang bị tiên đề hóa, nên chỉ riêng tỷ lệ này chưa đủ để đánh giá toàn bộ phạm vi chưa được hỗ trợ

Ví dụ dịch Option::unwrap_or_default

  • Option::unwrap_or_default của Rust sẽ trả về x nếu là Some(x), và gọi T::default() nếu là None
  • coq-of-rust dịch nó thành một định nghĩa Coq dạng monadic
    • Khớp đối số đầu vào và kiểu dữ liệu
    • Ở nhánh Some, lấy trường của tuple rồi sao chép
    • Ở nhánh None, gọi phương thức default của trait core::default::Default
  • Trong kiểm chứng thực tế, họ dùng một định nghĩa hàm đơn giản hơn thay vì định nghĩa sinh tự động
    • Nếu là None thì trả về core.simulations.default.Default.default
    • Nếu là Some x thì trả về x
  • Chứng minh rằng định nghĩa sinh tự động và định nghĩa đơn giản là tương đương nằm tại CoqOfRust/core/proofs/option.v
  • Khi mã Rust gốc thay đổi, chứng minh này sẽ giúp phát hiện thay đổi
  • Vì bản dịch thư viện core được tạo hoàn toàn tự động, nên có thể tin cậy định nghĩa sinh ra hơn các định nghĩa viết tay
  • Tuy nhiên, coq-of-rust vẫn có thể có sai sót hoặc chưa hoàn thiện, nên cần kiểm tra tính đúng đắn của mã tại thời điểm chứng minh

Các bài toán còn lại

  • Mức độ tin cậy vào việc hình thức hóa thư viện chuẩn trong kiểm chứng chương trình Rust đã tăng lên
  • Mục tiêu tiếp theo vẫn là đơn giản hóa quy trình chứng minh vốn còn tẻ nhạt
  • Đặc biệt, để cho thấy mô phỏng là tương đương với mã Rust gốc, vẫn cần các bước sau
    • Phân giải tên
    • Đưa vào các kiểu cấp cao
    • Loại bỏ tác dụng phụ
  • Hướng cải tiến tiếp theo là tách riêng và xử lý từng bước này

Bài viết liên quan

1 bình luận

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

  • Thật sự ấn tượng
    Kiểu dịch tự động này chuyển đối tượng cần tin cậy sang công cụ. Bản thân coq-of-rust được viết bằng Rust chứ không phải Coq, nên cấu trúc đệ quy của nó khá đáng ngạc nhiên; nhưng nếu kết hợp cách tiếp cận kiểu CompCert với phương pháp dùng trình biên dịch thứ hai để né đòn tấn công Trusting Trust của Ken Thompson, như trong “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0] của David A. Wheeler, thì có vẻ có thể chứng minh được tính đúng đắn
    Để kiểm chứng, có thể dùng coq-of-rust để chuyển trình dịch coq-of-rust từ Rust sang Coq; vì bản dịch đó được thực hiện bằng Rust nên dù không tin nó, chỉ cần chứng minh trong Coq các tính chất đúng đắn mong muốn, đặc biệt là việc bảo toàn ngữ nghĩa khi dịch chương trình Rust sang Coq
    Như trong bài báo, rất có thể việc chứng minh trên các định nghĩa mang tính hàm hơn so với các định nghĩa được sinh ra sẽ dễ hơn, nên chỉ cần trải qua bước chứng minh tính tương đương giữa các định nghĩa như cách làm trong thư viện chuẩn. Nếu trình dịch coq-of-rust hiện tại, đặc biệt là lib/ [1], có 6.350 dòng Rust, thì việc viết toàn bộ trình dịch bằng Coq và chứng minh nó tương đương với bản được sinh ra cũng có vẻ thực tế
    Sau đó, nếu chạy trình dịch coq-of-rust bản Coq đã được chứng minh trên mã nguồn coq-of-rust viết bằng Rust, các định nghĩa Coq đầu ra phải khớp với đầu ra của trình dịch coq-of-rust bản Rust đã dùng ban đầu
    Ngoài lề, thật tốt khi thấy những công việc như thế này nhận được tài trợ từ công nghiệp. Tôi khá hoài nghi về tiền mã hóa, nhưng đúng là yêu cầu về tính đúng đắn trong lĩnh vực đó đang thúc đẩy cải thiện ở những mảng tôi quan tâm như Rust, Coq, và hỗ trợ các học viên cao học mà tôi quen
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • Tôi là một trong các tác giả; thực tế quy trình như vậy có thể là một cách tốt để kiểm chứng coq-of-rust
      Tuy nhiên, dù bản thân mã khá ngắn, nó vẫn dựa vào trình biên dịch Rust để phân tích cú pháp và kiểm tra kiểu mã Rust đầu vào. Vì vậy phần đó cũng phải được kiểm chứng, hoặc ít nhất phải có đặc tả hình thức dù không chứng minh. Việc API của rustc khá lớn và không ổn định là một trở ngại, nhưng dù sao đây vẫn có thể là một cách để tăng mức độ tin cậy
    • Điều này làm tôi nhớ lại thời còn làm với SPARK Ada. Với những dự án không có target Ada được hỗ trợ, đặc biệt là trên các thiết bị rất nhỏ, chúng tôi thường chuyển Ada sang C rồi biên dịch cho target đó; nhờ vậy phía SPARK vẫn có thể thực hiện nhiều dạng phân tích tĩnh
      Dĩ nhiên lại phát sinh vấn đề phải kiểm chứng đầu ra hoặc bộ chuyển đổi, nhưng mã C kết quả khá dễ đọc cho mục đích kiểm chứng, phong cách cũng bị giới hạn, và mức độ tin cậy vào công cụ cũng cao. Phân tích tĩnh của SPARK là một phần trong toàn bộ quy trình verification/validation, còn kiểm thử và các hoạt động khác cung cấp thêm các lớp tin cậy. Nhìn chung đó là một cách tiếp cận hoạt động khá tốt
    • Lý do tiền mã hóa giúp cho những việc này không chỉ là các ràng buộc về tính đúng đắn, mà còn vì nhiều của cải đã được chuyển sang tay những người quan tâm đến khoa học máy tính
      Việc họ dùng số tiền đó cho nghiên cứu khoa học máy tính không chỉ vì có lợi cho họ, mà còn là một dạng hoạt động thiện nguyện gắn với sở thích của họ
    • Tôi không rõ cách tiếp cận đó ngăn trình biên dịch Rust được dùng để tạo binary khỏi chèn payload độc hại như thế nào. Có thể build A thành B rồi build B thành A và so sánh binary, nhưng
      Một cách khác là proof-carrying code. Tức là trình biên dịch Rust xuất kèm một chứng minh Coq rằng file thực thi đầu ra khớp với ngữ nghĩa của mã nguồn đầu vào
      Dĩ nhiên cũng có thể viết một trình biên dịch cho một tập con của Rust, chẳng hạn không có borrow checker hay tối ưu hóa, sang mã máy của một kiến trúc cụ thể rồi bootstrap mọi thứ từ đó

  • Kích thước của các chương trình được kiểm chứng từ đầu đến cuối bằng hệ thống chứng minh suy diễn bán tự động như Coq là nhỏ. Thư viện có thể dễ hơn vì mức độ tương tác giữa các phần mã thấp hơn, nhưng chương trình thông thường thì không như vậy
    Trên thực tế, tốc độ tăng kích thước của các chương trình có thể kiểm chứng theo cách này chậm hơn tốc độ tăng kích thước trung bình của toàn bộ chương trình. Kiểm chứng phần mềm sound, tức chứng minh khớp 100% với đặc tả, rõ ràng hữu ích ở những chỗ như chứng minh tính đúng đắn của thuật toán lõi, nhưng không mở rộng tốt
    Vì vậy nghiên cứu phần nào đã chuyển sang các phương pháp unsound. Chi phí cho bảo đảm 100% có thể gấp 10 lần bảo đảm 99,9999%, và chênh lệch xác suất đó có thể nhỏ hơn xác suất hỏng hóc ngoài phần mềm. Hệ thống vật lý ngay từ đầu đã không thể được chứng minh là khớp với đặc tả, và bản thân đặc tả cũng có xác suất không đủ khớp với thực tế

    • Điểm cốt lõi là nếu chứng minh được các phần unsafe của thư viện chuẩn và các bảo đảm an toàn của Rust, thì có thể chứng minh bắc cầu cho mọi mã Rust an toàn chỉ dùng thư viện chuẩn về an toàn bộ nhớ, không có data race, v.v.
      Việc chứng minh chỉ phần mã unsafe là đúng có thể thực hiện với ít công sức hơn rất nhiều so với chứng minh toàn bộ mã Rust. Đây là câu trả lời cho phê phán thường gặp khi nói về các bảo đảm an toàn của Rust: “thế còn mã unsafe thì sao?”. Những khoảng trống chưa đủ mạnh để hệ thống kiểu của Rust xử lý có thể được lấp bằng một hệ thống mạnh hơn như Coq

  • Có một điểm trong những nỗ lực kiểu này mà tôi chưa hiểu rõ. Nếu phải chuyển đổi mã sang Coq thủ công hoặc bán thủ công, chẳng phải khả năng mắc lỗi trong quá trình đó còn lớn hơn rất nhiều so với lợi ích thu được từ xác minh hình thức sao?
    Nói cách khác, làm sao ta biết điều mình đã chứng minh vẫn có hiệu lực với mã gốc?

    • Không thể biết chắc. Rốt cuộc vẫn phải tin tưởng vào một thứ gì đó, như phần cứng, trình biên dịch, đặc tả, kernel tin cậy của Coq, v.v.
      Xác minh hình thức thường được bàn như thể nó loại bỏ hoàn toàn khả năng có lỗi, nhưng thực tế gần với việc giảm xác suất lỗi xuống rất nhiều hơn. Dù vậy, dịch tự động giữa Rust và Coq làm giảm đáng kể độ phức tạp của những thứ phải tin tưởng, nên nên được ưu tiên hơn dịch thủ công
    • Đó là một giới hạn đúng, nhưng không phải giới hạn tệ đến vậy
      Trong nhiều trường hợp, lỗi dịch đơn giản sẽ khiến việc chứng minh trở nên bất khả thi. Khi đó ai đó sẽ điều tra vì sao chứng minh không qua và tìm ra lỗi dịch
      Vấn đề thật sự là khi lỗi dịch triệt tiêu chính xác lỗi trong mã gốc. Nếu không có rủi ro mang tính hệ thống, khả năng hai lỗi xóa nhau theo cách này là khá thấp
    • Mã được dịch tự động bằng coq-of-rust. Nếu phát hiện vấn đề trong bản dịch, chỉ cần sửa một lần trong công cụ coq-of-rust, và mọi kết quả dịch sẽ được cập nhật

  • Với độc giả quan tâm: Tôi gửi bài blog này vì nội dung liên quan đến tiền mã hóa trong đó ít trực tiếp hơn so với các bài khác trên cùng blog, nhưng ở đó có nhiều bài viết thú vị hơn về mặt kỹ thuật
    Đặc biệt hai bài gần đây nói về việc áp dụng cùng cách tiếp cận này cho Python chứ không phải Rust

  • Tôi nhớ một bài giảng [1] trước đây nói rằng fuzzer đã tìm thấy lỗi trong một trình biên dịch C đã được xác minh hình thức. Lý do là xác minh hình thức không bao gồm frontend và backend
    Tôi cũng biết có câu hỏi về việc có thể tin cậy Coq hoặc bản dịch đến mức nào, và cũng thắc mắc nó sẽ được đồng bộ với các bản cập nhật Rust ra sao, nhưng ngay cả xác minh hình thức hoàn hảo cũng không có nghĩa là độ chính xác 100% từ đầu đến cuối
    [1] https://youtu.be/Ux0YnVEaI6A

  • Tôi hoàn toàn không phải chuyên gia về xác minh hình thức, nhưng nếu thư viện cơ bản của Rust được xác minh hình thức và không dùng mã unsafe, thì mọi chương trình Rust dùng thư viện đã được xác minh hình thức có thực tế đạt chất lượng ở mức xác minh hình thức về mặt xử lý bộ nhớ không?

    • Tính an toàn của Rust gần như không liên quan đến bug
      Rust có định nghĩa “safe” riêng, có thể xem là một tập con của an toàn bộ nhớ. Ngay cả trong mã Rust hoàn toàn safe vẫn có thể xảy ra data race, deadlock, cạn bộ nhớ, chưa nói đến lỗi logic
    • Tôi nghĩ ở mức nào đó đó là giấc mơ, nhưng có rất nhiều điều kiện kèm theo và vài mảnh phải khớp với nhau
      Thứ nhất, cần hình thức hóa ngữ nghĩa của unsafe Rust. Công trình RustBelt[1] tiên phong của Ralf Jung là một bước tiến lớn nhưng vẫn chưa hoàn chỉnh. Đặc biệt nguồn gốc con trỏ đang lộ ra là một yếu tố khó
      Thứ hai, như một phần của việc đó, cần có mô hình hình thức của borrow checker. Stacked borrows[2] là một nỗ lực tốt nhưng có khiếm khuyết, và Tree borrows[3] có thể sửa được điều đó, nhưng cũng có khả năng sẽ xuất hiện thứ gì đó tinh vi hơn
      Thứ ba, cần một mô hình bộ nhớ hình thức. Điều này chủ yếu liên quan đến hành vi của các phép toán nguyên tử và đồng bộ hóa, nên rất quan trọng đối với các thành phần thư viện chuẩn như Arc. Việc mô hình bộ nhớ của Rust nên giống và tương tác được với C++ được chấp nhận rộng rãi, nhưng vẫn còn vấn đề “out of thin air” và các tính năng còn thiếu như seqlock. Đó là một trong những lý do kernel Linux vẫn dùng mô hình riêng
      Thứ tư, cần chứng minh rằng các bảo đảm an toàn kết hợp tốt với nhau. Đặc biệt, khi mã đúng đắn viết bằng unsafe Rust được kết hợp với mã safe Rust, các bảo đảm an toàn vẫn phải được duy trì. Đến nay đã có các kết quả tốt, nhưng cần được chứng minh cho toàn bộ hệ thống
      Thứ năm, để những chứng minh như vậy đúng với mọi mã, Rust phải đóng tất cả các lỗi soundness[1] còn lại. Khá nhiều vấn đề trong số này chỉ thực sự quan trọng trong lý thuyết hoặc trong mã đối nghịch[5], nên tiến độ chậm
      Ngay cả khi tất cả những điều này hoàn tất, đó vẫn chỉ là bảo đảm một phần. Một phần cực lớn của bề mặt tiếp xúc với hệ thống dựa trên mã unsafe. Nếu chỉ làm tính toán thuần túy thì có thể khác, nhưng ví dụ nếu bạn làm giao diện đồ họa thì vẫn còn rất nhiều thứ có thể sai
      Dù vậy vẫn có một con đường tiến thực dụng, và nó dẫn đến tình trạng tốt hơn rất nhiều so với trạng thái phổ biến hiện nay là các hệ thống đầy lỗ hổng
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • Tôi không phải chuyên gia Rust, nhưng có vẻ trong mã core có khá nhiều unsafe. Điều đó cũng hợp lý
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      Tôi không nghĩ Coq theo cách được trình bày ở đây có thể xác minh mọi lời gọi unsafe

  • Có thể so sánh cách tiếp cận này khác với Aeneas hay RustHornBelt như thế nào không? Con trỏ và borrow khả biến được xử lý ra sao?

    • Tôi không biết RustHornBelt hoạt động như thế nào. Chúng tôi tập trung vào mã an toàn, nhưng cũng tạo bản dịch cho các khối unsafe theo kiểu “nỗ lực tốt nhất”
      So với Aeneas, mục tiêu rất giống nhau, vì cả hai đều nhằm kiểm chứng chương trình Rust bằng trình chứng minh định lý tương tác. Tuy nhiên, trong coq-of-rust, chúng tôi viết thủ công phiên bản mã thuần hàm để làm đối tượng chứng minh, hoặc vì đây là công việc lặp lại nên viết với sự trợ giúp của GitHub Copilot, rồi chứng minh nó tương đương với kết quả dịch tự động. Aeneas hướng tới việc trực tiếp tạo ra phiên bản hàm
      Mọi con trỏ đều được xử lý như con trỏ khả biến, tức kiểu *. Chúng tôi không dùng thông tin của borrow checker trong Rust; nhờ vậy bản dịch đơn giản hơn, nhưng cái giá phải trả nằm ở thời điểm chứng minh
      Để suy luận về con trỏ trong chứng minh, chúng tôi cho phép người dùng cung cấp một bộ cấp phát tùy chỉnh, được thiết kế theo cách bộ nhớ sẽ được sử dụng. Ví dụ, nếu chương trình dùng ba biến khả biến toàn cục, có thể biểu diễn bộ nhớ dưới dạng một record có ba mục. Ban đầu các mục này là None để biểu thị trạng thái chưa được cấp phát
      Chúng tôi chưa biết kỹ thuật này sẽ mở rộng được đến đâu, nhưng ít nhất hiện tại có thể tránh suy luận bằng separation logic. Chúng tôi kỳ vọng phần lớn chương trình cần kiểm chứng, đặc biệt ở phía ứng dụng, sẽ có kỷ luật bộ nhớ tương đối “đơn giản”

  • Việc viết đặc tả kiểm chứng hình thức có giống như dùng kiểm thử dựa trên thuộc tính phức tạp hơn không? Khi vượt ra ngoài các chương trình không phức tạp, việc viết kiểm thử dựa trên thuộc tính cũng khá khó và tốn thời gian

    • Giống, nhưng không phải lúc nào cũng như nhau. Kiểm thử dựa trên thuộc tính thường chỉ định mô tả đầu vào ở cấp giao diện hệ thống, cấp hàm hoặc thủ tục, hay cấp cao hơn, rồi kiểm tra xem đầu ra có thỏa một thuộc tính hoặc một tập thuộc tính nào đó không
      Khi làm kiểm chứng hình thức ở cùng cấp độ, trông nó cũng có thể khá giống. Nhưng các công cụ kiểm chứng hình thức có thể đi sâu hơn. Ví dụ, chúng có thể trả lời các câu hỏi như “có bất biến vòng lặp này đối với trạng thái hệ thống bên trong phép tính, liệu có chứng minh được rằng nó thật sự được duy trì ở mọi vòng lặp không?” hoặc “có thể chứng minh rằng không bao giờ xảy ra underflow/overflow ở bất kỳ phép tính trung gian nào trong quá trình tính toán này không?”
      Trường hợp đầu cũng có thể làm bằng kiểm thử dựa trên thuộc tính nếu tách phần lõi của vòng lặp thành một thủ tục riêng và chạy với nhiều trạng thái trung gian để kiểm tra thuộc tính bất biến. Trường hợp sau khó hơn nhiều, trừ khi chia nhỏ chương trình đến mức từng dòng có thể chạy riêng

  • Tôi thậm chí không biết là có thể làm được những thứ như vậy
    Tôi tò mò liệu những nỗ lực như thế này có thể đẩy nhanh việc chấp nhận Rust trong các phần cốt lõi của việc đưa Rust vào kernel hay không

  • Ai đó có thể giải thích khái niệm “kiểm chứng” thật dễ hiểu được không? Tôi tò mò vì sao cả một ngôn ngữ như Coq lại tồn tại chỉ cho mục đích này, và nó có ý nghĩa thực tiễn gì đối với xã hội rộng hơn