Các nhà nghiên cứu từ Viện Nghiên cứu Tin học và Tự động hóa Nhà nước (INRIA), Nghiên cứu của Microsoft và Đại học Carnegie Mellon trình bày phiên bản dùng thử đầu tiên của thư viện tiền điện tử EverCrypt được phát triển trong khuôn khổ dự án Everest và sử dụng các phương pháp toán học để xác minh độ tin cậy chính thức.
Đối với khả năng và hiệu suất của nó, EverCrypt rất gần với các thư viện tiền điện tử hiện có (OpenSSL) nhưng, không giống như chúng, cung cấp thêm đảm bảo về độ tin cậy và bảo mật.
Ví dụ: quá trình xác minh tóm tắt để xác định các thông số kỹ thuật chi tiết mô tả tất cả các hành vi của chương trình và bằng chứng toán học rằng mã được viết đáp ứng các thông số kỹ thuật đã chuẩn bị.
Không giống như các phương pháp kiểm soát chất lượng dựa trên bằng chứng, xác minh cung cấp đảm bảo đáng tin cậy rằng chương trình sẽ chỉ chạy như dự định của nhà phát triển và không có các loại lỗi cụ thể.
Ví dụ: việc tuân thủ đặc điểm kỹ thuật đảm bảo làm việc an toàn với bộ nhớ và không có lỗi dẫn đến tràn bộ đệm, đến con trỏ tham chiếu, để truy cập vào các vùng bộ nhớ đã được giải phóng hoặc để giải phóng gấp đôi các khối bộ nhớ.
EverCrypt là gì?
EverCrypt cung cấp kiểm tra loại và giá trị mạnh mẽ- Một thành phần sẽ không bao giờ chuyển các tham số cho thành phần không tuân thủ khác và sẽ không có quyền truy cập vào trạng thái bên trong của các thành phần khác.
Hành vi đầu vào / đầu ra hoàn toàn phù hợp với các hành động hàm toán học đơn giản, được định nghĩa trong các tiêu chuẩn mật mã.
Để bảo vệ khỏi các cuộc tấn công trong các kênh của bên thứ ba, hành vi trong khi tính toán (ví dụ: khoảng thời gian thực thi hoặc sự hiện diện của quyền truy cập vào bộ nhớ nhất định) nó không phụ thuộc vào dữ liệu bí mật được xử lý.
Mã dự án được viết bằng ngôn ngữ chức năng F * (F sao) , cung cấp một hệ thống các loại và sàng lọc phụ thuộc, cho phép thiết lập các thông số kỹ thuật chính xác (mô hình toán học) cho các chương trình và đảm bảo tính đúng đắn và không có lỗi trong quá trình thực hiện bằng các công thức SMT và các công cụ kiểm tra phụ trợ.
Mã trong F * được phân phối theo giấy phép Apache 2.0 và các mô-đun cuối cùng trong C và trình hợp dịch theo giấy phép MIT.
Dựa trên mã tham chiếu F *, trình hợp dịch, C, OCaml, JavaScript được tạo và mã lắp ráp web.
Một số phần của mã chuẩn bị bởi dự án đã được sử dụng trong Firefox, nhân Windows , chuỗi khối của Tezos và VPN Wireguard.
Các thành phần của EverCrypt
Về bản chất, EverCrypt kết hợp hai dự án khác nhau trước đây từ HACL * và Vale, cung cấp một API thống nhất dựa trên chúng và làm cho chúng phù hợp để sử dụng trong các dự án thực tế.
HACL * được viết bằng Thấp* và mục tiêu của nó là cung cấp các nguyên bản mật mã để sử dụng trong các chương trình C họ sử dụng các API kiểu libsodium và NaCL.
Dự án Vale đã phát triển một ngôn ngữ cụ thể miền để tạo xác minh trong trình hợp dịch.
Khoảng 110 nghìn dòng mã HACL * bằng ngôn ngữ Low * và 25 nghìn dòng mã cho Vale được kết hợp và chúng được viết lại bằng khoảng 70 nghìn dòng mã bằng ngôn ngữ phổ thông F *, ngôn ngữ này cũng đang được phát triển như một phần của dự án Everest.
Phiên bản đầu tiên của thư viện EverCrypt triển khai các tính năng đã được xác minh các thuật toán mật mã sau đây được đề xuất trong phiên bản C hoặc trình lắp ráp (khi sử dụng.
Trong số này, nổi bật sau đây trên trang dự án:
- Thuật toán băm: tất cả các biến thể của SHA2, SHA3, SHA1 và MD5
- Mã xác thực: HMAC qua SHA1, SHA2-256, SHA2-384 và SHA2-512 để xác thực nguồn dữ liệu
- Thuật toán tạo khóa HKDF (Hàm mở rộng và trích xuất khóa dựa trên HMAC)
- Mã hóa luồng ChaCha20 (có sẵn phiên bản C không được tối ưu hóa)
- Thuật toán xác thực thư Poly1305 (MAC) (phiên bản C và trình hợp dịch)
- Giao thức Diffie-Hellman trên đường cong elip Curve25519 (phiên bản C và trình hợp dịch với các tối ưu hóa dựa trên hướng dẫn BMI2 và ADX)
- Chế độ mật mã khối AEAD (mật mã được xác thực) ChachaPoly (phiên bản C không được tối ưu hóa)
- Chế độ mã hóa khối AEAD AES-GCM (phiên bản trình hợp dịch với tối ưu hóa AES-NI).
Trước hết phiên bản alpha, xác minh mã đã hoàn thành phần lớn, nhưng vẫn còn một số khu vực được phát hiện.
Bên cạnh đó, API chưa ổn định, sẽ được mở rộng trong các phiên bản alpha sau (Nó được lên kế hoạch để thống nhất cấu trúc cho tất cả các API.
Trong số các sai sót, hỗ trợ cho kiến trúc x86_64 cũng được nhấn mạnh (trong giai đoạn đầu, mục tiêu chính là độ tin cậy, trong khi tối ưu hóa và nền tảng sẽ được thực hiện ở vị trí thứ hai).
Fuente: https://jonathan.protzenko.fr