Apple công bố quy trình xác minh hình thức cho corecrypto: Bảo mật tối ưu cho kỷ nguyên lượng tử

Apple công bố quy trình xác minh hình thức cho corecrypto: Bảo mật tối ưu cho kỷ nguyên lượng tử

Sự ra đời của mật mã học an toàn trước lượng tử (quantum-secure cryptography) trong iMessage đã đánh dấu một bước chuyển đổi an ninh quan trọng nhằm bảo vệ người dùng Apple trước các mối đe dọa từ máy tính lượng tử trong tương lai. Để triển khai thế hệ thuật toán mới này trên quy mô lớn cho tất cả các nền tảng của Apple, chúng tôi đã phát triển các phương pháp xác minh hình thức (formal verification) nghiêm ngặt để chứng minh tính chính xác về mặt toán học của việc triển khai thực tế.

Với bản phát hành corecrypto mới nhất, Apple công bố các triển khai thuật toán ML-KEM và ML-DSA an toàn trước lượng tử, cùng với các bằng chứng toán học được xây dựng để đảm bảo chúng tuân thủ đúng các đặc tả FIPS 203 và FIPS 204. Hơn nữa, để thúc đẩy hơn nữa nghệ thuật đảm bảo phần mềm quan trọng, chúng tôi cũng công bố các thư viện và công cụ xác minh hình thức được tạo ra để đạt được kết quả chính xác mạnh mẽ nhất cho bất kỳ triển khai sản xuất nào được sử dụng rộng rãi hiện nay.

Tầm quan trọng của corecrypto và thách thức mới

Vào năm 2024, Apple đã thêm mã hóa hậu lượng tử vào corecrypto, thư viện mật mã nền tảng trong các hệ điều hành của Apple. Để đối phó với mối đe dọa đã được chứng minh từ các máy tính lượng tử trong tương lai, chúng tôi đã tập trung phát triển và triển khai mật mã học an toàn trước lượng tử mạnh mẽ trong các lĩnh vực mang lại lợi ích lớn nhất: các ứng dụng liên quan đến truyền thông được mã hóa và thông tin nhạy cảm, bao gồm iMessage, VPN và mạng TLS.

corecrypto được sử dụng liên tục trong các sản phẩm của Apple, cung cấp mã hóa và giải mã, băm, tạo số ngẫu nhiên và chữ ký số trên hơn 2,5 tỷ thiết bị đang hoạt động. Một lỗi nghiêm trọng trong corecrypto có khả năng làm tổn hại an ninh và độ tin cậy của mọi ứng dụng và tính năng phụ thuộc vào nó. Do đó, chúng tôi cực kỳ thận trọng khi thêm mã mới vào thư viện và nỗ lực hết mình để đảm bảo tính toàn diện trong quá trình kiểm thử.

Chúng tôi chỉ bao gồm các thuật toán mật mã mới vào corecrypto sau khi đánh giá kỹ lưỡng dựa trên các tiêu chí: cải thiện an ninh, thiết kế an toàn, hiệu suất cao và thông số nhỏ gọn. Khi một thuật toán đáp ứng các tiêu chuẩn cao của chúng tôi, chúng tôi phát triển một bản triển khai phải đảm bảo: An toàn (không rò rỉ thông tin), Tối ưu hóa (tận dụng tối đa kiến trúc silicon), và Chính xác (tuân thủ đúng tiêu chuẩn).

Tại sao cần Xác minh hình thức?

Xác minh hình thức sử dụng các bằng chứng toán học để chứng minh rằng một hệ thống hoặc đối tượng thỏa mãn các thuộc tính cụ thể mà chúng tôi định nghĩa. Tại Apple, chúng tôi đã thực hiện xác minh hình thức rộng rãi trong phát triển silicon hơn 15 năm, và bắt đầu sử dụng nó để chứng minh mật mã học cổ điển từ năm 2019.

Đối với corecrypto, chúng tôi sử dụng bằng chứng toán học để chỉ ra rằng các triển khai thuật toán của mình chính xác ở mức độ đảm bảo cao hơn đáng kể so với kiểm thử phần mềm thông thường. Nếu chúng ta có thể chứng minh rằng công thức toán học của việc triển khai tương đương với công thức của đặc tả kỹ thuật, thì chúng ta biết rằng việc triển khai sẽ tạo ra kết quả đầu ra đúng.

Tuy nhiên, các cân nhắc thực tế phức tạp hơn. Xác minh hình thức đòi hỏi sự đầu tư lớn về thời gian và chuyên môn sâu sắc. Việc triển khai và đặc tả kỹ thuật của nó phải được biểu diễn bằng các công thức toán học được lựa chọn cẩn thận. Do các công thức kết quả có thể cực kỳ lớn, việc viết các bằng chứng toán học và làm chủ các công cụ để xác minh từng bước đòi hỏi kỹ năng kỹ thuật chuyên biệt.

Quy trình xác minh hình thức của Apple

Chiến lược tùy chỉnh và Công cụ sử dụng

Để tìm ra cách tiếp cận đúng đắn, chúng tôi đã đánh giá một số công cụ xác minh và các triển khai đã được xác minh hiện có. Hầu hết không đáp ứng các yêu cầu của chúng tôi về việc hỗ trợ nhiều ngôn ngữ (C và ARM64 assembly), sự tiến hóa mã nhanh và các công cụ phát triển hiện có.

Cuối cùng, chúng tôi đã thiết kế một cách tiếp cận tùy chỉnh cho xác minh hình thức, kết hợp các công cụ hiện có với các công cụ mới để hỗ trợ các yêu cầu hoàn chỉnh và theo đuổi các bằng chứng từ trên xuống dưới (top-to-bottom) từ bản triển khai cuối cùng quay trở lại các đặc tả FIPS cho ML-KEM và ML-DSA.

Quy trình sử dụng các công cụ mã nguồn mở sau:

• Isabelle: Ngôn ngữ hình thức và trợ lý bằng chứng mạnh mẽ để xác minh các bằng chứng toán học phức tạp.
• Software Analysis Workbench (SAW): Công cụ do Galois phát triển để xác minh hình thức các thuộc tính của chương trình phần mềm.
• Cryptol: Ngôn ngữ hình thức hoạt động với SAW.
• cryptol-to-isabelle: Công cụ mới do Galois tạo ra theo đặc tả của Apple để dịch các mô hình thuật toán Cryptol sang công thức trong Isabelle.

Quy trình bao gồm việc dịch thủ công việc triển khai C di động sang ngôn ngữ Cryptol, sau đó sử dụng SAW để xác minh mô hình Cryptol khớp với việc triển khai C. Sau đó, một trình dịch chuyên dụng chuyển mô hình Cryptol sang Isabelle để so sánh với đặc tả Isabelle của thuật toán. Cuối cùng, chúng tôi chứng minh sự tương đương của từng chương trình con ARM64 với chương trình con C mà nó thay thế, đảm bảo tính chính xác cho việc triển khai Assembly được tối ưu hóa thủ công.

Kết quả và Đóng góp cho cộng đồng

Quy trình xác minh hình thức của chúng tôi đã phát hiện ra các vấn đề mà kiểm thử thông thường sẽ không bắt được, cho phép chúng tôi giải quyết lỗi trước khi chúng đến được sản phẩm. Ví dụ, chúng tôi đã xác định một bước bị thiếu trong việc triển khai ML-KEM sớm, có thể gây ra lỗi đầu ra trong các trường hợp hiếm gặp. Chúng tôi cũng phát hiện ra một lỗi trong một bằng chứng của bên thứ ba và có thể sửa chữa độc lập.

Với việc phát hành mã nguồn corecrypto mới nhất, Apple đang chia sẻ những tiến bộ có ý nghĩa trong xác minh hình thức ứng dụng với cộng đồng mật mã toàn cầu, bao gồm chi tiết về cách tiếp cận và các công cụ chúng tôi đã sử dụng. Các thư viện lý thuyết Isabelle mới, bao gồm mô hình ARM64, khung tinh chỉnh, thư viện đại số tách SProp và các định dạng hóa FIPS, được công bố để cho phép công chúng sử dụng và đánh giá.

Cách tiếp cận tùy chỉnh mới này cho phép Apple đạt được mức độ đảm bảo tính chính xác chức năng cao nhất hiện có cho bất kỳ bản triển khai sản xuất nào của ML-KEM và ML-DSA được sử dụng rộng rãi.