ข่าว 
ข้อมูลเหรียญ 
แนะนำสื่อ 
มีรายงานว่า LayerZero Research ตรวจสอบส่วนขยายไบต์โค้ด RISC-V ของ Jolt zkVM ได้ 60 รายการจากทั้งหมด 67 รายการ ส่วนคำสั่งที่เหลืออีก 7 รายการยังอยู่ระหว่างการตรวจสอบ เนื่องจากเกี่ยวข้องกับกรณีขอบบางรูปแบบ
CryptoBriefing รายงานว่า LayerZero Research ใช้เวลาประมาณ 2 เดือนครึ่งในการตรวจสอบดังกล่าว โดยใช้ตัวพิสูจน์ทฤษฎี Lean อย่างไรก็ตาม ตัวเลขและเอกสารการตรวจสอบนี้ยังไม่ได้รับการยืนยันในรายละเอียดเดียวกันผ่านช่องทางอย่างเป็นทางการของ LayerZero
การตรวจสอบรูปแบบ (formal verification) คือการยืนยันด้วยหลักฐานทางคณิตศาสตร์ว่าซอฟต์แวร์เป็นไปตามข้อกำหนดที่กำหนดไว้ ไม่ใช่การทดสอบทั่วไป ขั้นตอนนี้มีความสำคัญใน zkVM เพราะการตีความคำสั่งผิดพลาดหรือข้อผิดพลาดระหว่างการทำงานอาจทำให้ผลลัพธ์ที่ไม่ถูกต้องถูกยอมรับเป็นหลักฐานที่ใช้ได้
ส่วนขยายไบต์โค้ดของ Jolt แปลงคำสั่ง RISC-V ดิบในไฟล์ ELF ที่ถอดรหัสแล้วให้เป็นตัวแทนภายใน ซึ่งรวมถึงตัวถูกดำเนินการ แอดเดรส แฟล็กวงจร และแฟล็กการค้นหา เอกสารอย่างเป็นทางการของ Jolt อธิบายว่าไบต์โค้ดเป็นจุดอ้างอิงของโปรแกรมที่นำมาใช้ในการทำงาน
ดัชนีไบต์โค้ดแบบขยายและแอดเดรสหน่วยความจำ ELF มีหน้าที่แตกต่างกัน ดัชนีไบต์โค้ดใช้เข้าถึงคำสั่งในแต่ละรอบการทำงาน ขณะที่แอดเดสหน่วยความจำ ELF ใช้ตรวจสอบข้อจำกัดของตัวนับโปรแกรม
ระหว่างการทำงาน ระบบยังพิสูจน์ด้วยว่าคำสั่งที่อ่านมาสอดคล้องกับไบต์โค้ดที่ผ่านการประมวลผลล่วงหน้าหรือไม่ ดังนั้นความถูกต้องของขั้นตอนการขยายไบต์โค้ดจึงอาจส่งผลต่อความน่าเชื่อถือของเส้นทางการทำงานและผลลัพธ์ของการสร้างหลักฐานในขั้นถัดไป
การตรวจสอบครั้งนี้ไม่ได้หมายความว่าการตรวจสอบรูปแบบของ Jolt ทั้งหมดเสร็จสิ้นแล้ว แอนดรีสเซน โฮโรวิทซ์อธิบายไว้ในบทความทางเทคนิคปี 2024 ว่างานตรวจสอบ Jolt เป็นกระบวนการแบบเป็นขั้นตอน ซึ่งครอบคลุมความสอดคล้องระหว่างความหมายของการค้นหา ระบบพิสูจน์เชิงโต้ตอบแบบพหุนาม ระบบข้อจำกัด ข้อกำหนด RISC-V และการใช้งานจริงด้วย Rust
แผนงานการตรวจสอบของแอนดรีสเซน โฮโรวิทซ์ยังระบุว่าต้องตรวจสอบแยกต่างหากว่าแบบจำลองที่ทำให้เป็นรูปแบบและโค้ดการใช้งานจริงสอดคล้องกันหรือไม่ แม้จะพิสูจน์แบบจำลองรูปแบบใน Lean ได้แล้ว ก็ยังต้องตรวจสอบเพิ่มเติมว่าแบบจำลองดังกล่าวสะท้อนการใช้งานจริงได้อย่างถูกต้องหรือไม่
งานวิจัยก่อนหน้านี้ใช้ตัวพิสูจน์ทฤษฎี ACL2 เพื่อตรวจสอบความหมายของการค้นหาสำหรับคำสั่ง RISC-V RV32I ของ Jolt นักวิจัยตรวจสอบว่าการแยกคำสั่งออกเป็นตารางค้นหาขนาดเล็กสอดคล้องกับข้อกำหนด RISC-V หรือไม่ และยังพบการปรับปรุงที่ช่วยลดการค้นหาที่ไม่จำเป็นในคำสั่งบางรายการ
งานวิจัยที่เกี่ยวข้องระบุว่าได้ทำให้คำสั่ง RV32I ทั้งหมดเป็นรูปแบบและตรวจสอบด้วย ACL2 แล้ว งานที่ใช้ Lean ในครั้งนี้จึงอาจมองได้ว่าเป็นกรณีที่ตรวจสอบขอบเขตการขยายไบต์โค้ดโดยใช้ตัวพิสูจน์ทฤษฎีที่แตกต่างจากงานวิจัยก่อนหน้า
LayerZero อธิบายในเอกสารทางเทคนิคของ Zero ว่า Jolt ถูกใช้เป็นโครงสร้างพื้นฐานด้านหลักฐานการทำงานของเครือข่าย Zero มีกระบวนการสร้างและตรวจสอบหลักฐานการทำงาน ขณะที่ Jolt ทำหน้าที่เป็น zkVM ซึ่งพิสูจน์ว่าผลลัพธ์จากการทำงานของโปรแกรมถูกต้อง
อย่างไรก็ตาม การตรวจสอบส่วนขยายไบต์โค้ดเพียงอย่างเดียวไม่อาจสรุปได้ว่าความปลอดภัยของเครือข่าย Zero ทั้งหมดหรือ Jolt ทั้งหมดได้รับการตรวจสอบแล้ว เนื่องจากยังต้องตรวจสอบความสอดคล้องระหว่างการใช้งานจริงด้วย Rust กับแบบจำลองรูปแบบ รวมถึงขอบเขตการตรวจสอบขององค์ประกอบอื่นในระบบพิสูจน์
การนำเสนอทางเทคนิคก่อนหน้านี้เกี่ยวกับ Akita และ Lattice Jolt ที่เผยแพร่โดย LayerZero และแอนดรีสเซน โฮโรวิทซ์มุ่งเน้นองค์ประกอบด้านการเข้ารหัสของโครงสร้างพื้นฐานการพิสูจน์แบบไม่เปิดเผยข้อมูล ส่วนงานครั้งนี้มุ่งเน้นการตีความคำสั่งระหว่างการทำงานและการแปลงไบต์โค้ด จึงแตกต่างจากการนำเสนอก่อนหน้า
ยังไม่มีการเปิดเผยรายชื่อคำสั่งทั้ง 60 รายการที่ผ่านการตรวจสอบและ 7 รายการที่ยังไม่ได้รับการตรวจสอบ โดยเฉพาะรายละเอียดว่าคำสั่งทั้ง 7 รายการเกี่ยวข้องกับกรณีขอบใด และโค้ดการใช้งานจริงสอดคล้องกับแบบจำลองรูปแบบในระดับใด ยังเป็นประเด็นที่ต้องรอข้อมูลเพิ่มเติม
การประกาศครั้งนี้จึงควรสรุปว่าเป็นความคืบหน้าในการตรวจสอบรูปแบบขององค์ประกอบบางส่วนใน Jolt zkVM ขอบเขตการตรวจสอบยังจำกัด และไม่ควรตีความขยายไปถึงการตรวจสอบความปลอดภัยของ zkVM ทั้งหมดหรือเครือข่าย Zero ทั้งหมด
ความคิดเห็น 0