Bài viết kỹ thuật

Phép toán đường cong NIST thuần Pascal cho ký PDF

HotPDF thực hiện thỏa thuận khóa đường cong elip và xác minh chữ ký cho PDF bằng Object Pascal thuần, không ràng buộc OpenSSL và không provider mật mã nền tảng nào trên đường đi. Điều đó phủ năm đường cong: P-256, P-384 và P-521 cho các họ số nguyên tố NIST, cộng X25519 và X448 cho thỏa thuận khóa trên đường cong Montgomery. Lý do để viết mã đó thay vì liên kết nó là triển khai, không phải sự thuần khiết. Một ứng dụng Delphi hay Free Pascal phát hành một tệp thực thi và không DLL mật mã nào thì không có lệch phiên bản để quản, không có provider theo nền tảng để phát hiện, và chẳng gì thay đổi hành vi khi khách hàng vá các thư viện hệ thống của họ

Cái giá là giờ bạn sở hữu phần phép toán. Phép nhân mô-đun số nguyên lớn là mã không khoan nhượng: nó hoặc tạo ra kết quả trùng từng byte với các test vector công bố, hoặc tạo ra rác trông có vẻ hợp lý, và khoảng cách giữa hai trạng thái đó có thể chỉ là một phép so sánh. Đây là câu chuyện của phép so sánh đó, vì hình dạng của bug khái quát hóa được cho bất kỳ bản chuyển nền Pascal nào của phép toán trường

Vì sao một thư viện PDF cần phép toán đường cong từ đầu?

Hai tính năng kéo nó vào. Thứ nhất là mã hóa khóa công khai của tài liệu: trình xử lý danh sách người nhận ISO 32000 bọc một khóa theo từng tài liệu cho các chứng chỉ được nêu tên, và khi một người nhận giữ khóa EC thì việc bọc chạy qua thỏa thuận khóa thay vì vận chuyển khóa RSA. Không có ECDH thì không có cách nào mở được loại tài liệu đó. Thứ hai là xác minh chữ ký. Xác minh một chữ ký ECDSA trên các byte /ByteRange cần một phép nhân điểm trên đường cong của người ký, và P-384 phổ biến trong các hồ sơ chính phủ và chữ ký đủ điều kiện, nơi P-256 được coi là sàn chứ không phải đích. HotPDF phơi kết quả của công việc đó qua con đường xác minh ECDSA và CMS và qua mô hình signature-provider cắm được

Sơ đồ nơi phép toán đường cong Pascal thuần của HotPDF được dùng: mã hóa ECDH danh sách người nhận và xác minh chữ ký ECDSA trên ByteRange
Thỏa thuận khóa mở các tài liệu mã hóa EC cho người nhận được nêu tên, còn xác minh chữ ký cần phép nhân điểm trên đường cong người ký

CIOS, và phép trừ duy nhất ở cuối

Phép nhân Montgomery tránh phép chia bằng cách làm việc trong một miền đã biến đổi nơi quy giản chỉ là một phép dịch. Biến thể HotPDF dùng là Coarsely Integrated Operand Scanning, thứ đan xen phép nhân và phép quy giản theo từng limb để phần trung gian không bao giờ vượt quá bề rộng mô-đun cộng thêm một limb. Thân vòng lặp thẳng thắn và dễ kiểm thử. Phần đuôi thì không: sau các lượt đan xen, bộ tích lũy có thể nằm bất cứ đâu trong khoảng tới hai lần mô-đun, nên thuật toán kết thúc bằng một phép trừ có điều kiện bỏ đi một bản sao của số nguyên tố nếu và chỉ nếu bộ tích lũy lớn hơn hoặc bằng nó

So sánh hai số nhiều limb nghĩa là đi từ limb có trọng số nhất xuống dưới trong khi mang một borrow. Cách viết hiển nhiên là so limb bộ tích lũy với limb mô-đun cộng borrow đi vào. Biểu thức đó sai, và nó sai theo cách mà phần lớn các đường cong giấu được

// Sai: P[I] + Borrow có thể tràn khi P[I] là $FFFFFFFFFFFFFFFF
if T[I] < P[I] + Borrow then
begin
  Borrow := 1;
  Break;
end;

// Đúng: so sánh mà không bao giờ cộng vào một limb
if (T[I] < P[I]) or ((T[I] = P[I]) and (Borrow = 1)) then
begin
  Borrow := 1;
  Break;
end;

Một tràn borrow thực ra trông như thế nào?

Nó trông như một đường cong chạy được ở mọi nơi trừ sản xuất. Các số nguyên tố của P-384 và P-521 chứa những limb toàn bit một, nên P[I] bằng $FFFFFFFFFFFFFFFF. Cộng borrow đi vào bằng một vào đó và một số nguyên 64-bit không dấu tràn về không. Phép so sánh sau đó hỏi liệu limb bộ tích lũy có nhỏ hơn không, kết luận là không, và kết luận rằng không cần borrow. Một limb của kết quả lệch đi một

Sơ đồ tràn borrow quy giản Montgomery đối chiếu phép so limb sai với lan truyền borrow đúng trong phép toán P-384 của HotPDF
Cộng borrow vào một limb toàn bit một tràn về không, nên P-384 và P-521 bỏ lỡ phép trừ trong khi P-256 giấu khuyết tật

P-256 thoát được vì chẳng limb nào của nó toàn bit một, nên phép cộng không bao giờ tràn và biểu thức lỗi tình cờ khớp với biểu thức đúng. Đó là kết quả tệ nhất có thể đối với một bộ kiểm thử: đường cong được thử nhiều nhất thì qua, các đường cong được thử ít hơn thì thất bại chốc chốc tùy giá trị toán hạng, và thất bại lộ ra dưới dạng kết quả xác minh "chữ ký không hợp lệ" trên những tài liệu hoàn toàn hợp lệ. HotPDF từng mang một cổng tường minh trên P-384 chính vì lý do này, trả về trạng thái không khả dụng thay vì một câu trả lời sai, cho đến khi phép toán được chứng minh với các vector tham chiếu

Con bug thực sự được định vị ra sao

Không phải bằng cách đọc mã. Chuỗi hiệu quả là cơ học, và nó dùng lại được. Thứ nhất, loại trừ các hằng số: mọi limb của p, RR^2 được tái sinh độc lập và so từng limb một, điều này loại bỏ nguồn phổ biến nhất của bug đường cong. Thứ hai, gắn công cụ vào phép toán chứ không phải API: một thủ tục dump tạm thời in các giá trị trung gian của phép nhân Montgomery của R^2, của x^3, và của y^2 cho một điểm đã biết, để chúng có thể được đối chiếu với chân lý được tính độc lập

Phép so sánh đó chỉ thẳng vào thủ phạm. Chuỗi x đúng từ đầu đến cuối, trong khi y^2 lệch ở đúng một limb đi đúng một đơn vị. Một khác biệt một limb đi một không phải bug nhân, bug lan truyền carry, hay bug hằng số; nó là bug chuỗi borrow, và chuỗi borrow duy nhất trong routine là phép trừ có điều kiện cuối cùng. Một chi tiết suýt làm trật đường: hằng tham chiếu dùng cho bản dump tự thân bị viết sai thứ tự byte ngay lần đầu, điều tạo ra một sự lệch ở giá trị y và thoáng gợi ý một khuyết tật thứ hai không tồn tại. Hãy xác minh endianness của chân lý cơ sở trước khi tin nó để buộc tội mã của bạn

Sơ đồ dòng cách con bug đường cong HotPDF được định vị bằng tái sinh hằng số, dump các giá trị trung gian Montgomery và diff với chân lý mirror
Một khác biệt một limb đi đúng một chỉ thẳng vào chuỗi borrow duy nhất trong routine, và một tham chiếu đảo byte suýt đánh lạc hướng cuộc săn

Những cái bẫy láng giềng trong cùng routine

Ba dạng thất bại nữa nằm trong vài dòng của phép so sánh đó, và cả ba đều từng sống động vào lúc nào đó trong quá trình phát triển

// 1. Bộ tích lũy có một limb trên bề rộng mô-đun. Chỉ so L limb thấp
//    bỏ sót trường hợp T đúng bằng p cộng 2^(64*L), thứ xảy ra với một
//    tỷ lệ đáng kể các đầu vào ngẫu nhiên vì 2p vượt 2^256 cho P-256
//    và 2^384 cho P-384
if (T[L] <> 0) or NotLessThanModulus(T, P, L) then
  SubtractModulus(T, P, L);

// 2. Một phép trừ nhiều limb chung chung có cùng mối nguy tràn: khi
//    Y[I] là $FFFFFFFFFFFFFFFF, Y[I] + Borrow tràn về không và borrow
//    phải sống sót sang limb kế tiếp thay vì bị xóa
Diff := X[I] - Y[I] - Borrow;
NextBorrow := Ord((X[I] < Y[I]) or ((X[I] = Y[I]) and (Borrow = 1)));

Thứ ba không phải mã, mà là nguồn gốc. Số nguyên tố của P-521 ban đầu được chép với 130 chữ số thập lục phân thay vì 131, thiếu một chữ F, và các hằng Montgomery sau đó được tính từ số nguyên tố sai đó, nên các hằng tự nhất quán và cùng nhau sai. Tham số đường cong phải được suy ra, không bao giờ gõ tay: tính R bằng (1 shl (64 * L)) mod p từ số nguyên tố bạn thực sự dùng, rồi kiểm tra chéo R * R mod p với giá trị mà hằng R^2 của bạn tuyên bố. Một cặp hằng khớp với nhau chẳng chứng minh điều gì về bất kỳ cái nào

Chiến lược xác minh mở rộng được ra ngoài một đường cong

Kỹ thuật khiến X25519 và X448 khả thi là viết một hiện thực mirror bằng một ngôn ngữ có số nguyên không giới hạn và chép luồng điều khiển Pascal vào đó từng dòng một. Khi mirror cho ra câu trả lời đúng còn Pascal thì không, khuyết tật là một chỗ chép trượt và dò cùng một giá trị trung gian trong cả hai hiện thực tìm ra nó trong vài giây. Cả ba lỗi thang kinh điển của RFC 7748 đều được bắt theo cách này: một swap thời gian hằng mà dòng thứ hai dùng lại giá trị đã swap, một nghịch đảo cuối trả về z luỹ thừa trừ một thay vì nhân nó vào X, và một phép nhân hằng nhỏ lắp các tích nửa từ bằng bitwise or và đánh mất carry

Với vật liệu kiểm thử, hãy lấy vector dưới dạng byte thay vì dạng văn bản. Trích xuất khóa riêng bằng một mẫu văn bản là cách một hiện thực đúng bị buộc tội lỗi lệch một byte mà hoàn toàn nằm ở bước trích xuất. Cắt phần hex ra khỏi mã hóa DER tại các offset đã biết và so mảng byte

Với chuỗi borrow đã sửa, cả năm đường cong khớp các vector tham chiếu công bố từng byte một, và HotPDF không còn cổng đường cong nào. Nếu bạn đang tích hợp ký dựa trên chứng chỉ hoặc mã hóa danh sách người nhận, bài học thực tiễn là lựa chọn đường cong giờ là một quyết định chính sách chứ không phải câu hỏi năng lực; các hồ sơ và cạm bẫy thứ tự byte phía ký được đề cập trong hướng dẫn từng bước ký PAdES. Chi tiết thành phần và ma trận thuật toán được hỗ trợ nằm trên trang sản phẩm HotPDF Delphi PDF component