ข่าว 
ข้อมูลเหรียญ 
แนะนำสื่อ 
ผลงานการตรวจสอบเชิงรูปแบบของวงจรหลัก zkWasm ที่ CertiK ดำเนินการเสร็จในปี 2024 ถูกนำกลับมาเผยแพร่อีกครั้ง โดยงานดังกล่าวไม่ใช่ผลงานใหม่ที่เสร็จสิ้นในปี 2026
CertiK ระบุในบล็อกเทคนิคปี 2024 ว่าได้ตรวจสอบว่า Halo2 circuit ของ zkWasm ซึ่งเป็นไปตามเงื่อนไขข้อจำกัดที่ถูกต้อง แสดงสถานะที่สอดคล้องกับกฎการทำงานของ WebAssembly (Wasm) หรือไม่ ขณะที่ Delphinus Lab ประกาศเมื่อวันที่ 2 พฤษภาคม 2024 ว่าการใช้งาน zkWasm ของบริษัทผ่านการตรวจสอบเชิงรูปแบบแล้ว
zkWasm เป็นระบบที่สร้าง zero-knowledge proof เพื่อยืนยันความถูกต้องของผลลัพธ์โดยไม่ต้องประมวลผลการคำนวณทั้งหมดซ้ำอีกครั้ง หลังโปรแกรม Wasm ทำงานเสร็จ ร่องรอยการทำงานของโปรแกรมจะถูกแปลงเป็นตารางหลายชุดใน Halo2 และผู้ตรวจสอบจะตรวจว่าทุกตารางเป็นไปตามข้อจำกัดทางคณิตศาสตร์ที่กำหนดหรือไม่
การตรวจสอบเชิงรูปแบบแตกต่างจากการตรวจสอบโค้ดทั่วไป เพราะไม่ได้มองหาเพียงรูปแบบช่องโหว่ที่รู้จัก แต่จะแปลงคำถามว่าโปรแกรมทำงานตามกฎที่กำหนดภายใต้เงื่อนไขเฉพาะหรือไม่ ให้เป็นข้อพิสูจน์ทางคณิตศาสตร์ที่เครื่องสามารถตรวจสอบได้
ใน zkVM วงจรเดียวสามารถรองรับการทำงานของโปรแกรมได้หลากหลาย ดังนั้นการตรวจสอบว่าข้อจำกัดของวงจรสอดคล้องกับความหมายการทำงานจริงของ Wasm หรือไม่ จึงเป็นขั้นตอนสำคัญในการประเมินความถูกต้องของผลการพิสูจน์
คลังโค้ดสาธารณะของ CertiK ระบุว่า การตรวจสอบเชิงรูปแบบที่เขียนด้วย Coq ครอบคลุมองค์ประกอบหลักของวงจร zkWasm เช่น ตารางการทำงาน ตารางหน่วยความจำ call stack และการดำเนินการระดับบิต เป้าหมายคือการพิสูจน์ว่า หากข้อจำกัดของวงจรทั้งหมดเป็นจริง แต่ละแถวของร่องรอยการทำงานจะแสดงสถานะที่สอดคล้องกับกฎการทำงานของ Wasm
ในระหว่างการตรวจสอบยังพบและแก้ไขปัญหาเกี่ยวกับการเข้าถึงหน่วยความจำ รวมถึงโครงสร้างการเรียกใช้และการส่งคืนของวงจร ซึ่งสะท้อนว่าการตรวจสอบเชิงรูปแบบไม่ได้จำกัดอยู่ที่การทบทวนโค้ดเดิม แต่ยังสามารถค้นหาความไม่สอดคล้องระหว่างข้อกำหนดกับการใช้งานจริงได้
อย่างไรก็ตาม ไม่ควรตีความว่า zkWasm ทั้งระบบผ่านการตรวจสอบอย่างสมบูรณ์แล้ว คลังโค้ดสาธารณะมีโมเดล Coq โค้ดพิสูจน์ และขั้นตอนการคอมไพล์ แต่ไม่ได้ครอบคลุมอัลกอริทึมทั้งหมดที่เขียนด้วย Rust
ขอบเขตการเปิดเผยก็ยังมีข้อจำกัด แม้จะมีการเผยแพร่โค้ดตรวจสอบแล้ว แต่การกำหนดค่าบางส่วนของวงจร ตรรกะการถอดรหัสคำสั่ง การทำงานของ Wasmi interpreter และการทำงานของ Halo2 ยังอาศัยสมมติฐานหรืออยู่นอกขอบเขตการตรวจสอบ
Wasmi interpreter ตัว Halo2 เอง และโค้ดบางส่วนที่สร้างข้อจำกัดก็ไม่ได้อยู่ในขอบเขตการตรวจสอบเช่นกัน ขณะที่ฟังก์ชันการเรียกใช้ภายนอกและตรรกะการถอดรหัสคำสั่งบางส่วนยังพึ่งพาสมมติฐานเพิ่มเติมหรือการทบทวนด้วยมนุษย์
CertiK ระบุว่าคลังโค้ดภายในที่เกี่ยวข้องมีโค้ด Coq รวม 33,080 บรรทัด แต่การเปิดเผยขนาดโค้ดไม่ได้หมายความว่าขอบเขตการพิสูจน์ทั้งหมดถูกเปิดเผย
รายงานประจำปี 2024 ของ CertiK ระบุว่าการตรวจสอบครอบคลุมวงจร zkWasm ที่ประกอบด้วยคำสั่ง 144 รายการ และประเมินว่าเป็นการตรวจสอบเชิงรูปแบบอย่างสมบูรณ์ครั้งแรกในระบบนิเวศ zero-knowledge proof อย่างไรก็ตาม นี่เป็นคำอธิบายของ CertiK เอง และยังไม่พบเกณฑ์เปรียบเทียบอิสระหรือผลการประเมินโดยผู้ทรงคุณวุฒิที่ยืนยันถ้อยคำดังกล่าว
CertiK ระบุว่าเฟรมเวิร์กการตรวจสอบเชิงรูปแบบดังกล่าวสามารถนำไปใช้กับ zkVM และ zkEVM อื่นได้ แต่เป็นเพียงคำอธิบายเรื่องความเป็นไปได้ในการประยุกต์ใช้จากบริษัท ไม่ได้หมายความว่าระบบอื่นผ่านการตรวจสอบแล้ว
Delphinus Lab เผยแพร่ข้อมูลว่าการใช้งาน zkWasm ของบริษัทผ่านการตรวจสอบเชิงรูปแบบ พร้อมเชื่อมโยงเอกสารทางเทคนิคของ CertiK ปฏิกิริยาเชิงบวกจากผู้พัฒนาสามารถยืนยันได้ แต่ไม่ได้หมายความว่าขอบเขตการตรวจสอบขยายไปครอบคลุมซอฟต์แวร์ทั้งหมด
CertiK ยังระบุว่าในเวลาต่อมาได้ใช้ Verus เพื่อนำบางส่วนของการพิสูจน์ zkWasm เดิมกลับมาสร้างใหม่ โดยลดขนาดโค้ดจาก 2,440 บรรทัดเหลือ 595 บรรทัด งานนี้เป็นการศึกษาต่อยอดที่แยกจากการประกาศเสร็จสิ้นการตรวจสอบครั้งแรก และไม่ควรถูกมองว่าเป็นการขยายขอบเขตการเปิดเผยของการตรวจสอบเดิม
งานวิจัยที่เกี่ยวข้องได้รับการลงทะเบียนเป็นบทความที่มีกำหนดเผยแพร่ในโครงการ ACM CCS 2026 ภายใต้ชื่อ “Formal Verification of Circuit-Soundness in zkWasm, a General Purpose zkVM” โดยมีนักวิจัยจาก CertiK, Delphinus Lab, NVIDIA (NVDA), Columbia University และ Yale University ร่วมเขียน อย่างไรก็ตาม รายละเอียดฉบับเต็มของบทความและผลการพิจารณายังไม่สามารถยืนยันได้จากข้อมูลสาธารณะ
ประเด็นสำคัญของกรณีนี้คือความพยายามอธิบายความถูกต้องของวงจรในโครงสร้างพื้นฐาน zkVM ด้วยคณิตศาสตร์ได้พัฒนาไปสู่ผลงานวิจัยที่เป็นรูปธรรม ขณะเดียวกันยังจำเป็นต้องแยกขอบเขตการตรวจสอบที่เปิดเผยและความสามารถในการทำซ้ำ ออกจากการสรุปว่าซอฟต์แวร์ทั้งระบบมีความปลอดภัย
ความคิดเห็น 0