ในบทความก่อนหน้านี้เราได้กล่าวถึงการตรวจสอบอย่างเป็นทางการขั้นสูงของระบบ Zero-Knowledge Proof (ZKP): วิธีตรวจสอบคําสั่ง ZK ด้วยการตรวจสอบคําสั่ง zkWasm แต่ละรายการอย่างเป็นทางการ เราจึงสามารถรับประกันความปลอดภัยทางเทคนิคและความถูกต้องของวงจร zkWasm ทั้งหมดได้อย่างเต็มที่ ในบทความนี้เราจะมุ่งเน้นไปที่มุมมองของการค้นพบช่องโหว่การวิเคราะห์ช่องโหว่เฉพาะที่ระบุในระหว่างกระบวนการตรวจสอบและตรวจสอบและบทเรียนที่ได้เรียนรู้จากช่องโหว่เหล่านี้ สําหรับการอภิปรายทั่วไปเกี่ยวกับการตรวจสอบอย่างเป็นทางการขั้นสูงของบล็อกเชน ZKP โปรดดูบทความเกี่ยวกับการตรวจสอบอย่างเป็นทางการขั้นสูงของบล็อกเชน ZKP

ก่อนที่จะพูดถึงช่องโหว่ของ ZK เรามาทําความเข้าใจกันก่อนว่า CertiK ดําเนินการตรวจสอบอย่างเป็นทางการของ ZK อย่างไร สําหรับระบบที่ซับซ้อนเช่น ZK Virtual Machine (zkVM) ขั้นตอนแรกในการตรวจสอบอย่างเป็นทางการ (FV) คือการกําหนดสิ่งที่ต้องตรวจสอบและคุณสมบัติอย่างชัดเจน สิ่งนี้ต้องการการตรวจสอบอย่างครอบคลุมเกี่ยวกับการออกแบบ การใช้โค้ด และการตั้งค่าการทดสอบของระบบ ZK กระบวนการนี้ทับซ้อนกับการตรวจสอบปกติ แต่แตกต่างกันตรงที่หลังจากการตรวจสอบจะต้องกําหนดเป้าหมายการตรวจสอบและคุณสมบัติ ที่ CertiK เราเรียกสิ่งนี้ว่าการตรวจสอบที่มุ่งเน้นการตรวจสอบ งานตรวจสอบและการตรวจสอบมักจะถูกรวมเข้าด้วยกัน สําหรับ zkWasm เราได้ดําเนินการทั้งการตรวจสอบและการตรวจสอบอย่างเป็นทางการพร้อมกัน

ช่องโหว่ของ ZK คืออะไร?

คุณสมบัติหลักของระบบ Zero-Knowledge Proof (ZKP) คืออนุญาตให้ถ่ายโอนหลักฐานการคํานวณที่เข้ารหัสสั้น ๆ ที่ดําเนินการแบบออฟไลน์หรือส่วนตัว (เช่น ธุรกรรมบล็อกเชน) ไปยังผู้ตรวจสอบ ZKP ผู้ตรวจสอบจะตรวจสอบและยืนยันหลักฐานเพื่อให้แน่ใจว่าการคํานวณเกิดขึ้นตามที่กล่าวอ้าง ในบริบทนี้ช่องโหว่ของ ZK จะช่วยให้แฮ็กเกอร์สามารถส่งหลักฐาน ZK ปลอมสําหรับธุรกรรมเท็จและให้ผู้ตรวจสอบ ZKP ยอมรับ

สําหรับโปรแกรมพิสูจน์ zkVM กระบวนการพิสูจน์ ZK เกี่ยวข้องกับการเรียกใช้โปรแกรมสร้างบันทึกการดําเนินการสําหรับแต่ละขั้นตอนและแปลงบันทึกการดําเนินการเหล่านี้เป็นชุดของตารางตัวเลข (กระบวนการที่เรียกว่า "เลขคณิต") ตัวเลขเหล่านี้ต้องเป็นไปตามชุดของข้อจํากัด ("วงจร") ซึ่งรวมถึงความสัมพันธ์ระหว่างเซลล์ตารางเฉพาะ ค่าคงที่คงที่ ข้อจํากัดในการค้นหาฐานข้อมูลระหว่างตาราง และสมการพหุนาม (หรือ "เกต") ที่แถวตารางที่อยู่ติดกันแต่ละคู่ต้องเป็นไปตาม การตรวจสอบแบบ On-chain สามารถยืนยันการมีอยู่ของตารางที่ตรงตามข้อจํากัดทั้งหมดโดยไม่เปิดเผยตัวเลขเฉพาะภายในตาราง

ตารางเลขคณิตใน zkWasm

ความแม่นยําของแต่ละข้อจํากัดเป็นสิ่งสําคัญ ข้อผิดพลาดใด ๆ ในข้อ จํากัด ไม่ว่าจะอ่อนแอเกินไปหรือขาดหายไปอาจทําให้แฮ็กเกอร์ส่งหลักฐานที่ทําให้เข้าใจผิดได้ ตารางเหล่านี้อาจดูเหมือนแสดงถึงการดําเนินการที่ถูกต้องของสัญญาอัจฉริยะ แต่ในความเป็นจริงไม่ใช่ เมื่อเทียบกับ VM แบบเดิมความทึบของธุรกรรม zkVM จะขยายช่องโหว่เหล่านี้ ในเชนที่ไม่ใช่ ZK รายละเอียดของการคํานวณธุรกรรมจะถูกบันทึกต่อสาธารณะบนบล็อกเชน อย่างไรก็ตาม zkVM ไม่ได้จัดเก็บรายละเอียดเหล่านี้บนเครือข่าย การขาดความโปร่งใสนี้ทําให้ยากต่อการระบุลักษณะเฉพาะของการโจมตีหรือแม้ว่าจะมีการโจมตีเกิดขึ้น

วงจร ZK ที่บังคับใช้กฎการดําเนินการของคําสั่ง zkVM นั้นซับซ้อนมาก สําหรับ zkWasm การใช้งานวงจร ZK เกี่ยวข้องกับรหัส Rust มากกว่า 6,000 บรรทัดและข้อจํากัดหลายร้อยข้อ ความซับซ้อนนี้มักหมายความว่าอาจมีช่องโหว่หลายอย่างที่รอการค้นพบ

สถาปัตยกรรมวงจร zkWasm

อันที่จริงจากการตรวจสอบและการตรวจสอบอย่างเป็นทางการของ zkWasm เราได้ค้นพบช่องโหว่ดังกล่าวหลายประการ ด้านล่างนี้เราจะพูดถึงตัวอย่างตัวแทนสองตัวอย่างและตรวจสอบความแตกต่างระหว่างพวกเขา

ช่องโหว่ของรหัส: Load8 Data Injection Attack

ช่องโหว่แรกเกี่ยวข้องกับคําสั่ง Load8 ใน zkWasm ใน zkWasm การอ่านหน่วยความจําฮีปทําได้โดยใช้ชุดคําสั่ง LoadN โดยที่ N คือขนาดของข้อมูลที่จะโหลด ตัวอย่างเช่น Load64 ควรอ่านข้อมูล 64 บิตจากที่อยู่หน่วยความจํา zkWasm Load8 ควรอ่านข้อมูล 8 บิต (เช่น หนึ่งไบต์) จากหน่วยความจําและใส่เลขศูนย์เพื่อสร้างค่า 64 บิต ภายใน zkWasm แสดงถึงหน่วยความจําเป็นอาร์เรย์ของไบต์ 64 บิต ดังนั้นจึงจําเป็นต้อง "เลือก" ส่วนหนึ่งของอาร์เรย์หน่วยความจํา ทําได้โดยใช้ตัวแปรกลาง (u16_cells) สี่ตัว ซึ่งรวมกันเป็นค่าโหลด 64 บิตที่สมบูรณ์

ข้อจํากัดสําหรับคําสั่ง LoadN เหล่านี้กําหนดไว้ดังนี้:

ข้อจํากัดนี้แบ่งออกเป็นสามกรณี: Load32, Load16 และ Load8 Load64 ไม่มีข้อ จํากัด เนื่องจากหน่วยหน่วยความจําเป็น 64 บิตพอดี สําหรับเคส Load32 รหัสช่วยให้แน่ใจว่าสูง 4 ไบต์ (32 บิต) ในหน่วยหน่วยความจําต้องเป็นศูนย์

สําหรับกรณี Load16 รหัสช่วยให้มั่นใจได้ว่าสูง 6 ไบต์ (48 บิต) ในหน่วยหน่วยความจําจะต้องเป็นศูนย์

สําหรับกรณี Load8 ควรกําหนดให้สูง 7 ไบต์ (56 บิต) ในหน่วยหน่วยความจําเป็นศูนย์ น่าเสียดายที่นี่ไม่ใช่กรณีในรหัส

อย่างที่คุณเห็นมีเพียง 9 ถึง 16 บิตสูงเท่านั้นที่ถูก จํากัด ไว้ที่ศูนย์ อีก 48 บิตสูงสามารถเป็นค่าใดก็ได้และยังคงส่งผ่านเป็น "อ่านจากหน่วยความจํา"

การใช้ประโยชน์จากช่องโหว่นี้แฮ็กเกอร์อาจแทรกแซงการพิสูจน์ ZK ของลําดับการดําเนินการที่ถูกต้องทําให้คําสั่ง Load8 โหลดไบต์ที่ไม่คาดคิดเหล่านี้ส่งผลให้ข้อมูลเสียหาย นอกจากนี้ ด้วยการจัดเรียงโค้ดและข้อมูลโดยรอบอย่างระมัดระวัง อาจทําให้เกิดการดําเนินการและการถ่ายโอนที่ผิดพลาด ซึ่งนําไปสู่การโจรกรรมข้อมูลและทรัพย์สิน ธุรกรรมปลอมแปลงเหล่านี้สามารถผ่านการตรวจสอบของตัวตรวจสอบ zkWasm และได้รับการยอมรับอย่างไม่ถูกต้องว่าเป็นธุรกรรมที่ถูกต้องตามกฎหมายโดยบล็อกเชน

การแก้ไขช่องโหว่นี้ค่อนข้างง่าย

ช่องโหว่นี้แสดงถึงประเภทของช่องโหว่ ZK ที่เรียกว่า "ช่องโหว่ของโค้ด" เนื่องจากมีต้นกําเนิดมาจากการใช้งานโค้ด และสามารถแก้ไขได้อย่างง่ายดายผ่านการแก้ไขโค้ดในเครื่องเล็กน้อย อย่างที่คุณอาจเห็นด้วยช่องโหว่เหล่านี้ยังค่อนข้างง่ายสําหรับผู้คนในการระบุ

ช่องโหว่ในการออกแบบ: Forged Return Attack

ลองมาดูช่องโหว่อื่นคราวนี้เกี่ยวกับการเรียกและการกลับมาของ zkWasm การเรียกใช้และการส่งคืนเป็นคําสั่ง VM พื้นฐานที่อนุญาตให้บริบทที่ทํางานอยู่ (เช่น ฟังก์ชัน) สามารถเรียกใช้อีกบริบทหนึ่งและดําเนินการบริบทการโทรต่อได้หลังจากที่ผู้รับสายดําเนินการเสร็จสิ้น การเรียกแต่ละครั้งคาดว่าจะกลับมาในภายหลัง ข้อมูลแบบไดนามิกที่ติดตามโดย zkWasm ในระหว่างวงจรชีวิตของการเรียกใช้และการส่งคืนเรียกว่า "กรอบการโทร" เนื่องจาก zkWasm ดําเนินการคําสั่งตามลําดับเฟรมการโทรทั้งหมดจึงสามารถสั่งซื้อได้ตามการเกิดขึ้นระหว่างรันไทม์ ด้านล่างนี้คือตัวอย่างของรหัสการเรียก/ส่งคืนที่ทํางานบน zkWasm

ผู้ใช้สามารถเรียกใช้ฟังก์ชัน buy_token() เพื่อซื้อโทเค็น (อาจโดยการชําระเงินหรือโอนสิ่งของมีค่าอื่นๆ) หนึ่งในขั้นตอนหลักคือการเพิ่มยอดเงินในบัญชีโทเค็น 1 โดยเรียกฟังก์ชัน add_token() เนื่องจาก ZK prover เองไม่รองรับโครงสร้างข้อมูลเฟรมการโทร จึงจําเป็นต้องใช้ตารางการดําเนินการ (E-Table) และ Jump Table (J-Table) เพื่อบันทึกและติดตามประวัติทั้งหมดของเฟรมการโทรเหล่านี้

รูปด้านบนแสดงกระบวนการเรียก buy_token() add_token() และกลับจาก add_token() เป็น buy_token() จะเห็นได้ว่ายอดเงินในบัญชีโทเค็นเพิ่มขึ้น 1 ในตารางการดําเนินการ แต่ละขั้นตอนการดําเนินการจะใช้หนึ่งแถว รวมถึงหมายเลขเฟรมการโทรปัจจุบันที่กําลังดําเนินการ ชื่อฟังก์ชันบริบทปัจจุบัน (เพื่อจุดประสงค์ในการอธิบายเท่านั้น) ในตารางกระโดดแต่ละเฟรมการโทรจะใช้พื้นที่หนึ่งแถวจัดเก็บหมายเลขของเฟรมผู้โทรชื่อบริบทของฟังก์ชันผู้โทร (เพื่อจุดประสงค์ในการอธิบายเท่านั้น) และตําแหน่งคําสั่งถัดไปของเฟรมผู้โทร (เพื่อให้เฟรมสามารถกลับมาได้) ในทั้งสองตาราง มีคอลัมน์ "jops" ที่ติดตามว่าคําสั่งปัจจุบันเป็นการโทร/ส่งคืนหรือไม่ (ในตารางการดําเนินการ) และจํานวนคําสั่งการโทร/ส่งคืนทั้งหมดสําหรับเฟรมนั้น (ในตารางกระโดด)

การโทรแต่ละครั้งควรมีการส่งคืนที่สอดคล้องกัน และแต่ละเฟรมควรมีการโทรเพียงครั้งเดียวและส่งคืนหนึ่งครั้ง ดังแสดงในรูปด้านบน ค่า "jops" สําหรับเฟรมแรกใน Jump Table คือ 2 ซึ่งสอดคล้องกับแถวแรกและแถวที่สามในตารางการดําเนินการ โดยที่ค่า "jops" คือ 1 ทุกอย่างดูปกติในขณะนี้

อย่างไรก็ตาม มีปัญหาที่นี่: ในขณะที่การโทรหนึ่งครั้งและการส่งคืนหนึ่งครั้งจะเพิ่มจํานวน "jops" สําหรับเฟรมเป็น 2 การโทรสองครั้งหรือสองคืนจะส่งผลให้นับ 2 ด้วย การมีการโทรสองครั้งหรือส่งคืนสองครั้งต่อเฟรมอาจดูไร้สาระ แต่สิ่งสําคัญคือต้องจําไว้ว่านี่คือสิ่งที่แฮ็กเกอร์พยายามทําโดยทําลายความคาดหวัง

ตอนนี้คุณอาจรู้สึกตื่นเต้น แต่เราพบปัญหาจริงหรือ?

ปรากฎว่าการโทรสองครั้งไม่ใช่ปัญหาเนื่องจากข้อจํากัดของตารางการดําเนินการและตารางกระโดดป้องกันไม่ให้สายสองสายถูกเข้ารหัสในแถวเดียวกันของเฟรม เนื่องจากการโทรแต่ละครั้งจะสร้างหมายเลขเฟรมใหม่ เช่น หมายเลขเฟรมการโทรปัจจุบันบวก 1

อย่างไรก็ตามสถานการณ์ไม่โชคดีนักสําหรับการส่งคืนสองครั้ง: เนื่องจากไม่มีการสร้างเฟรมใหม่เมื่อส่งคืนแฮ็กเกอร์สามารถรับตารางการดําเนินการและตารางกระโดดของลําดับการดําเนินการที่ถูกต้องและฉีดผลตอบแทนปลอมแปลง (และเฟรมที่เกี่ยวข้อง) ตัวอย่างเช่น ตัวอย่างตารางการดําเนินการและตารางข้ามก่อนหน้าของ buy_token() การเรียก add_token() อาจถูกแฮ็กเกอร์ดัดแปลงในสถานการณ์ต่อไปนี้:

แฮ็กเกอร์ได้แทรกการส่งคืนที่ปลอมแปลงสองครั้งระหว่างการเรียกเดิมและการส่งคืนในตารางการดําเนินการ และเพิ่มแถวเฟรมปลอมแปลงใหม่ในตารางการกระโดด (การส่งคืนเดิมและขั้นตอนการดําเนินการคําสั่งที่ตามมาในตารางการดําเนินการจะต้องเพิ่มขึ้น 4) เนื่องจากจํานวน "jops" สําหรับแต่ละแถวในตารางกระโดดคือ 2 ข้อ จํากัด จึงเป็นไปตามข้อกําหนดและตัวตรวจสอบการพิสูจน์ zkWasm จะยอมรับ "การพิสูจน์" ของลําดับการดําเนินการปลอมแปลงนี้ ดังที่เห็นจากรูป ยอดเงินในบัญชีโทเค็นเพิ่มขึ้น 3 เท่าแทนที่จะเป็น 1 ดังนั้นแฮ็กเกอร์สามารถรับ 3 โทเค็นในราคา 1

มีหลายวิธีในการแก้ไขปัญหานี้ แนวทางหนึ่งที่ชัดเจนคือการติดตามการโทรและการส่งคืนแยกกัน และตรวจสอบให้แน่ใจว่าแต่ละเฟรมมีการโทรหนึ่งครั้งและการส่งคืนหนึ่งครั้ง

คุณอาจสังเกตเห็นว่าจนถึงตอนนี้เรายังไม่ได้แสดงโค้ดแม้แต่บรรทัดเดียวสําหรับช่องโหว่นี้ เหตุผลหลักคือไม่มีบรรทัดรหัสที่มีปัญหา การใช้โค้ดสอดคล้องกับตารางและการออกแบบข้อจํากัดอย่างสมบูรณ์แบบ ปัญหาอยู่ที่การออกแบบเองและการแก้ไขก็เช่นกัน

คุณอาจคิดว่าช่องโหว่นี้ควรชัดเจน แต่ในความเป็นจริงไม่ใช่ นี่เป็นเพราะมีช่องว่างระหว่าง "สองสายหรือสองคืนจะส่งผลให้ 'jops' นับ 2" และ "สองคืนเป็นไปได้จริง" อย่างหลังต้องการการวิเคราะห์อย่างละเอียดและครอบคลุมเกี่ยวกับข้อจํากัดต่างๆ ในตารางการดําเนินการและตารางกระโดด

การเปรียบเทียบช่องโหว่สองจุด

"Load8 Data Injection Vulnerability" และ "Forgery Return Vulnerability" ทั้งคู่มีศักยภาพที่จะอนุญาตให้แฮ็กเกอร์จัดการหลักฐาน ZK สร้างธุรกรรมเท็จหลอกลวงตัวตรวจสอบหลักฐานและมีส่วนร่วมในการโจรกรรมหรือการจี้ อย่างไรก็ตามธรรมชาติและวิธีการค้นพบของพวกเขาแตกต่างกันมาก

"Load8 Data Injection Vulnerability" ถูกค้นพบระหว่างการตรวจสอบ zkWasm นี่ไม่ใช่งานง่าย เนื่องจากเราต้องตรวจสอบข้อจํากัดหลายร้อยข้อในโค้ด Rust กว่า 6,000 บรรทัดและคําแนะนํา zkWasm หลายสิบรายการ อย่างไรก็ตามเรื่องนี้ช่องโหว่นั้นค่อนข้างง่ายในการตรวจจับและยืนยัน เนื่องจากช่องโหว่นี้ได้รับการแก้ไขก่อนที่จะเริ่มการตรวจสอบอย่างเป็นทางการจึงไม่พบในระหว่างกระบวนการตรวจสอบ หากไม่พบช่องโหว่นี้ในระหว่างการตรวจสอบเราสามารถคาดหวังได้ว่าจะพบในระหว่างการตรวจสอบคําสั่ง Load8

พบ "ช่องโหว่การส่งคืนการปลอมแปลง" ระหว่างการตรวจสอบอย่างเป็นทางการหลังการตรวจสอบ เหตุผลหนึ่งที่เราไม่พบในระหว่างการตรวจสอบคือ zkWasm มีกลไกที่คล้ายกับ "jops" ที่เรียกว่า "mops" ซึ่งติดตามคําแนะนําการเข้าถึงหน่วยความจําที่สอดคล้องกับข้อมูลในอดีตสําหรับแต่ละหน่วยหน่วยความจําระหว่างรันไทม์ zkWasm ข้อ จํากัด ในการนับไม้ถูพื้นนั้นถูกต้องจริง ๆ เพราะมันติดตามคําสั่งหน่วยความจําเพียงประเภทเดียวการเขียนหน่วยความจําและข้อมูลประวัติของหน่วยความจําแต่ละหน่วยจะไม่เปลี่ยนรูปและเขียนเพียงครั้งเดียว (จํานวนไม้ถูพื้นคือ 1) แต่แม้ว่าเราจะสังเกตเห็นช่องโหว่ที่อาจเกิดขึ้นนี้ในระหว่างการตรวจสอบ เราก็ยังคงไม่สามารถยืนยันหรือแยกแยะทุกสถานการณ์ที่เป็นไปได้ได้อย่างง่ายดายหากไม่มีเหตุผลอย่างเป็นทางการที่เข้มงวดเกี่ยวกับข้อจํากัดที่เกี่ยวข้องทั้งหมด เนื่องจากจริงๆ แล้วไม่มีบรรทัดของโค้ดที่ไม่ถูกต้อง

โดยสรุป ช่องโหว่ทั้งสองนี้อยู่ในหมวดหมู่ของ "ช่องโหว่ของโค้ด" และ "ช่องโหว่ในการออกแบบ" ตามลําดับ ช่องโหว่ของโค้ดค่อนข้างตรงไปตรงมา ง่ายต่อการค้นพบ (รหัสผิดพลาด) และให้เหตุผลและยืนยันได้ง่ายขึ้น ช่องโหว่ในการออกแบบอาจเป็นเรื่องที่ละเอียดอ่อน ยากต่อการค้นพบ (ไม่มีโค้ดที่ "ผิดพลาด") และยากที่จะให้เหตุผลและยืนยัน

แนวทางปฏิบัติที่ดีที่สุดสําหรับการค้นหาช่องโหว่ของ ZK

จากประสบการณ์ของเราในการตรวจสอบและตรวจสอบ zkVM และเชน ZK และ non-ZK อื่น ๆ อย่างเป็นทางการต่อไปนี้เป็นคําแนะนําบางประการเกี่ยวกับวิธีปกป้องระบบ ZK ให้ดีที่สุด:

ตรวจสอบรหัสและการออกแบบ

ดังที่ได้กล่าวไว้ก่อนหน้านี้ทั้งรหัสและการออกแบบของ ZK อาจมีช่องโหว่ ช่องโหว่ทั้งสองประเภทอาจส่งผลต่อความสมบูรณ์ของระบบ ZK ดังนั้นจึงต้องได้รับการแก้ไขก่อนที่ระบบจะถูกนําไปใช้งาน ปัญหาหนึ่งของระบบ ZK เมื่อเทียบกับระบบที่ไม่ใช่ ZK คือการโจมตีใด ๆ นั้นตรวจจับและวิเคราะห์ได้ยากกว่าเนื่องจากรายละเอียดการคํานวณของพวกเขาไม่เปิดเผยต่อสาธารณะหรือเก็บไว้ในห่วงโซ่ ด้วยเหตุนี้ ผู้คนอาจทราบว่ามีการโจมตีของแฮ็กเกอร์เกิดขึ้น แต่พวกเขาอาจไม่ทราบรายละเอียดทางเทคนิคว่ามันเกิดขึ้นได้อย่างไร สิ่งนี้ทําให้ค่าใช้จ่ายของช่องโหว่ ZK สูงมาก ดังนั้นมูลค่าของการรับรองความปลอดภัยของระบบ ZK ล่วงหน้าจึงสูงมากเช่นกัน

ดําเนินการตรวจสอบและการตรวจสอบอย่างเป็นทางการ

ช่องโหว่สองจุดที่เรากล่าวถึงที่นี่ถูกค้นพบผ่านการตรวจสอบและการตรวจสอบอย่างเป็นทางการ บางคนอาจคิดว่าการตรวจสอบอย่างเป็นทางการเพียงอย่างเดียวทําให้ไม่จําเป็นต้องตรวจสอบ เนื่องจากช่องโหว่ทั้งหมดจะถูกตรวจพบผ่านการตรวจสอบอย่างเป็นทางการ อย่างไรก็ตามคําแนะนําของเราคือดําเนินการทั้งสองอย่าง ตามที่อธิบายไว้ในตอนต้นของบทความนี้งานตรวจสอบอย่างเป็นทางการคุณภาพสูงเริ่มต้นด้วยการตรวจสอบการตรวจสอบและการใช้เหตุผลอย่างไม่เป็นทางการเกี่ยวกับรหัสและการออกแบบอย่างละเอียดซึ่งทับซ้อนกับการตรวจสอบ นอกจากนี้ การค้นหาและแก้ไขช่องโหว่ที่ง่ายขึ้นในระหว่างการตรวจสอบสามารถลดความซับซ้อนและปรับปรุงกระบวนการตรวจสอบอย่างเป็นทางการได้

หากคุณกําลังดําเนินการทั้งการตรวจสอบและการตรวจสอบอย่างเป็นทางการสําหรับระบบ ZK วิธีที่ดีที่สุดคือดําเนินการทั้งสองอย่างพร้อมกัน สิ่งนี้ช่วยให้ผู้ตรวจสอบและวิศวกรตรวจสอบอย่างเป็นทางการสามารถทํางานร่วมกันได้อย่างมีประสิทธิภาพซึ่งอาจค้นพบช่องโหว่เพิ่มเติมเนื่องจากจําเป็นต้องมีอินพุตการตรวจสอบคุณภาพสูงสําหรับการตรวจสอบอย่างเป็นทางการ

หากโครงการ ZK ของคุณผ่านการตรวจสอบ (ความรุ่งโรจน์) หรือการตรวจสอบหลายครั้ง (ความรุ่งโรจน์ครั้งใหญ่) คําแนะนําของเราคือทําการตรวจสอบอย่างเป็นทางการในวงจรตามผลการตรวจสอบก่อนหน้านี้ ประสบการณ์ของเราเกี่ยวกับการตรวจสอบและการตรวจสอบอย่างเป็นทางการในโครงการเช่น zkVM และอื่น ๆ ทั้ง ZK และไม่ใช่ ZK ได้แสดงให้เห็นซ้ําแล้วซ้ําอีกว่าการตรวจสอบอย่างเป็นทางการมักจะจับช่องโหว่ที่พลาดไประหว่างการตรวจสอบ ด้วยลักษณะของ ZKP ในขณะที่ระบบ ZK ควรให้ความปลอดภัยและความสามารถในการปรับขนาดของบล็อกเชนที่ดีกว่าโซลูชันที่ไม่ใช่ ZK ความสําคัญของความปลอดภัยและความถูกต้องนั้นสูงกว่าระบบที่ไม่ใช่ ZK แบบดั้งเดิมมาก ดังนั้นมูลค่าของการตรวจสอบอย่างเป็นทางการคุณภาพสูงสําหรับระบบ ZK จึงสูงกว่าระบบที่ไม่ใช่ ZK

มั่นใจในความปลอดภัยของวงจรและสัญญาอัจฉริยะ

แอปพลิเคชัน ZK โดยทั่วไปประกอบด้วยสององค์ประกอบ: วงจรและสัญญาอัจฉริยะ สําหรับแอปพลิเคชันที่ใช้ zkVM มีวงจร zkVM สากลและแอปพลิเคชันสัญญาอัจฉริยะ สําหรับแอปพลิเคชันที่ไม่ได้ใช้ zkVM จะมีวงจร ZK เฉพาะแอปพลิเคชันพร้อมกับสัญญาอัจฉริยะที่เกี่ยวข้องซึ่งปรับใช้บนเชน L1 หรือที่ปลายอีกด้านหนึ่งของบริดจ์

ความพยายามในการตรวจสอบและการตรวจสอบอย่างเป็นทางการของเราสําหรับ zkWasm เกี่ยวข้องกับวงจร zkWasm เท่านั้น อย่างไรก็ตาม จากมุมมองของการรักษาความปลอดภัยโดยรวมสําหรับแอปพลิเคชัน ZK สิ่งสําคัญคือต้องตรวจสอบและตรวจสอบสัญญาอัจฉริยะอย่างเป็นทางการเช่นกัน ท้ายที่สุดมันจะเป็นเรื่องน่าเสียใจหากหลังจากลงทุนความพยายามอย่างมากในการรับรองความปลอดภัยของวงจรความหละหลวมในการตรวจสอบสัญญาอัจฉริยะนําไปสู่การประนีประนอมแอปพลิเคชัน

สัญญาอัจฉริยะสองประเภทสมควรได้รับความสนใจเป็นพิเศษ ประเภทแรกจัดการหลักฐาน ZK โดยตรง แม้ว่าพวกมันอาจไม่ใหญ่นัก แต่ความเสี่ยงก็สูงเป็นพิเศษ ประเภทที่สองประกอบด้วยสัญญาอัจฉริยะขนาดกลางถึงขนาดใหญ่ที่ทํางานบน zkVM เราทราบดีว่าบางครั้งสัญญาเหล่านี้อาจมีความซับซ้อนสูง และสัญญาที่มีค่าที่สุดควรได้รับการตรวจสอบและยืนยัน โดยเฉพาะอย่างยิ่งเนื่องจากรายละเอียดการดําเนินการของพวกเขาไม่ปรากฏให้เห็นบนเครือข่าย โชคดีที่หลังจากหลายปีของการพัฒนาการตรวจสอบอย่างเป็นทางการสําหรับสัญญาอัจฉริยะนั้นใช้งานได้จริงและเตรียมพร้อมสําหรับเป้าหมายที่มีมูลค่าสูงที่เหมาะสม

มาสรุปผลกระทบของการตรวจสอบอย่างเป็นทางการ (FV) ต่อระบบ ZK และส่วนประกอบด้วยประเด็นต่อไปนี้

ถ้อยแถลง:

1. บทความนี้ทําซ้ําจาก [panewslab] ลิขสิทธิ์เป็นของผู้เขียนต้นฉบับ [CertiK] หากคุณมีข้อโต้แย้งใด ๆ ต่อการพิมพ์ซ้ํา โปรดติดต่อทีม Gate Learn และทีมงานจะจัดการโดยเร็วที่สุดตามขั้นตอนที่เกี่ยวข้อง

2. ข้อจํากัดความรับผิดชอบ: มุมมองและความคิดเห็นที่แสดงในบทความนี้เป็นมุมมองส่วนตัวของผู้เขียนเท่านั้นและไม่ถือเป็นคําแนะนําในการลงทุนใดๆ

3. บทความเวอร์ชันภาษาอื่นได้รับการแปลโดยทีม Gate Learn และไม่ได้กล่าวถึงใน Gate.io บทความที่แปลแล้วไม่สามารถทําซ้ําแจกจ่ายหรือลอกเลียนแบบได้