Bài viết kỹ thuật

Ed448 và Brainpool ECDSA thuần Pascal cho PDF

PDFlibPas ký và xác minh bằng Ed448 và bằng ba đường cong ECDSA Brainpool trong Object Pascal thuần. Không thư viện mật mã ngoài, không platform provider, không DLL: PDFlibEd448 triển khai PureEdDSA theo RFC 8032 trên edwards448, và PDFlibBrainpool triển khai brainpoolP256r1, brainpoolP384r1 và brainpoolP512r1 theo RFC 5639. Cả hai đều được xây dựng theo cùng một cách, đối chiếu với các known-answer vector được sinh độc lập trước khi bất kỳ dòng Pascal nào được viết, và cả hai đều đáng để viết về, chủ yếu là vì những con bug

Phép toán trên trường (field arithmetic) là loại mã trung thực một cách hiếm có. Nó hoặc khớp với các vector công bố từng byte một, hoặc không, nên không có khoảng trống cho kiểu "chủ yếu là chạy được". Điều khiến nó khó là một hiện thực sai vẫn tạo ra chữ ký, vẫn xác minh được chính chữ ký của nó, và vẫn trông hoàn toàn hợp lý

Vì sao là các đường cong này, và vì sao viết bằng Pascal

Các đường cong Brainpool xuất hiện trong các hồ sơ chữ ký đủ điều kiện (qualified signature) của châu Âu, nên một thư viện ký tài liệu cho thị trường đó không thể coi chúng là hiếm gặp. Ed448 nằm trong bộ thuật toán mà ISO/TS 32002 mang đến cho PDF, với digest nội bộ là SHAKE256 thay vì SHA-2. Cả hai họ đều không có sẵn trong các thư viện mật mã Pascal thông dụng, nên một thư viện PDF muốn có chúng thì phải tự sở hữu chúng

Luật lẽ triển khai cũng là luận điểm áp dụng cho toàn bộ phần mật mã của thư viện này: một ứng dụng phát hành một binary duy nhất không phụ thuộc mật mã thì không có provider để phát hiện, không có phiên bản để khớp, và không có hành vi nào thay đổi khi máy chủ được vá. Ký số chính là lĩnh vực mà bạn ít muốn một phụ thuộc luôn dịch chuyển nhất

Hằng số lấy từ văn bản đặc tả, không bao giờ lấy từ trí nhớ

Lần thử đầu với điểm base của edwards448 được viết từ trí nhớ và đã sai. Đó không phải là một lỗi đáng chú ý gì nhưng lại rất đắt đỏ, vì một điểm base sai tạo ra một hệ thống tự nhất quán: sinh khóa, ký và xác minh của bạn đều khớp với nhau và bất đồng với phần còn lại của thế giới

Quy trình làm việc là lấy mọi tham số miền (domain parameter) từ văn bản đặc tả, rồi kiểm tra chéo. Với edwards448, điều đó nghĩa là số nguyên tố, hằng số đường cong, bậc của nhóm (group order) và cả hai tọa độ thập phân của điểm base lấy từ RFC 8032, chuyển sang biểu diễn limb nội bộ, rồi đối chiếu với các test vector công bố trong chính tài liệu đó. Với các đường cong Brainpool, điều đó nghĩa là các tham số từ RFC 5639, một hiện thực độc lập được viết ra để sinh vector, và một lần kiểm tra chéo với một thư viện hệ thống theo cả hai chiều trước khi bất kỳ dòng Pascal nào chạy

Tham số miền Ed448 và Brainpool chảy từ văn bản đặc tả RFC 8032 và RFC 5639 sang dạng limb và được kiểm tra chéo trước khi bất kỳ dòng Pascal nào chạy
Tham số miền cho edwards448 và các đường cong Brainpool được lấy từ văn bản RFC, chuyển sang dạng limb và kiểm tra chéo với các vector độc lập

Một con đường tắt khi suy ra tham số xứng đáng được cảnh báo vì nó trông có vẻ phổ quát nhưng không phải: tái tạo điểm base từ một giá trị y cố định chỉ đúng với đường cong 25519 và không đúng với edwards448, nơi giá trị đó không có căn bậc hai. Một đoạn script đã bác bỏ nó trong vài giây, rẻ hơn nhiều so với việc phát hiện ra qua debugger

Phương pháp: một bản mirror ở mức limb trước bất kỳ dòng Pascal nào

Kỹ thuật khiến cả hai unit khả thi là một hiện thực mirror trong một ngôn ngữ có số nguyên không giới hạn, được dựng từ dưới lên. Trước hết là riêng tầng số học: nhân trường, trừ và lan truyền carry, được thử sức chống lại các bất biến đại số của chúng qua vài trăm ca ngẫu nhiên. Sau đó là sinh khóa hoàn chỉnh bên trong mirror, nơi các bug ngữ nghĩa cư trú và nơi chúng rẻ để tìm ra. Cuối cùng mới là bản chép sang Pascal

Quy trình của một hiện thực mirror với số nguyên không giới hạn để kiểm chứng phép toán trường Pascal và sinh khóa cho Ed448 và Brainpool
Quy trình mirror từ dưới lên: số học trước, rồi sinh khóa bên trong mirror, sau đó là bản chép sang Pascal và so sánh giá trị trung gian

Lợi ích mang tính chẩn đoán hơn là phát triển. Khi mirror đã được biết là đúng, bất kỳ sự bất đồng nào giữa mirror và Pascal đều là một chỗ chép sai, và việc dò cùng một giá trị trung gian trong cả hai hiện thực sẽ định vị ngay. Điều đó biến một lớp bug mà nếu không thì gần như không thể debug — một limb sai duy nhất nằm sâu trong phép nhân vô hướng — thành một phép so sánh năm phút

Bốn nguyên nhân gốc trong Ed448

Cả bốn đều được tìm ra bằng cách dò giá trị trung gian, và cả bốn đều thuộc loại tạo ra đầu ra trông có vẻ hợp lệ

Thứ nhất là cái bẫy ký hiệu. Phần lớn công thức cộng Edwards thuần nhất được công bố giả định hằng số đường cong bằng trừ một, trong khi edwards448 là cộng một. Mang nguyên trạng sang, tử số của tọa độ y bị viết thành tổng trong khi lẽ ra phải là hiệu. Cách sửa không phải là vá dấu mà là suy lại dạng tích không cần nghịch đảo từ luật cộng affine cho đúng đường cong, cách này tạo ra bốn biểu thức tọa độ và không chừa chỗ nào cho dấu được thừa kế từ nguồn sai

Thứ hai nằm ở phép giải nén điểm. Tái tạo tọa độ affine x từ tọa độ projective cần đúng một phép nhân với nghịch đảo của Z. Nhân với nghịch đảo bình phương cho ra một giá trị vẫn là biểu diễn projective hợp lệ nhưng là tọa độ affine sai, nên triệu chứng là y đúng kèm x sai. Bất cứ khi nào một tọa độ đúng còn tọa độ kia sai, bug nằm ở khâu chuẩn hóa, không nằm ở phép toán

Thứ ba là một thói quen nhập khẩu từ đường cong ngắn hơn. Cả scalar từng chữ ký lẫn scalar challenge đều phải được quy giản từ digest đầy đủ — với Ed448 là 114 byte — chứ không phải từ 57 byte đầu. Đường cong 32 byte cũng dùng trọn digest 64 byte của nó, nên quy luật là nhất quán; thứ sai chỉ là giả định "một nửa digest chính là bề rộng scalar"

Thứ tư là thứ tự. Prefix phân tách miền (domain separation) đứng trước, trước prefix ngữ cảnh và thông điệp, một thứ tự mà cách đọc trực giác các giá trị RA trong đặc tả không gợi ra. Làm sai chỗ này tạo ra những chữ ký chỉ xác minh được với hiện thực của chính bạn và không gì khác, kiểu thất bại gây hiểu lầm nhất có thể

// Thiết kế carry trường: lan truyền thuần ngữ nghĩa floor, nên cả
// limb dương lẫn limb âm đều chạy và phép trừ không cần bias.
// Carry trên cùng quay về qua 2^448 = 2^224 + 1 (mod p), chạm vào
// limb 0 và limb 8. Giới hạn bốn vòng; thực tế quan sát được hai vòng
procedure FeCarry(var A: TFe448);
var
  I, Round: Integer;
  Carry: Int64;
begin
  for Round := 1 to 4 do
  begin
    Carry := 0;
    for I := 0 to 15 do
    begin
      A[I] := A[I] + Carry;
      Carry := Floor28(A[I]);          // floor chứ không phải truncation
      A[I] := A[I] - (Carry shl 28);
    end;
    if Carry = 0 then
      Break;
    A[0] := A[0] + Carry;              // 2^448 == 1
    A[8] := A[8] + Carry;              // 2^448 == 2^224
  end;
end;

Một phiên bản trước của routine này áp dụng bias trước khi lan truyền, và với đầu vào lớn nó gộp một carry giả có độ lớn sai vào các limb thấp. Các sơ đồ carry dựa trên bias là nguồn lặp đi lặp lại của lớp khuyết tật này; ngữ nghĩa floor với vòng lặp có giới hạn dễ suy luận hơn và theo phép đo thì nhanh đủ dùng

Hai nguyên nhân gốc trong Brainpool

Thứ nhất thậm chí không phải là mật mã học. Biểu diễn làm việc gồm 33 limb, nên tích của hai giá trị cần 66, còn mảng tích lại được khai báo 64. Ghi tràn quá cuối làm hỏng bộ nhớ liền kề, biểu hiện đầu tiên là kết quả sai và chỉ trở thành crash sau khi một bước quét rộng hơn được thêm vào. Quy luật rút ra từ đó đáng áp dụng cho mọi bộ đệm số có kích thước cố định: đặt kích thước theo bề rộng tích trong trường hợp xấu nhất rồi cộng thêm biên, sau đó không bao giờ phải nghĩ đến nó nữa. Mảng trong mã phát hành là 68 limb

Thứ hai là một dạng lũy thừa bị trộn lẫn. Có hai dạng square-and-multiply đúng và chúng tiêu thụ số mũ theo hai hướng ngược nhau: dạng phải-sang-trái nhân rồi bình phương cơ số và phải đọc bit từ đầu ít trọng số nhất, trong khi dạng trái-sang-phải bình phương rồi nhân và đọc từ đầu có trọng số nhất. Vòng lặp nghịch đảo mô-đun từng có thân phải-sang-trái đi kèm bước đi bit trọng số-trước. Cả hai nửa đều nằm trong sách giáo khoa, sự kết hợp thì không, và kết quả là một nghịch đảo sai mà vẫn trông như một phần tử trường hợp lệ

Hai dạng lũy thừa square-and-multiply với hướng bit ngược nhau và dạng trộn lẫn đã tính ra các nghịch đảo mô-đun Brainpool sai
Từng dạng square-and-multiply đều tự nó đúng; ghép thân phải-sang-trái với bước đi bit trọng số-trước cho ra một nghịch đảo sai nhưng trông hợp lý
// Nhân đôi và cộng điểm Jacobian khi record đích có thể trùng biến
// với một record nguồn. Sao chép nguyên record ngay khi vào là lời
// phòng thủ đáng tin duy nhất: ghi các limb của R làm bẩn các lần
// đọc P sau đó
procedure BPPointDouble(var R: TBPPoint; const P: TBPPoint;
  const Curve: TBPCurve);
var
  Pin: TBPPoint;
begin
  Pin := P;        // sao chép trước, rồi chỉ tính từ Pin
  // ... M = 3X^2 + A*Z^4, S = 4*X*Y^2, X3 = M^2 - 2S, ...
end;

Hai bài học quy trình đắt hơn cả những con bug

Vá nóng theo kiểu tăng dần không hội tụ với một unit mật mã. Một bản thảo đã bị vá đi vá lại đến mức mang 32 routine trùng lặp và một cấu trúc tổn thương, và chỉ được giải quyết bằng cách viết lại. Mô hình nên chọn là hoặc viết một lần từ mirror đã được kiểm chứng, hoặc viết lại; một chuỗi vá cục bộ lên phần số học mà bạn chưa hiểu sẽ tích lũy nhanh hơn nó sửa

Và hãy kiểm tra timestamp trên tệp thực thi trước khi tin một kết quả kiểm thử. Một bản build tăng dần biên dịch được nhưng không liên kết lại sẽ chạy binary trước đó, và điều đó đã tạo ra cả một vòng manh mối sai về các probe thiếu và đầu ra trùng lặp. Khi debug mật mã, một kết quả không giải thích được nên gợi ra câu hỏi "đây có phải binary tôi vừa build không" trước câu hỏi "thuật toán có sai không"

Hiệu năng, phạm vi và cách gọi

Quy giản mô-đun trong unit Brainpool là dạng shift-subtract tuần tự bit bắt đầu từ bit bật cao nhất của tích, nên một phép nhân tốn cỡ theo bậc bề rộng bit. Một lần xác minh P-256 rơi vào vùng vài trăm mili-giây đầu, điều này chẳng có gì đáng nói với ký hay xác minh tài liệu và sẽ không đủ cho một TLS terminator. Quy giản Barrett là bản nâng cấp hiển nhiên nhưng cần một giá trị làm việc rộng hơn biểu diễn hiện tại mang được, nên đó là thay đổi để thực hiện khi khối lượng công việc đòi hỏi chứ không phải làm phòng ngừa từ trước

uses
  PDFlibEd448, PDFlibBrainpool;

var
  PublicKey, Signature: AnsiString;
  Curve: TBPCurve;
  R, S, PubX, PubY: TBPValue;
begin
  // Ed448: PureEdDSA, SHAKE256 bên trong, khóa 57 byte
  if Ed448PublicKeyFromSeed(Seed, PublicKey) and
     Ed448Sign(DocumentDigest, Seed, Signature) then
    Assert(Ed448Verify(DocumentDigest, PublicKey, Signature));

  // Brainpool: caller tự cung cấp nonce từng chữ ký, nên chính sách
  // nonce nằm với ứng dụng
  Curve := BPLoadCurve(bpP256r1);
  if BPKeyGen(PubX, PubY, PrivateD, Curve) and
     BPSignFixedK(R, S, Hash, PrivateD, Nonce, Curve) then
    Assert(BPVerify(R, S, Hash, PubX, PubY, Curve));
end;

Lưu ý rằng điểm vào ký Brainpool nhận nonce thay vì tự sinh ra. Điều đó là có chủ đích: sinh nonce là thứ duy nhất mà khi sai thì thảm họa nhất trong ECDSA, vì một giá trị lặp lại hoặc đoán được sẽ làm lộ khóa riêng, và quyết định về nơi mà tính ngẫu nhiên đến từ đâu thuộc về ứng dụng và chế độ tuân thủ của nó, không thuộc về một thư viện PDF

Các đường cong này đứng cạnh phần hậu lượng tử được mô tả trong bài viết về FIPS 204 ML-DSA, và chúng cắm vào cùng một pipeline ký và xác thực được trình bày trong ký và xác thực PAdES. Để có chứng chỉ kiểm thử trên các đường cong này, con đường sinh cục bộ được mô tả trong chứng chỉ tự ký với CryptoAPI. Toàn bộ ma trận thuật toán được liệt kê trên trang sản phẩm losLab PDF Developer Library