บทนำ: การตรวจสอบอย่างเป็นทางการของกลไกฉันทามติของ Gasper
หมายเหตุบรรณาธิการ: บทความนี้มาจากผู้ที่ชื่นชอบ Ethereum (ID: ethfans)หมายเหตุบรรณาธิการ: บทความนี้มาจาก
ผู้ที่ชื่นชอบ Ethereum (ID: ethfans)
ผู้ที่ชื่นชอบ Ethereum (ID: ethfans)
Gasper เป็นเลเยอร์โปรโตคอล Proof-of-stake แบบนามธรรมที่นำมาใช้โดยโปรโตคอล Beacon Chain (โปรโตคอลพื้นฐานของเครือข่าย Ethereum 2.0 ที่กำลังจะมาถึง) ส่วนสำคัญของ Gasper คือชุดของกลไกขั้นสุดท้าย ซึ่งใช้เพื่อให้มั่นใจถึงความทนทานของธุรกรรมและการทำงานอย่างต่อเนื่องของระบบจะไม่ได้รับความเสียหายจากการโจมตี
Gasper
เรายินดีที่จะประกาศความสำเร็จอีกขั้นในการทำงานร่วมกันระยะยาวระหว่าง Runtime Verification และ Ethereum Foundation: เราได้พัฒนากรอบอย่างเป็นทางการเพื่อจำลองและตรวจสอบโปรโตคอล beacon chain และประสบความสำเร็จในการพิสูจน์ความถูกต้องขั้นสุดท้ายของ Gasper อย่างเป็นทางการ และเรายังใช้ผลลัพธ์เหล่านี้ เพื่อแสดงให้เห็นว่าการนำสิ่งที่เป็นนามธรรมของ Gasper ไปใช้กับบีคอนเชนก็มีคุณสมบัติเหล่านี้เช่นกัน สามารถดูทั้งแบบจำลองและสคริปต์การพิสูจน์ได้ที่นี่
ชื่อระดับแรก
โปรโตคอล beacon chain เป็นโปรโตคอลการพิสูจน์การเดิมพันชุดใหม่ ซึ่งเป็นแกนหลักของการอัปเกรดครั้งใหญ่ในอนาคตของ Ethereum "Ethereum 2.0" ในโปรโตคอล beacon chain โหนดที่เข้าร่วม (หรือ "ตัวตรวจสอบ") ล้วนมีเงินฝาก (เดิมพันในรูปของ ETH) ในระบบ ตัวตรวจสอบยืนยันความถูกต้องของบล็อกและลงคะแนนให้กับคุณลักษณะต่างๆ โดยการส่ง "การยืนยัน" ไปยังเครือข่าย โปรโตคอล beacon chain นั้นมีเครื่องมือหลายอย่างที่จะช่วยให้ผู้ตรวจสอบได้รับความเห็นพ้องต้องกันเกี่ยวกับสถานะล่าสุดของ blockchain
Gasper เสนอคำอธิบายที่เป็นนามธรรมแต่แม่นยำเกี่ยวกับเครื่องมือขั้นสุดท้ายในโปรโตคอล beacon chain และยังกำหนดกฎการเลือกทางแยก เครื่องมือขั้นสุดท้ายใช้เพื่อกำหนดว่าบล็อกใดควรได้รับการพิจารณาโดยผู้เข้าร่วม กฎการเลือกทางแยกใช้เพื่อกำหนดว่าทางแยกใด โซ่หลักเมื่อโซ่ส้อม Finality ใน Gasper สรุปแนวคิดที่เกิดขึ้นในกระดาษ "Casper Friendly Finality Gadget (Casper FFG)" ทำให้ "finalization" เป็นรูปแบบทั่วไปมากขึ้น
ชื่อเรื่องรอง
การให้เหตุผลและการสรุปผล
แนวคิดเรื่องความเป็นที่สุดเกี่ยวข้องเฉพาะกับ "บล็อกด่าน" (เรียกอีกอย่างว่า "บล็อกขอบเขตยุค" ซึ่งเป็นบล็อกที่จุดเริ่มต้นของยุค) ข้อความรับรองส่วนหนึ่งเรียกว่า "การลงคะแนน rationalization" ในการลงคะแนนเสียง rationalization ผู้ตรวจสอบจะเชื่อมโยงบล็อกจุดตรวจต้นทางกับบล็อกจุดตรวจเป้าหมายในภายหลัง โดยแสดงให้เห็นด้วยสายตาว่า Validator ที่เริ่มต้นการยืนยันเชื่อว่า "เราสามารถย้ายจากสถานะของ ด่านต้นทางสู่สภาพด่านปลายทาง”. ผลที่ได้คือ การลงคะแนนเพื่อเหตุผลจะแสดง: (1) ผู้ตรวจสอบความถูกต้องที่เริ่มต้นการลงคะแนน (2) จุดตรวจต้นทางและความสูงของเหตุผล (3) จุดตรวจสอบเป้าหมายและความสูงของเหตุผล
หากตรงตามเงื่อนไข: (1) จุดตรวจสอบต้นทาง B0 ได้รับการหาเหตุผลเข้าข้างตนเอง (2) เสียงส่วนใหญ่ (เช่น อย่างน้อย 2/3 ของผู้ตรวจสอบความถูกต้อง) ลงคะแนนให้คู่แหล่งที่มาและเป้าหมาย B0-B1 ด้วย จากนั้น จุดตรวจสอบเป้าหมาย B1 มันถูกหาเหตุผลเข้าข้างตนเองผ่านจุดตรวจต้นทาง B0
B0 บรรลุผลสำเร็จของคำสั่ง K (k > 0) และจุดตรวจสอบทั้งหมดระหว่าง B0 และ Bk จะได้รับการสรุปก็ต่อเมื่อผู้ตรวจสอบความถูกต้องส่วนใหญ่เชื่อมโยง B0 กับจุดตรวจสอบลูกหลานรุ่น K Bk โปรดทราบว่าการกำเนิดบล็อกนั้นถือเป็นทั้งการหาเหตุผลเข้าข้างตนเองและขั้นสุดท้าย แผนภาพด้านล่างแสดงแนวคิดการหาเหตุผลเข้าข้างตนเองและการสรุปผลใน Gasper
หากผู้ตรวจสอบความถูกต้องพยายามเบี่ยงเบนไปจากโปรโตคอลและส่งคะแนนเสียงที่ขัดแย้ง ผู้ตรวจสอบความถูกต้องจะถูกลงโทษ: เงินมัดจำส่วนใหญ่จะถูกหักออก Gasper กำหนดสองเงื่อนไข (หรือที่เรียกว่าเงื่อนไขการเฉือน) เพื่อกำหนดสิ่งที่ถือเป็นการลงคะแนนที่ขัดแย้งกัน:
การลงคะแนนเสียงรอบทิศทาง: จุดตรวจสอบสองจุดที่เกี่ยวข้องกับการลงคะแนนที่ออกโดยผู้ตรวจสอบความถูกต้องนั้นอยู่ภายในช่วงความสูงของจุดตรวจสอบสองจุดของการลงคะแนนอื่นที่ออกโดยผู้ตรวจสอบความถูกต้อง
ข้อความ
ผู้ตรวจสอบความถูกต้องที่เริ่มต้นการลงคะแนนเสียงสองครั้งจะถือว่าละเมิดเงื่อนไขเครื่องหมายทับแรก ผู้ตรวจสอบความถูกต้องที่เริ่มต้นการลงคะแนนแบบตัดคำจะละเมิดเงื่อนไขเครื่องหมายทับที่สอง ไม่ว่าในกรณีใด ผู้ตรวจสอบความถูกต้องที่ละเมิดกฎจะถูกหักเงินมัดจำเป็นจำนวนมาก
ชื่อเรื่องรอง
ความถูกต้อง (คุณสมบัติความถูกต้อง)
เช่นเดียวกับโปรโตคอล Byzantine Fault Tolerance (BFT) อื่นๆ ข้อสันนิษฐานที่สำคัญของโปรโตคอล Gasper คือผู้ตรวจสอบส่วนใหญ่ (มากกว่า 2/3 ซึ่งกำหนดโดยจำนวนเงินฝาก) มีความซื่อสัตย์และจะปฏิบัติตามข้อกำหนดของโปรโตคอล ภายใต้สมมติฐานนี้ Gasper มีคุณสมบัติพื้นฐานสองประการ:
ความปลอดภัยที่รับผิดชอบได้: จะไม่มีการสรุปบล็อกสองบล็อกที่เป็นของส้อมที่แตกต่างกันเว้นแต่จะมีการตัดเฉือนอย่างน้อย 1/3 ของผู้ตรวจสอบความถูกต้อง (ในแง่ของจำนวนเงินฝาก)
ความมีชีวิตชีวาที่สมเหตุสมผล: ไม่ว่าจะเกิดอะไรขึ้นกับบล็อกเชนในอดีต กระบวนการสุดท้ายของบล็อกจะไม่มีทางหยุดชะงัก
นอกจากนี้ ในสภาพแวดล้อมที่ชุดของ Validator เปลี่ยนแปลงแบบไดนามิก (เมื่อ Validator ออกจากเครือข่ายและ Validator ใหม่เข้าร่วม ชุดของ Validator ที่ใช้งานอยู่อาจเปลี่ยนแปลง) คุณสมบัติที่สามจะวัดปริมาณเมื่อมีคนละเมิดกฎของโปรโตคอล ที่สามารถยึดได้:
Slashable bound: ตราบเท่าที่สามารถใช้เงื่อนไขโปรโตคอลพิเศษเพื่อควบคุมเงื่อนไขการเปิดใช้งานและออกจากตัวตรวจสอบความถูกต้อง จะสามารถพิสูจน์ได้ว่า (เมื่อทำลายการรักษาความปลอดภัย) มีขอบเขตที่ต่ำกว่าในจำนวนเงินฝากที่สามารถเฉือนได้
ชุดเครื่องมือตรวจสอบแบบไดนามิก (ซึ่งเป็นสิ่งที่โปรโตคอล Beacon Chain ใช้) นำเสนอปัญหาที่ท้าทายอีกประการหนึ่ง: ระบบไม่สามารถลงโทษตัวตรวจสอบความถูกต้องที่เป็นอันตรายได้อย่างน่าเชื่อถืออีกต่อไป เนื่องจากอาจทำได้หลังจากทำสิ่งที่ไม่ดี แต่ก่อนที่จะฝากเงิน ถูกตัดจริง ออกจากเครือข่าย คุณสมบัติขีดจำกัดล่างแบบสแลชได้ทำให้สามารถปรับช่วงตัวแปรของชุดเครื่องมือตรวจสอบที่ใช้งานอยู่และรักษาระดับความรับผิดชอบขั้นต่ำไว้ได้
ตรวจสอบความสมบูรณ์ของ Gasper
Gasper มีจุดมุ่งหมายเพื่อให้คำอธิบายทางคณิตศาสตร์ที่แม่นยำเกี่ยวกับขั้นสุดท้ายที่สามารถใช้ในการพิสูจน์ความถูกต้องอย่างเป็นทางการ ความถูกต้องนี้ยังเป็นกุญแจสำคัญในการพิสูจน์ความปลอดภัยของโปรโตคอล beacon chain แพลตฟอร์ม Ethereum กำลังถูกใช้เป็นราคาหุ้นสำหรับระบบการซื้อขายทางการเงินขนาดใหญ่มากขึ้นเรื่อยๆ โดยเน้นถึงความสำคัญที่ไม่เคยเกิดขึ้นมาก่อนของการรับประกันความปลอดภัย
ด้วยความร่วมมือกับ Ethereum Foundation เราได้ทำให้กลไกขั้นสุดท้ายของ Gasper เป็นทางการภายใต้เงื่อนไขทั่วไปของชุดเครื่องมือตรวจสอบแบบไดนามิกโดยใช้ตัวช่วยพิสูจน์ Coq เราชี้ให้เห็นและพิสูจน์คุณสมบัติหลักทั้งสามของ Gasper ภายใต้เงื่อนไขนี้: ความปลอดภัยที่รับผิดชอบ ความน่าอยู่ และขอบเขตล่างที่เฉือนได้ การพิสูจน์ทั้งหมดใช้โมเดล Coq เดียวกัน
ที่นี่เราให้รายละเอียดสั้น ๆ เกี่ยวกับความสำเร็จนี้เท่านั้น สามารถดูรายละเอียดทั้งหมดได้ที่:
รายงานทางเทคนิคเกี่ยวกับโครงการ
ที่เก็บ Github ของโครงการ
ชื่อเรื่องรอง
วิธีการสร้างแบบจำลองและการตรวจสอบ
ขั้นตอนแรกคือการพัฒนารูปแบบของโปรโตคอลที่ช่วยให้เราสามารถแสดงคุณสมบัติหลักทั้งหมดที่เราต้องการระบุและพิสูจน์อย่างเป็นทางการ โมเดลนี้สร้างขึ้นจากงานก่อนหน้าของเราในการตรวจสอบความปลอดภัยและอายุการใช้งานของ Casper FFG (โมเดลก่อนหน้านี้ได้กำหนดเวอร์ชันก่อนหน้าของกลไกขั้นสุดท้าย Gasper)
รุ่นนี้มีสามโมดูลโครงสร้างหลัก:
\sum คือตัวดำเนินการผลรวม stake.[st_fun v] ให้จำนวนเงินเดิมพันที่สอดคล้องกับตัวตรวจสอบความถูกต้อง v (st_fun ถือว่าตัวตรวจสอบความถูกต้องทุกตัวจะต้องมีส่วนได้เสียในระบบ)
นอกจากนี้ เนื่องจากเราต้องการจำลองชุดของเครื่องมือตรวจสอบความถูกต้องแบบไดนามิก นั่นคือชุดของเครื่องมือตรวจสอบความถูกต้องที่ใช้งานอยู่อาจเปลี่ยนจากบล็อกหนึ่งไปอีกบล็อกหนึ่ง เราจึงประกาศการจับคู่นามธรรม (จำกัด) vsset: {fmap Hash -> {set Validator}} กำหนดชุดตัวตรวจสอบความถูกต้องที่ใช้งานอยู่ที่บล็อก ตอนนี้ เมื่อใช้ vset และ wt เราสามารถกำหนดได้ว่าชุดข้อมูลสำคัญยิ่งคืออะไร:
ที่บล็อกใดบล็อกหนึ่ง ถ้าน้ำหนักของเซตย่อยของเซตของ Active Validator เกิน 2/3 ของน้ำหนักของเซตทั้งหมด เซตย่อยนั้นจะเป็นเซตเสียงข้างมาก
ต้นไม้บล็อก เราใช้บล็อกแฮชประเภทจำกัดเพื่อจำลองบล็อกแฮช:finType และใช้การกำเนิดเพื่อแสดงถึงบล็อกการกำเนิด เราใช้สัญกรณ์ h1 <~ h2 เพื่อแสดงความสัมพันธ์ของบล็อกแม่และลูก (h1 เป็นพาเรนต์ของ h2) เพื่อจำลองแผนผังบล็อกจุดตรวจสอบ
ต่อไป เราใช้ h1 <~* h2 เพื่อกำหนดความสัมพันธ์ของบรรพบุรุษ h1 เป็นบรรพบุรุษของ h2 และ h2 เป็นลูกหลานของ h1 (h1 และ h2 สามารถเป็นบล็อกเดียวกันได้) สำหรับคุณลักษณะของความสัมพันธ์ระหว่างบรรพบุรุษ เช่น บรรพบุรุษของบรรพบุรุษก็เป็นบรรพบุรุษเช่นกัน ซึ่งคล้ายกับคุณลักษณะของความสัมพันธ์ระหว่างบิดากับบุตร
ข้อความ
ชื่อเรื่องรอง
ตามคำจำกัดความเหล่านี้และคุณสมบัติที่สอดคล้องกัน เรากำหนดโครงสร้างและคุณสมบัติอื่นๆ ทั้งหมดในแบบจำลอง รวมถึงเงื่อนไขการลงโทษ คุณสมบัติการตัดกันขององค์ประชุม และการหาเหตุผลเข้าข้างตนเองและการสรุปผล ตัวอย่างเช่น คุณสมบัติของการยึดชุมชนในกรณีที่มีการละเมิดโปรโตคอลสามารถกำหนดได้โดยใช้ข้อจำกัดความเป็นสมาชิกที่เป็นนามธรรมต่อไปนี้:
ข้อเสนอนี้ระบุว่าการเฉือนกลุ่มหมายความว่ามีกลุ่มที่มีอำนาจเหนือกว่าสองกลุ่ม vL และ vR ในบางช่วงตึก bL และ bR และจุดตัดของทั้งสองกลุ่มนี้คือตัวตรวจสอบความถูกต้องแบบเฉือน (เริ่มต้นการลงคะแนนเสียงสองครั้งหรือการลงคะแนนเสียงรอบทิศทาง) โปรดทราบว่าภายใต้เงื่อนไขพิเศษที่ชุดของเครื่องมือตรวจสอบความถูกต้องที่ใช้งานอยู่นั้นคงที่เสมอ น้ำหนักของการตัดกันของชุดของผลสำคัญยิ่งยวดเหล่านี้คืออย่างน้อย 1/3 ของเงินฝากทั้งหมด
อีกตัวอย่างหนึ่งคือคำจำกัดความของfinalizing fork (เช่น การละเมิดความปลอดภัย):
ข้อเสนอนี้ระบุว่าบล็อก b1 และ b2 ที่ขัดแย้งกันสองบล็อกได้รับการสรุปผล (เพราะทั้ง b1 และ b2 ไม่ใช่บล็อกบรรพบุรุษของอีกบล็อกหนึ่ง) บล็อกทั้งสองนี้สามารถสรุปได้ด้วยห่วงโซ่ยาวโดยพลการที่ความสูงของการหาเหตุผลเข้าข้างตนเองใด ๆ
คำจำกัดความและชุดของผลลัพธ์เหล่านี้ใช้เพื่อชี้ให้เห็นและพิสูจน์ทฤษฎีบทสามประการของความปลอดภัย ความรับผิดชอบ กิจกรรมที่น่าจะเป็น และขอบเขตล่างแบบสแลชได้ เพื่อความชัดเจน เราได้นิยามการกำหนดทฤษฎีบทความปลอดภัยความรับผิดชอบใหม่ดังนี้:
คำจำกัดความนั้นเรียบง่ายและบอกเพียงว่า: หากการรักษาความปลอดภัยเสียหาย (ด้วยการแยกขั้นสุดท้ายใดๆ) จะต้องหมายความว่าชุดเครื่องมือตรวจสอบความถูกต้องบางชุดถูกเฉือน การพิสูจน์นี้ใช้กลข้อโต้แย้งอย่างไม่เป็นทางการที่ Gasper มอบให้ และแสดงให้เห็นว่าเหตุใดการสรุปผลทางแยกจึงหมายความว่าต้องมีกลุ่มเสียงข้างมากสองกลุ่มที่ละเมิดเงื่อนไขการเฉือนข้อใดข้อหนึ่ง ดังนั้นการตัดกันจึงถูกเฉือนได้
ข้อความ
รายงานทางเทคนิคของเราอธิบายกระบวนการทำให้เป็นทางการและการพิสูจน์คุณสมบัติเหล่านี้ ในขณะที่ที่เก็บรหัสโครงการของเราให้ข้อมูลจำเพาะแบบเต็ม
ชื่อระดับแรก
ทำต่อไป
