Vitalik Buterin แห่ง Ethereum อธิบายว่า AI สามารถทำให้สัญญาอัจฉริยะปลอดภัยอย่างแท้จริงได้อย่างไร

โพสต์ Ethereum's Vitalik Buterin อธิบายว่า AI จะทำให้สัญญาอัจฉริยะปลอดภัยอย่างแท้จริงได้อย่างไร ปรากฏครั้งแรกบน Coinpedia Fintech News

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

"หลายคนอ้างว่าด้วยการค้นหาบั๊กที่ช่วยด้วย AI โค้ดที่ปลอดภัยจะเป็นไปไม่ได้" Buterin เขียน "ผมมีมุมมองที่มองโลกในแง่ดีกว่ามาก และการตรวจสอบเชิงรูปแบบที่ช่วยด้วย AI เป็นส่วนสำคัญของเหตุผลนั้น"

การตรวจสอบเชิงรูปแบบคืออะไรกันแน่

การตรวจสอบเชิงรูปแบบคือแนวทางปฏิบัติในการเขียนบทพิสูจน์ทางคณิตศาสตร์เกี่ยวกับโค้ดที่สามารถตรวจสอบได้โดยอัตโนมัติโดยคอมพิวเตอร์ แทนที่จะทดสอบซอฟต์แวร์และหวังว่าจะไม่มีบั๊กปรากฏขึ้น นักพัฒนาจะเขียนบทพิสูจน์ที่รับประกันทางคณิตศาสตร์ว่าโค้ดส่วนหนึ่งทำงานตรงตามที่ตั้งใจไว้ภายใต้ทุกเงื่อนไข

เทคโนโลยีนี้มีมานานหลายทศวรรษแต่ยังคงเป็นเฉพาะกลุ่มเพราะการเขียนบทพิสูจน์เหล่านี้ด้วยมือนั้นยากและใช้เวลานานมาก ข้อโต้แย้งของ Buterin คือ AI เปลี่ยนสมการนี้อย่างมากมาย AI สามารถเขียนทั้งโค้ดและบทพิสูจน์ได้ ในขณะที่มนุษย์เพียงแค่ตรวจสอบว่าคำสั่งที่พิสูจน์นั้นตรงกับสิ่งที่พวกเขาต้องการให้ซอฟต์แวร์ทำจริงๆ

เขาอธิบายการผสมผสานนี้ว่าคือสิ่งที่นักวิจัย Yoichi Hirai เรียกว่า "รูปแบบสุดท้ายของการพัฒนาซอฟต์แวร์"

ทำไมจึงสำคัญสำหรับ Ethereum

Buterin ชี้ให้เห็นหลายพื้นที่ที่การตรวจสอบเชิงรูปแบบกำลังถูกนำไปใช้แล้วภายในระบบนิเวศการพัฒนาของ Ethereum ซึ่งรวมถึงลายเซ็นที่ทนต่อควอนตัม ระบบพิสูจน์ STARK อัลกอริทึมฉันทามติ และ ZK-EVM ทั้งหมดเป็นพื้นที่ที่คุณสมบัติด้านความปลอดภัยนั้นกำหนดได้ง่าย แม้ว่าโค้ดพื้นฐานจะซับซ้อนอย่างยิ่ง

โปรเจกต์อย่าง Arklib กำลังมุ่งสู่การใช้งาน STARK ที่ได้รับการตรวจสอบเชิงรูปแบบอย่างสมบูรณ์ โปรเจกต์ evm-asm กำลังสร้าง EVM ทั้งหมดที่เขียนโดยตรงใน RISC-V assembly ซึ่งได้รับการตรวจสอบทางคณิตศาสตร์กับการใช้งานอ้างอิงที่มนุษย์อ่านได้ โปรโตคอลฉันทามติที่ทนทานต่อข้อผิดพลาดของไบแซนไทน์ก็กำลังถูกระบุและตรวจสอบอย่างเป็นทางการใน Lean เช่นกัน

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

ข้อจำกัดที่เขายอมรับ

Buterin ระมัดระวังที่จะไม่พูดเกินจริง การตรวจสอบเชิงรูปแบบมีรูปแบบความล้มเหลวที่แท้จริง บทพิสูจน์สามารถเขียนเกี่ยวกับเพียงส่วนหนึ่งของระบบในขณะที่บั๊กที่สำคัญซ่อนอยู่ในส่วนที่ยังไม่ได้รับการตรวจสอบ นักพัฒนาอาจลืมระบุคุณสมบัติที่สำคัญ ข้อกำหนดเชิงรูปแบบเองอาจผิดพลาด ช่องโหว่ของฮาร์ดแวร์อย่างการโจมตีแบบ side-channel สามารถหลีกเลี่ยงซอฟต์แวร์ที่ถูกต้องทางคณิตศาสตร์ได้

"ความถูกต้องที่พิสูจน์ได้ไม่ได้พิสูจน์ว่าซอฟต์แวร์นั้นถูกต้องในแบบที่มนุษย์ส่วนใหญ่เข้าใจความถูกต้อง" เขาเขียน สิ่งที่การตรวจสอบเชิงรูปแบบทำได้จริงๆ คือช่วยให้นักพัฒนาแสดงความตั้งใจของพวกเขาในหลายวิธีที่ซ้ำซ้อนและตรวจสอบโดยอัตโนมัติว่านิพจน์ทั้งหมดนั้นเข้ากันได้กับกันและกัน

วิสัยทัศน์ที่กว้างขึ้น

Buterin อธิบายอนาคตในแง่ดีที่ซอฟต์แวร์แบ่งออกเป็นสองชั้น ชั้นขอบที่ไม่ปลอดภัยจัดการฟังก์ชันที่มีความเสี่ยงต่ำกว่า ทำงานใน sandbox และดำเนินการด้วยสิทธิ์ขั้นต่ำ แกนหลักที่ปลอดภัยจัดการทุกสิ่งที่สำคัญ รวมถึง Ethereum เอง เคอร์เนลของระบบปฏิบัติการ และโครงสร้างพื้นฐาน IoT ที่ละเอียดอ่อน

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

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