Giới thiệu: Xác minh chính thức tính hữu hạn của cơ chế đồng thuận Gasper
Lưu ý của biên tập viên: Bài viết này đến từNhững người đam mê Ethereum (ID: ethfans)Lưu ý của biên tập viên: Bài viết này đến từ
Những người đam mê Ethereum (ID: ethfans)
Những người đam mê Ethereum (ID: ethfans)
Gasper là một lớp giao thức bằng chứng cổ phần trừu tượng được triển khai bởi giao thức chuỗi đèn hiệu (giao thức cơ bản của mạng Ethereum 2.0 sắp tới). Phần quan trọng của Gasper là một bộ cơ chế tài chính, được sử dụng để đảm bảo độ bền của các giao dịch và hoạt động liên tục của hệ thống sẽ không bị phá hủy bởi các cuộc tấn công.
Gasper
Chúng tôi vui mừng thông báo một cột mốc quan trọng khác trong sự hợp tác lâu dài giữa Runtime Verification và Ethereum Foundation: chúng tôi đã phát triển một khung chính thức để mô phỏng và xác minh giao thức chuỗi đèn hiệu, đồng thời chính thức chứng minh thành công tính đúng đắn của Gasper; đồng thời, chúng tôi cũng sử dụng những kết quả này để chứng minh rằng việc triển khai trừu tượng hóa Gasper của chuỗi đèn hiệu cũng sở hữu các thuộc tính này. Bạn có thể tìm thấy cả mô hình và tập lệnh kiểm chứng tại đây.
tiêu đề cấp đầu tiên
Giao thức chuỗi đèn hiệu là một bộ giao thức bằng chứng cổ phần mới, là cốt lõi của bản nâng cấp lớn trong tương lai của Ethereum "Ethereum 2.0". Trong giao thức chuỗi đèn hiệu, các nút tham gia (hoặc "người xác minh") đều có tiền gửi (cổ phần, dưới dạng ETH) trong hệ thống. Trình xác thực xác nhận tính hợp lệ của các khối và bỏ phiếu cho các thuộc tính khác nhau bằng cách gửi "chứng thực" cho mạng. Bản thân giao thức chuỗi đèn hiệu bao gồm một số công cụ để giúp những người xác thực đạt được sự đồng thuận về trạng thái mới nhất của chuỗi khối.
Gasper đề xuất một mô tả trừu tượng nhưng chính xác về tiện ích cuối cùng trong giao thức chuỗi đèn hiệu và cũng xác định các quy tắc lựa chọn ngã ba; tiện ích cuối cùng được sử dụng để xác định những khối nào sẽ được người tham gia xem xét hoàn thiện Quy tắc lựa chọn ngã ba được sử dụng để xác định ngã ba nào là chuỗi chính khi chuỗi rẽ nhánh. Finality trong Gasper khái quát hóa một khái niệm bắt nguồn từ bài báo "Casper Friendly Finality Gadget (Casper FFG)", đưa ra "hoàn thiện" ở dạng tổng quát hơn.
tiêu đề phụ
Biện minh và hoàn thiện
Khái niệm về tính hữu hạn chỉ liên quan đến "khối điểm kiểm tra" (còn được gọi là "khối ranh giới kỷ nguyên", là các khối ở đầu kỷ nguyên). Một phần của thông báo chứng thực được gọi là "phiếu hợp lý hóa". Trong phiếu hợp lý hóa, người xác minh liên kết khối điểm kiểm tra nguồn với khối điểm kiểm tra đích sau đó, biểu thị trực quan rằng người xác thực đã khởi tạo chứng thực tin rằng "chúng ta có thể di chuyển từ trạng thái điểm kiểm tra nguồn sang trạng thái của điểm kiểm tra đích". Trên thực tế, một biểu quyết chứng minh cho thấy: (1) người xác thực đã bắt đầu biểu quyết; (2) điểm kiểm tra nguồn và chiều cao chứng minh của nó; (3) điểm kiểm tra mục tiêu và chiều cao chứng minh của nó.
Nếu và chỉ khi các điều kiện được đáp ứng: (1) điểm kiểm tra nguồn B0 đã được hợp lý hóa; (2) đa số (tức là ít nhất 2/3 số người xác thực) cũng đã bỏ phiếu cho cặp nguồn-đích B0-B1; thì điểm kiểm tra mục tiêu B1 Nó được hợp lý hóa thông qua điểm kiểm tra nguồn B0.
B0 đạt được mức cuối cùng của thứ tự K (k > 0) và tất cả các điểm kiểm tra giữa B0 và Bk được hoàn thành khi và chỉ khi phần lớn trình xác thực liên kết B0 với điểm kiểm tra hậu duệ thế hệ K của nó Bk. Lưu ý rằng bản thân khối gốc được coi là hợp lý hóa và cuối cùng. Sơ đồ dưới đây thể hiện các khái niệm hợp lý hóa và hoàn thiện trong Gasper.
Nếu người xác thực cố gắng đi chệch khỏi giao thức và gửi các phiếu bầu trái ngược nhau, thì người xác thực đó sẽ bị phạt: một phần lớn tiền gửi của họ sẽ bị khấu trừ. Gasper định nghĩa hai điều kiện (còn được gọi là điều kiện cắt giảm) để xác định điều gì tạo nên một cuộc bỏ phiếu mâu thuẫn:
Bỏ phiếu xung quanh: Hai điểm kiểm tra được liên kết với phiếu bầu do người xác thực đưa ra nằm chính xác trong phạm vi chiều cao của hai điểm kiểm tra của một phiếu bầu khác do người xác thực đưa ra.
chữ
Trình xác thực bắt đầu biểu quyết kép được coi là đã vi phạm điều kiện gạch chéo đầu tiên; trình xác nhận bắt đầu biểu quyết bao bọc vi phạm điều kiện dấu gạch chéo thứ hai. Trong cả hai trường hợp, những người xác nhận vi phạm quy tắc sẽ bị khấu trừ một khoản tiền lớn.
tiêu đề phụ
Tính đúng đắn (Thuộc tính đúng đắn)
Giống như các giao thức Byzantine Fault Tolerance (BFT) khác, giả định cơ bản chính của giao thức Gasper là phần lớn người xác minh (hơn 2/3, được xác định bằng số tiền gửi) là trung thực và sẽ tuân theo các yêu cầu của giao thức. Theo giả định này, Gasper có hai thuộc tính cơ bản:
An toàn có trách nhiệm: Sẽ không có hai khối thuộc các nhánh khác nhau được hoàn tất trừ khi ít nhất 1/3 số người xác thực (về số tiền gửi) bị cắt giảm;
Tính sống động hợp lý: Bất kể điều gì đã xảy ra với chuỗi khối trong quá khứ, quá trình hoàn thiện khối sẽ không bao giờ bị bế tắc.
Hơn nữa, trong một môi trường mà tập hợp các trình xác thực thay đổi linh hoạt (khi các trình xác thực rời khỏi mạng và các trình xác nhận mới tham gia, nhóm các trình xác thực đang hoạt động có thể thay đổi), thuộc tính thứ ba định lượng khi ai đó vi phạm các quy tắc của giao thức. có thể bị tịch thu:
Giới hạn có thể cắt giảm: Miễn là các điều kiện giao thức bổ sung có thể được sử dụng để kiểm soát việc kích hoạt trình xác thực và các điều kiện tham số thoát, thì có thể chứng minh rằng (khi vi phạm bảo mật) sẽ có giới hạn dưới đối với số tiền gửi có thể bị cắt giảm.
Một bộ trình xác thực động (là thứ mà giao thức Beacon Chain triển khai) gây ra một vấn đề thách thức khác: hệ thống không còn có thể trừng phạt những trình xác nhận độc hại một cách đáng tin cậy, vì chúng có thể làm như vậy sau khi chúng đã làm điều gì đó xấu nhưng trước khi gửi tiền thực sự là bị chém.Rời khỏi mạng. Thuộc tính giới hạn dưới có thể cắt giảm cho phép điều chỉnh phạm vi biến của bộ trình xác thực đang hoạt động và duy trì mức trách nhiệm giải trình tối thiểu.
Xác minh tính hữu hạn của Gasper
Mục đích của Gasper là cung cấp một mô tả toán học chính xác về tính hữu hạn có thể được sử dụng để chính thức chứng minh tính đúng đắn của nó; tính đúng đắn này cũng là chìa khóa để chứng minh tính bảo mật của giao thức chuỗi đèn hiệu. Nền tảng Ethereum ngày càng được sử dụng làm giá cổ phiếu cho các hệ thống giao dịch tài chính lớn, làm nổi bật tầm quan trọng chưa từng có của việc đảm bảo an ninh.
Phối hợp với Ethereum Foundation, chúng tôi đã chính thức hóa cơ chế cuối cùng của Gasper trong điều kiện chung của các bộ xác thực động bằng cách sử dụng trình trợ giúp bằng chứng Coq. Chúng tôi chỉ ra và chứng minh cả ba thuộc tính chính của Gasper trong điều kiện này: an toàn có trách nhiệm, khả năng sống động và giới hạn dưới có thể cắt giảm; tất cả các bằng chứng đều sử dụng cùng một mô hình Coq.
Ở đây chúng tôi chỉ kể sơ lược về thành tích này. Chi tiết đầy đủ có sẵn tại:
Báo cáo kỹ thuật dự án
Kho lưu trữ Github của dự án
tiêu đề phụ
Phương pháp lập mô hình và xác minh
Bước đầu tiên là phát triển một mô hình của giao thức cho phép chúng tôi thể hiện tất cả các thuộc tính chính mà chúng tôi muốn chính thức nêu và chứng minh. Mô hình này được xây dựng dựa trên công việc trước đây của chúng tôi nhằm xác thực tính an toàn và tính sống động của Casper FFG (mô hình trước đó đã xác định phiên bản đầu tiên của cơ chế cuối cùng của Gasper).
Mô hình này có ba mô-đun cấu trúc chính:
\sum là toán tử tính tổng; cổ phần.[st_fun v] đưa ra số tiền cổ phần tương ứng với trình xác thực v (st_fun giả định rằng mọi người xác thực đều phải có cổ phần trong hệ thống).
Ngoài ra, vì chúng tôi muốn mô phỏng một tập hợp các trình xác thực động, nghĩa là, tập hợp các trình xác thực đang hoạt động có thể thay đổi từ khối này sang khối khác, chúng tôi khai báo một ánh xạ trừu tượng (có giới hạn) vset: {fmap Hash -> {set Trình xác thực}}, Đưa ra tập hợp các trình xác thực đang hoạt động tại một khối. Bây giờ, bằng cách sử dụng vset và wt , chúng ta có thể định nghĩa tập hợp đa số là gì:
Tại một khối nhất định, nếu trọng số của một tập hợp con của tập hợp các trình xác thực đang hoạt động vượt quá 2/3 trọng số của toàn bộ tập hợp, thì tập hợp con đó là tập hợp đa số tuyệt đối.
cây khối. Chúng tôi sử dụng loại băm khối hữu hạn để mô phỏng Hash khối:finType và sử dụng genesis để biểu thị khối genesis. Chúng tôi sử dụng ký hiệu h1 < ~ h2 để biểu thị mối quan hệ cha-con của khối (h1 là cha của h2) để mô phỏng cây khối điểm kiểm tra.
Tiếp theo, chúng ta sử dụng h1 <~* h2 để xác định mối quan hệ tổ tiên, h1 là tổ tiên của h2 và h2 là hậu duệ của h1 (h1 và h2 có thể là cùng một khối). Đối với các thuộc tính của mối quan hệ tổ tiên, ví dụ, tổ tiên của tổ tiên cũng là tổ tiên, tương tự như các thuộc tính của mối quan hệ cha con.
chữ
tiêu đề phụ
Dựa trên các định nghĩa này và các thuộc tính tương ứng của chúng, chúng tôi xác định tất cả các cấu trúc và thuộc tính khác trong mô hình, bao gồm các điều kiện phạt, thuộc tính giao điểm đại biểu, và hợp lý hóa và hoàn thiện. Ví dụ: thuộc tính tịch thu một cộng đồng trong trường hợp vi phạm giao thức có thể được xác định bằng cách sử dụng các ràng buộc thành viên trừu tượng sau:
Đề xuất này tuyên bố rằng việc cắt giảm một nhóm có nghĩa là có hai nhóm siêu đa số vL và vR tại một số khối bL và bR, và giao điểm của hai nhóm này là trình xác thực bị cắt giảm (bắt đầu bỏ phiếu kép hoặc bỏ phiếu xung quanh) Tập hợp đầy đủ của . Lưu ý rằng trong điều kiện đặc biệt là tập hợp các trình xác thực đang hoạt động luôn cố định, trọng số của giao điểm của các tập hợp đa số này ít nhất là 1/3 tổng số tiền gửi.
Một ví dụ khác là định nghĩa về một fork hoàn thiện (nghĩa là vi phạm bảo mật):
Mệnh đề này phát biểu rằng hai khối mâu thuẫn b1 và b2 đều được hoàn thiện (vì cả b1 và b2 đều không phải là khối tổ tiên của khối kia). Hai khối này có thể được hoàn thiện bằng một chuỗi dài tùy ý ở bất kỳ độ cao hợp lý hóa nào.
Các định nghĩa và tập hợp kết quả này được sử dụng để chỉ ra và chứng minh ba định lý về bảo mật trách nhiệm giải trình, hoạt động hợp lý và giới hạn dưới có thể cắt giảm. Để rõ ràng, chúng tôi cũng xác định lại công thức của định lý bảo mật trách nhiệm giải trình như sau:
Định nghĩa rất đơn giản và chỉ nói rằng: nếu tính bảo mật bị phá vỡ (với bất kỳ đợt phân tách đã hoàn thiện nào), điều đó có nghĩa là một số bộ trình xác thực đã bị cắt giảm. Bằng chứng này cơ giới hóa lập luận không chính thức do Gasper đưa ra và cho thấy lý do tại sao các nhánh được hoàn thiện có nghĩa là phải có hai nhóm siêu đa số vi phạm một trong các điều kiện cắt giảm, vì vậy giao điểm của chúng có thể bị cắt giảm.
chữ
Báo cáo kỹ thuật của chúng tôi mô tả quy trình chính thức hóa và bằng chứng về các thuộc tính này, trong khi kho lưu trữ mã dự án của chúng tôi cung cấp thông số kỹ thuật đầy đủ.
tiêu đề cấp đầu tiên
tiếp tục đi
