Xác thực mã hóa Rust trong SymCrypt: Từ tiêu chuẩn đến thực thi

Cách Rust, Lean, Aeneas và các tác nhân AI giúp mở rộng quy mô kiểm chứng hình thức (formal verification) cho các thuật toán mật mã trong môi trường thực tế.

Tóm tắt

Giới thiệu và động lực cho việc kiểm chứng hình thức

Mã mật mã là nền tảng của điện toán hiện đại. Nó bảo vệ các hệ điều hành, dịch vụ đám mây, firmware, hệ thống nhắn tin và các giao thức kết nối chúng. Những sai sót nhỏ có thể dẫn đến hậu quả khôn lường: một lỗi tính toán đơn lẻ, thiếu kiểm tra giới hạn (bounds check) hoặc chuyển đổi trạng thái không chính xác đều có thể làm suy yếu tính bảo mật của một thiết kế vốn dĩ an toàn.

Kiểm thử (testing) và kiểm toán (auditing) vẫn rất cần thiết, nhưng tự chúng là chưa đủ. Các triển khai mật mã thường được tối ưu hóa, chạy trong thời gian hằng định (constant-time), đặc thù theo kiến trúc và cố ý viết ở cấp độ thấp. Mã nguồn được phát hành hiếm khi giống với thuật toán sạch sẽ trong tiêu chuẩn: nó chứa các phép rút gọn, thao tác bit, các hàm nội tại SIMD (SIMD intrinsics), các vòng lặp được định hình cẩn thận và các lớp tương thích cho nhiều môi trường.

Kiểm chứng hình thức giải quyết khoảng trống này bằng cách triển khai các chứng minh được máy tính kiểm tra thay vì chỉ dựa vào kiểm thử. Thay vì chỉ kiểm tra xem mã nguồn thường hoạt động đúng, kiểm chứng thực hiện một đặc tả toán học chính xác cho tất cả các đầu vào thỏa mãn các điều kiện tiên quyết đã nêu.

Tháng 6 năm ngoái, Microsoft thông báo chúng tôi sẽ kiểm chứng hình thức các thuật toán mới được viết bằng Rust trong SymCrypt, nhà cung cấp mật mã được sử dụng trên các sản phẩm và dịch vụ bao gồm Windows và Azure. Các triển khai mật mã mới đang được viết bằng Rust an toàn, sau đó được kiểm chứng trong khung chứng minh hình thức Lean (mở trong tab mới) sử dụng chuỗi công cụ Aeneas (mở trong tab mới). Điều này đặc biệt áp dụng cho mật mã hậu lượng tử, vốn đòi hỏi các triển khai nhanh và an toàn của các thuật toán phức tạp. Sự kết hợp này mang lại cho chúng tôi hai lớp đảm bảo: Rust loại bỏ các nhóm lỗi an toàn bộ nhớ phổ biến, trong khi các chứng minh Lean thiết lập tính đúng đắn về chức năng dựa trên các đặc tả hình thức được rút ra từ các tiêu chuẩn.

Kết quả là một phương pháp kiểm chứng mới cho mật mã thực tế: kiểm chứng mã nguồn ngay khi lập trình viên viết, bảo toàn các lựa chọn triển khai hướng hiệu năng và làm cho quy trình chứng minh đủ khả năng mở rộng để theo kịp một cơ sở mã đang phát triển.

Trạng thái kiểm chứng trong SymCrypt

Chúng tôi đã mở mã nguồn một nhánh SymCrypt (mở trong tab mới) bao gồm các đặc tả và chứng minh hình thức. Nhánh công khai này cung cấp các kết quả chứng minh cùng với các triển khai thuật toán Rust mà chúng xác thực, cho thấy cách phương pháp này áp dụng cho mã mật mã thực tế. SymCrypt không phải là một nguyên mẫu nghiên cứu độc lập; đó là thư viện mật mã mã nguồn mở của Microsoft được sử dụng trên các sản phẩm và dịch vụ bao gồm Windows và Azure Linux.

Bản phát hành đầu tiên này bao gồm các chứng minh hoàn chỉnh cho mã Rust ML-KEM và SHA3 đang được sử dụng trong các bản dựng nội bộ (insiders builds) của Windows hiện nay. SymCrypt đang mở rộng quy trình làm việc dựa trên Rust, Lean và Aeneas tương tự cho nhiều thuật toán thuần Rust hơn và tích hợp chúng vào các phiên bản thực tế cho Windows và Linux, ví dụ như mã Rust đã được kiểm chứng cho AES-GCM, FrodoKEM và ML-DSA. Phần còn lại của bài viết này sử dụng công việc tại SymCrypt này làm ví dụ cụ thể, bắt đầu với cách các tiêu chuẩn công khai trở thành các đặc tả Lean có thể thực thi.

Chuyển đổi các tiêu chuẩn thành đặc tả Lean hình thức

Bước đầu tiên là hình thức hóa những gì thuật toán cần thực hiện. Đối với các nguyên hàm mật mã, nguồn tin cậy thường là một tiêu chuẩn công khai: đặc tả NIST, IETF RFC hoặc một mô tả thuật toán đã được xem xét kỹ lưỡng khác.

Trong phương pháp của chúng tôi, đặc tả Lean được thiết kế để bám sát tiêu chuẩn. Khi tiêu chuẩn mô tả một vòng lặp, cập nhật mảng hoặc phép toán, mô hình Lean tuân theo cùng cấu trúc đó bất cứ khi nào có thể. Sự gần gũi về cú pháp này rất quan trọng: nó giúp đặc tả hình thức dễ kiểm toán hơn vì người đánh giá có thể so sánh tiêu chuẩn và Lean song song với nhau.

Lean cũng cho phép chúng tôi viết các đặc tả có thể thực thi. Điều đó có nghĩa là chúng tôi có thể chạy mô hình hình thức dựa trên các vector kiểm thử chính thức để phát hiện lỗi sao chép, lỗi lệch một đơn vị (off-by-one) hoặc hiểu sai về tiêu chuẩn. Đối với các thuật toán như ML-KEM, chúng tôi có thể tiến xa hơn và chứng minh các thuộc tính toán học cấp cao, chẳng hạn như chỉ ra rằng mô hình hình thức của phép biến đổi số học (number-theoretic transform) tương ứng với phép toán dự định trên vành đa thức liên quan.

Một ví dụ điển hình là phép biến đổi số học (NTT) từ ML-KEM. Tiêu chuẩn mô tả thuật toán này như một phép biến đổi tại chỗ (in-place) trên 256 hệ số modulo q, với ba vòng lặp lồng nhau cập nhật các cặp hệ số sử dụng lũy thừa kế tiếp của hằng số ζ (= 17).

Dưới đây là bản dịch trực tiếp tiêu chuẩn NIST sang Lean, cố gắng bám sát cú pháp gốc nhất có thể:

Phiên bản Lean cố tình phản chiếu cấu trúc của tiêu chuẩn: cùng một cấu trúc vòng lặp lồng nhau, cùng cách chọn zeta và cùng cách cập nhật hệ số, cho phép con người dễ dàng đánh giá từng dòng. Đồng thời, nó có thể thực thi và sử dụng các kiểu dữ liệu toán học, vì vậy nó có thể được kiểm thử dựa trên các vector đã biết và kết nối với các định lý cấp cao hơn về ý nghĩa đại số của NTT. Tóm lại, đặc tả Lean là một mô hình súc tích, có thể thực thi, có ý nghĩa toán học và bám sát tiêu chuẩn đủ để các nhà mật mã học và kỹ sư chứng minh có thể đánh giá.

Kết nối đặc tả hình thức với mã nguồn

Sau khi đặc tả được hình thức hóa, thách thức tiếp theo là kết nối nó với triển khai. Chúng tôi không yêu cầu các nhà phát triển viết lại mã mật mã thực tế bằng một ngôn ngữ hướng kiểm chứng, cũng như không tạo ra mã mà các nhóm sản phẩm phải tự quản lý. Thay vào đó, chúng tôi kiểm chứng mã Rust mà các kỹ sư viết, chính xác như cách họ viết.

Aeneas làm cho điều này trở nên khả thi bằng cách dịch biểu diễn cấp trung của Rust thành một mô hình Lean thuần túy. Kỷ luật về quyền sở hữu (ownership) và mượn (borrowing) của Rust rất quan trọng ở đây. Chúng cho phép Aeneas loại bỏ một cách an toàn phần lớn các suy luận về con trỏ aliasing, tính sống (liveness) và đột biến (mutation) vốn khiến việc kiểm chứng mã kiểu C trở nên rất tốn kém.

Ví dụ, một hàm Rust cập nhật một mảng tại chỗ sẽ trở thành một hàm trong Lean nhận vào và trả về một mảng hàm một cách rõ ràng. Các quyền mượn có thể thay đổi (mutable borrows) được dịch thành các phép biến đổi giá trị. Điều này bảo toàn hành vi quan trọng trong khi cung cấp cho các kỹ sư chứng minh một mô hình hàm dễ suy luận hơn nhiều.

Khi đã ở trong Lean, hàm có thể được trang bị một định lý khẳng định rằng nó tinh chỉnh (refine) một đặc tả hình thức. Nói cách khác, với mọi đầu vào thỏa mãn các giới hạn và điều kiện đúng đắn cần thiết, hàm triển khai trả về cùng một kết quả toán học như đặc tả Lean được rút ra từ tiêu chuẩn.

Phong cách này giữ cho các trách nhiệm được phân tách rõ ràng. Các kỹ sư phần mềm tiếp tục viết mã Rust hiệu năng và đúng phong cách. Các kỹ sư kiểm chứng làm việc với các mô hình Lean đã tạo và chứng minh các định lý về chúng. Mã Rust và các chứng minh tồn tại song song, nhưng gánh nặng chứng minh không làm biến đổi mã nguồn thành thứ gì đó thiếu tự nhiên.

Quay lại ví dụ NTT, triển khai Rust của nó là một hàm fn ntt(&mut [u16; 256]) sử dụng quyền mượn có thể thay đổi để cập nhật mảng tại chỗ. Bản dịch Lean làm tinh khiết nó thành một hàm ntt: Array U16 256#usize → Result (Array U16 256#usize) xuất trực tiếp mảng đã cập nhật, đồng thời bao bọc nó trong một kiểu Result để nắm bắt rõ ràng thực tế rằng các hàm Rust có thể gây ra lỗi panic.

Trong trường hợp này, định lý khẳng định rằng, nếu mảng thỏa mãn một bất biến về tính đúng đắn (đảm bảo nó đại diện cho một đa thức hợp lệ), thì việc chạy mô hình Rust ntt sẽ trả về biểu diễn đúng đắn của kết quả từ đặc tả toán học Spec.ntt, sau khi đã chuyển đổi từ các mảng cấp thấp sang các đa thức cấp cao.

Việc mở rộng quy mô này cho mọi hàm trong mã mật mã thực tế đòi hỏi sự tự động hóa đáng kể. Khả năng mở rộng của Lean cho phép chúng tôi xây dựng một lộ trình tự động hóa với các chiến thuật cho thực thi biểu tượng (symbolic execution), số học, mảng và suy luận bit-vector. Trải nghiệm trở nên gần giống với việc gỡ lỗi: tự động hóa xử lý các nghĩa vụ chứng minh thông thường, trong khi các kỹ sư có thể kiểm tra và tinh chỉnh chứng minh khi một mục tiêu không tự động đóng lại.

Hỗ trợ các hàm nội tại và nhiều kiến trúc

Mật mã thực tế không thể bỏ qua phần cứng. SymCrypt phải chạy trên các môi trường từ ngữ cảnh nhúng và kernel đến các dịch vụ đám mây. Nó cũng cần tận dụng các chỉ dẫn đặc thù của nền tảng khi có sẵn, bao gồm các hàm nội tại SIMD và các đường dẫn tối ưu hóa đặc thù theo kiến trúc.

Một câu chuyện kiểm chứng chỉ hoạt động với một triển khai tham chiếu di động (portable) là chưa đầy đủ. Chúng tôi cần kiểm chứng mã nguồn thực sự được phát hành: bao gồm logic điều phối, các quy trình tối ưu hóa và các biến thể đặc thù cho mục tiêu.

Mã dưới đây được điều chỉnh từ hàm ntt_layer được sử dụng nội bộ bởi NTT. Hàm này được biên dịch khác nhau cho x86-64 và aarch64, cho phép điều phối động (dynamic dispatch) đến các triển khai đặc thù mục tiêu hoặc di động. Trên x86-64, nó kiểm tra sự sẵn có của các chỉ dẫn SSE2, trong khi trên aarch64, nó kiểm tra Neon.

Vì đầu ra của rustc vốn dĩ đặc thù theo mục tiêu, chuỗi công cụ của chúng tôi biên dịch mã nhiều lần, mỗi lần cho một mục tiêu biên dịch cần kiểm chứng, trước khi hợp nhất các mô hình tương ứng. Trên thực tế, thao tác hợp nhất này biến việc điều phối tĩnh được cho phép bởi các thuộc tính cfg trong mã Rust thành một lớp điều phối động đầu tiên giữa x86-64 và aarch64 trong mô hình Lean. Theo những gì mã Rust thực hiện, các mô hình đặc thù mục tiêu này sau đó tự điều phối động đến các mô hình của XMM, Neon và các triển khai chung.

Các hàm nội tại đòi hỏi cách xử lý hơi khác. Một số trình bao bọc cấp thấp, đặc biệt là những trình thao tác con trỏ thô hoặc hiển thị các chỉ dẫn nền tảng, được mô hình hóa bằng các đặc tả Lean nhỏ, được xem xét kỹ lưỡng. Những phần khác có thể được mô hình hóa bằng mã Rust, có thể được kiểm thử dựa trên tài liệu tham chiếu phần cứng, sau đó được dịch và kiểm chứng. Mã Rust an toàn xung quanh sau đó được kiểm chứng dựa trên các mô hình đó. Điều này giữ cho bề mặt tin cậy hẹp trong khi vẫn bảo toàn được lợi ích hiệu năng của tăng tốc phần cứng.

Điểm quan trọng là kiểm chứng không đòi hỏi phải từ bỏ tối ưu hóa. Phương pháp này được thiết kế để bảo toàn sự phức tạp của mã thực tế – bao gồm các hàm nội tại, điều phối và các triển khai đặc thù nền tảng – trong khi vẫn chứng minh được một tuyên bố đúng đắn duy nhất, có thể kiểm toán.

Phản ánh các đảm bảo hình thức đến nhà phát triển mã

Kiểm chứng hình thức chỉ có thể mở rộng quy mô trong một tổ chức kỹ thuật nếu các nhà phát triển có thể hiểu những gì đã được chứng minh. Không đủ nếu một chứng minh chỉ tồn tại trong kho lưu trữ; sự đảm bảo phải hiển thị, có thể xem xét và đồng bộ hóa với mã nguồn mà các kỹ sư duy trì.

Để hỗ trợ điều này, chúng tôi hiển thị kết quả kiểm chứng thông qua các bảng điều khiển được tạo tự động. Các bảng điều khiển này tóm tắt các định lý theo thuật ngữ mà nhà phát triển có thể hiểu: các điều kiện tiên quyết, điều kiện hậu quyết, các hàm được bao phủ, các mô hình tin cậy và các giả định còn lại. Các kỹ sư không cần mở Lean để xem những gì đã được kiểm chứng. Ví dụ, dưới đây là trang được hiển thị bởi bảng điều khiển cho hàm ntt của chúng tôi.