Vitalik Buterin ปฏิเสธคำกล่าวอ้างว่า AI จะทำให้ความปลอดภัยไซเบอร์ล่มสลาย โดย Olivia Stephanie

Buterin เขียนในโพสต์ X เมื่อวันที่ 17 ก.ย. ว่าเขาไม่เห็นด้วยกับมุมมองที่แพร่หลายมากขึ้นเรื่อย ๆ ว่า “การแฮ็กด้วย AI หมายความว่าความปลอดภัยไซเบอร์ถึงจุดจบแล้ว” เขากล่าวว่าผู้ที่ยังคงถือคริปโตเคอร์เรนซีกำลังเดิมพันโดยปริยายว่าระบบดิจิทัลที่ปลอดภัยสามารถอยู่รอดจากการโจมตีอัตโนมัติที่แข็งแกร่งขึ้นได้ พร้อมเสริมว่าประมาณ 90% ของมูลค่าทรัพย์สินสุทธิของเขายังคงอยู่ในคริปโตเคอร์เรนซี

ข้อโต้แย้งของเขามุ่งเน้นไปที่การตรวจสอบเชิงรูปแบบ (formal verification) ซึ่งเป็นเทคนิคที่ใช้ข้อกำหนดทางคณิตศาสตร์และการพิสูจน์เพื่อตรวจสอบว่าซอฟต์แวร์ทำงานตามคุณสมบัติที่กำหนดไว้ล่วงหน้าหรือไม่ Buterin ใช้การพิสูจน์ทฤษฎีบททางคณิตศาสตร์ขั้นสูงเป็นอุปมา โดยกล่าวว่า AI ที่มีความสามารถเพียงพอสามารถช่วยพิสูจน์ได้ว่า “โปรแกรมนี้ปลอดภัย” แม้ว่าตัวซอฟต์แวร์เองจะซับซ้อนก็ตาม

Buterin กล่าวว่าการตรวจสอบเชิงรูปแบบสามารถเอื้อประโยชน์ต่อฝ่ายตั้งรับ

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

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

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

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

Buterin เคยอธิบายว่าการตรวจสอบเชิงรูปแบบที่ช่วยด้วย AI อาจเป็น “รูปแบบสุดท้าย” ของการพัฒนาซอฟต์แวร์ ความเห็นก่อนหน้านี้ของเขาใช้แนวทางนี้กับพื้นที่ต่าง ๆ รวมถึงฉันทามติของ Ethereum ระบบ zero-knowledge และการเข้ารหัสที่ต้านทานควอนตัม

Ethereum กำลังทดสอบความปลอดภัยที่ช่วยด้วย AI อยู่แล้ว

นักวิจัยของ Ethereum ใช้ AI ในงานด้านความปลอดภัยอยู่แล้ว แม้ว่าระบบปัจจุบันยังห่างไกลจากการพิสูจน์ความปลอดภัยของทั้งระบบโดยอัตโนมัติ

ทีม Protocol Security ของ Ethereum Foundation รายงานในเดือนกรกฎาคมว่าเอเจนต์ AI ที่ประสานงานกันพบข้อบกพร่องจริงในระบบที่ Ethereum ใช้ การค้นพบที่ได้รับการยืนยันรายการหนึ่งเกี่ยวข้องกับข้อขัดข้องที่เข้าถึงได้จากระยะไกลในการใช้งานเครือข่าย Gossipsub ของ Rust libp2p

ข้อบกพร่องดังกล่าวกลายเป็น CVE-2026-34219 บันทึกของ U.S. National Vulnerability Database ระบุว่าเวอร์ชันก่อน 0.49.4 อาจถูกทำให้ขัดข้องจากระยะไกลผ่านข้อความ PRUNE ที่สร้างขึ้นเป็นพิเศษ ซึ่งทำให้เกิด arithmetic overflow ระหว่างการจัดการ Gossipsub backoff เวอร์ชัน 0.49.4 แก้ไขปัญหานี้แล้ว

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

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

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

การตรวจสอบเชิงรูปแบบกำลังเข้าสู่แผนงานโปรโตคอลของ Ethereum

Ethereum Foundation ได้แยกการตรวจสอบเชิงรูปแบบให้เป็นส่วนหนึ่งของโครงการวิจัยโปรโตคอลปัจจุบัน ในการอัปเดตลำดับความสำคัญของโปรโตคอลเมื่อวันที่ 7 ก.ย. Foundation กล่าวว่าการตรวจสอบเชิงรูปแบบจะทำหน้าที่เป็นเครื่องมือข้ามสายงานในพื้นที่การวิจัยหลายปีที่เหลืออยู่ เอกสารครอบคลุมงานด้านความเป็นส่วนตัว สถานะ การพัฒนา zkEVM ความปลอดภัยหลังควอนตัม และส่วนประกอบโปรโตคอลอื่น ๆ จนถึงปี 2029

แผนงานเดียวกันระบุว่าการพัฒนา L1 zkEVM คาดว่าจะช่วยพัฒนาเครื่องมือการตรวจสอบเชิงรูปแบบ เวิร์กโฟลว์ และส่วนประกอบการเข้ารหัสที่ผ่านการตรวจสอบแล้ว นักวิจัยของ Ethereum กำลังทำงานไปสู่ระบบที่ผู้ตรวจสอบจะตรวจสอบหลักฐานการประมวลผลแบบย่อแทนการประมวลผลทุกบล็อกใหม่โดยอิสระ

โครงการแยกต่างหากของ Ethereum Foundation ที่เปิดตัวในเดือนสิงหาคมกำลังผสานเอเจนต์ AI เข้ากับการพิสูจน์ที่ตรวจสอบด้วยเครื่องจักรแล้ว โครงการ better.codes ช่วยให้นักวิจัยสั่งให้ระบบ AI จัดการกับปัญหาความถูกต้องด้านการเข้ารหัสที่กำหนดเป็นทางการใน Lean ในขณะที่เคอร์เนล Lean ตรวจสอบว่าหลักฐานที่ส่งมาตรงกับข้อความทฤษฎีบทที่กำหนดไว้หรือไม่

รายงานการให้ทุนไตรมาส 2 ของ Foundation ระบุงานเพิ่มเติมที่ผสานโมเดลภาษาขนาดใหญ่เข้ากับวิธีการเชิงรูปแบบ โครงการต่าง ๆ รวมถึง ETHeorem สำหรับตรวจสอบการใช้งานไคลเอนต์ Ethereum เทียบกับข้อกำหนด SPECA และ LeanAgent สำหรับงานตรวจสอบการปฏิบัติตามโปรโตคอลอัตโนมัติ และการตรวจสอบเชิงรูปแบบที่เกี่ยวข้องกับโครงสร้างพื้นฐาน RISC-V zkVM

แผนงานทางเทคนิคที่อัปเดตของ Ethereum ให้บทบาทการตรวจสอบเชิงรูปแบบควบคู่ไปกับความเป็นส่วนตัว หลักฐาน zero-knowledge และการป้องกันหลังควอนตัม ความเห็นของ Buterin เมื่อวันที่ 17 ก.ย. จึงเป็นการสานต่อแนวทางการวิจัยที่มีอยู่แล้ว แทนที่จะประกาศการอัปเกรดใหม่หรือการ fork ตามกำหนดการ โพสต์ของเขาไม่ได้ระบุ EIP ใหม่ วันปรับใช้ หรือกฎบังคับที่กำหนดให้ทุกโปรแกรม Ethereum ต้องผ่านการตรวจสอบเชิงรูปแบบ

หลักฐาน AI ปัจจุบันยังแสดงถึงความสามารถในการโจมตีที่แข็งแกร่งขึ้นด้วย

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

งานวิจัยก่อนหน้านี้จาก Anthropic พบหลักฐานที่คล้ายกันในวงกว้าง แดชบอร์ดการเปิดเผยข้อมูลแบบประสานงานของบริษัทระบุว่า ณ วันที่ 26 ส.ค. บริษัทได้เปิดเผยช่องโหว่ที่ AI ค้นพบ 2,300 รายการในโครงการโอเพนซอร์ส 392 โครงการ โดย 421 รายการได้รับการแพตช์ต้นทางแล้ว ณ จุดนั้น

Anthropic อธิบายว่าเทคโนโลยีเดียวกันนี้มีประโยชน์ต่อการป้องกัน โครงการ Project Glasswing ของบริษัทรายงานว่าใช้โมเดล frontier ร่วมกับบริษัทความปลอดภัยและผู้จำหน่ายซอฟต์แวร์เพื่อค้นหาข้อบกพร่องระดับสูงและร้ายแรงก่อนที่ผู้ไม่หวังดีจะใช้ประโยชน์ได้

ด้านการโจมตียังคงวัดผลได้ การศึกษาของ Anthropic ในเดือนมิถุนายนตรวจสอบบัญชี 832 บัญชีที่เกี่ยวข้องกับกิจกรรมไซเบอร์ที่เป็นอันตรายตั้งแต่เดือนมีนาคม 2025 ถึงมีนาคม 2026 และพบว่าผู้คุกคามใช้ AI ในหลายขั้นตอนของการปฏิบัติการไซเบอร์ Buterin เคยปฏิเสธข้อโต้แย้งอีกประการหนึ่งว่าความเสี่ยงด้านความปลอดภัยที่ขับเคลื่อนด้วย AI อาจทำลายความเชื่อมั่นใน Bitcoin อย่างรุนแรง เขากล่าวว่าปัญหาในระดับเครือข่ายมักแก้ไขได้ด้วยการอัปเกรดซอฟต์แวร์และโครงสร้างพื้นฐานการขุด ในขณะที่อธิบายว่าการเจาะแฮชหรือกลไก proof-of-work ของ Bitcoin จริง ๆ นั้นไม่น่าเป็นไปได้อย่างยิ่ง

รายงานเดือนกันยายนของ Anthropic กล่าวว่าผู้สืบสวนของบริษัทระบุผู้ปฏิบัติการที่ใช้ไปป์ไลน์ช่องโหว่ที่สร้างด้วย AI กับอุปกรณ์ความปลอดภัยและเป้าหมายภาครัฐ โดยบางแคมเปญสร้างช่องโหว่ที่ไม่เคยรู้จักมาก่อนซึ่งผู้โจมตีตรวจสอบในสภาพแวดล้อมทดสอบของตนเอง