Vitalik: อะไรคือหัวใจสำคัญของ Ethereum ในช่วงต่อไป?

ผู้เขียน: วิตาลิก บูเทอริน

แปลโดย: เจียฮวา, เชนแคทเชอร์

ขอขอบคุณเป็นพิเศษแก่ Yoichi Hirai, Justin Drake, Nadim Kobeissi และ Alex Hicks สำหรับข้อเสนอแนะและการตรวจสอบของพวกเขา

ในช่วงไม่กี่เดือนที่ผ่านมา รูปแบบการเขียนโปรแกรมใหม่ได้รับความนิยมอย่างรวดเร็วในแวดวงการพัฒนา Ethereum และวงการคอมพิวเตอร์อื่นๆ อีกมากมาย นั่นคือ การเขียนโค้ดโดยตรงในภาษาที่ระดับต่ำมาก (เช่น EVM bytecode, ภาษาแอสเซมบลี) หรือ Lean และใช้การพิสูจน์ทางคณิตศาสตร์ที่ตรวจสอบได้โดยอัตโนมัติซึ่งเขียนด้วย Lean เพื่อตรวจสอบความถูกต้องของโค้ด

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

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

การตรวจสอบอย่างเป็นทางการคืออะไร?

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

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …

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

กรณีแรกคือกรณีพื้นฐาน ให้ F1 = F2 = 1, F3 = 2 จากการสังเกต เราจะเห็นว่าข้อความ ("Fi เป็นจำนวนคู่เมื่อ i เป็นพหุคูณของ 3 มิฉะนั้นจะเป็นจำนวนคี่") เป็นจริงก่อนที่ x จะเท่ากับ 3

ต่อไปเป็นกรณีอุปนัย สมมติว่าข้อความดังกล่าวเป็นจริงก่อน 3k+3 ซึ่งหมายความว่าเรารู้แล้วว่าค่าคู่หรือคี่ของ F3k+1, F3k+2 และ F3k+3 คือ คี่ คี่ และคู่ ตามลำดับ เราสามารถคำนวณค่าคู่หรือคี่ของกลุ่มตัวเลขสามตัวถัดไปได้:

F3k+4 = F3k+2 + F3k+3 = คี่ + คู่ = คี่

F3k+5 = F3k+3 + F3k+4 = คู่ + คี่ = คี่

F3k+6 = F3k+4 + F3k+5 = คี่ + คี่ = คู่

ดังนั้น จากการที่เรารู้ว่าข้อความนี้เป็นจริงก่อน 3k+3 เราจึงสรุปได้ว่าข้อความนี้เป็นจริงก่อน 3k+6 เราสามารถใช้เหตุผลนี้ซ้ำๆ ได้ เพื่อให้มั่นใจว่ากฎนี้ใช้ได้กับจำนวนเต็มทุกจำนวน

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

นี่คือวิธีการนำเสนอ:

-- ลำดับฟิโบนาชี่ โดยที่ fib 0 = 0, fib 1 = 1, fib 2 = 1 (ดัชนีเลื่อนไปทีละ 1)

def fib : Nat → Nat

| 0 => 0

| 1 => 1

| n + 2 => fib (n + 1) + fib n

-- ข้ออ้าง: fib (3k+1) เป็นจำนวนคี่, fib (3k+2) เป็นจำนวนคี่, fib (3k+3) เป็นจำนวนคู่

-- กล่าวอีกนัยหนึ่งคือ ทุกๆ จำนวนฟิโบนาชี่ลำดับที่สามนับจากลำดับที่ 3 จะเป็นจำนวนคู่

-- เราพิสูจน์ทั้งสามกรณีพร้อมกันโดยใช้วิธีอุปนัยบน k เนื่องจากแต่ละกรณี

-- บล็อกถัดไปสร้างขึ้นจากบล็อกก่อนหน้า

ทฤษฎีบท fib_triple (k : Nat) :

fib (3 * k + 1) % 2 = 1 ∧

fib (3 * k + 2) % 2 = 1 ∧

fib (3 * k + 3) % 2 = 0 := by

การเหนี่ยวนำ k กับ

| ศูนย์ => ตัดสินใจ

| succ k ih =>

-- เขียนดัชนีใหม่ให้อยู่ในรูปแบบ (บางอย่าง) + 2 เพื่อให้ลำดับฟิวชันคลี่ออก

ปรับแต่ง ⟨?_, ?_, ?_⟩

· แสดง (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1

โอเมก้า

· แสดง (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1

โอเมก้า

· แสดง (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)

+ (ตอแหล (3 * k + 3) + ตอแหล (3 * k + 2))) % 2 = 0

โอเมก้า

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

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

ในการพิสูจน์ข้างต้น คุณไม่ได้เน้นย้ำข้อเท็จจริงที่ว่า fib(3k+4) = fib(3k+3) + fib(3k+2) แต่กลับเน้นย้ำว่า fib(3k+3) + fib(3k+2) เป็นจำนวนคี่ ในขณะที่กลยุทธ์ใน Lean ที่เรียกว่า omega จะรวมข้อเท็จจริงนี้เข้ากับความรู้เกี่ยวกับนิยามของ fib(3k+4) โดยอัตโนมัติ

ในการพิสูจน์ที่ซับซ้อนมากขึ้น บางครั้งคุณต้องระบุอย่างชัดเจนว่ากฎทางคณิตศาสตร์ใดที่อนุญาตให้คุณดำเนินการในขั้นตอนปัจจุบัน และบางครั้งคุณต้องใช้ชื่อที่ไม่คุ้นเคย เช่น Prod.mk.inj

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

ลักษณะที่ไม่เป็นไปตามสัญชาตญาณและยุ่งยากนี้เองที่เป็นเหตุผลว่าทำไม แม้จะมีหลักฐานที่ตรวจสอบได้ด้วยเครื่องจักรมาเกือบ 60 ปีแล้ว แต่สาขานี้ก็ยังคงเป็นเพียงกลุ่มเฉพาะ อย่างไรก็ตาม ในทางกลับกัน ด้วยการพัฒนาอย่างรวดเร็วของปัญญาประดิษฐ์ สิ่งที่เคยเป็นไปไม่ได้หลายอย่างกำลังกลายเป็นไปได้ในปัจจุบัน

เมื่อการพิสูจน์ทางคณิตศาสตร์เริ่มปกป้องโค้ด

จนถึงตอนนี้ คุณอาจคิดว่า: คอมพิวเตอร์สามารถตรวจสอบข้อพิสูจน์ของทฤษฎีบททางคณิตศาสตร์ได้ ดังนั้นเราจึงสามารถระบุได้ในที่สุดว่าข้อสรุปใหม่ ๆ เกี่ยวกับจำนวนเฉพาะข้อไหนเป็นจริง และข้อไหนเป็นเพียงข้อผิดพลาดในเอกสาร PDF ความยาวร้อยหน้า

บางทีเราอาจจะหาคำตอบได้ว่ามุมมองของชินอิจิ โมจิซึกิเกี่ยวกับสมมติฐาน ABC นั้นถูกต้องหรือไม่!

แต่ถ้าไม่นับเรื่องความอยากรู้แล้ว ล่ะ?

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

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

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

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

ปรากฏว่ามีทีมงานที่กำลังพยายามหาคำตอบเกี่ยวกับปัญหานี้อยู่จริง ๆ! หนึ่งในทฤษฎีบทด้านความปลอดภัยของพวกเขามีลักษณะดังนี้:

ทฤษฎีบท passive_secrecy_le_ddh

(ก : ก)

(adv : PassiveAdversary G SK) :

passiveSecrecyAdvantage (F := F) g adv ≤

ProbComp.boolDistAdvantage

(DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))

(DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

ต่อไปนี้คือบทสรุปความหมายจาก Leanstral:

ทฤษฎี passivesecrecyle_ddh เป็นการลดรูปอย่างกระชับที่แสดงให้เห็นว่าการรักษาความลับของข้อความแบบพาสซีฟของ X3DH นั้นยากอย่างน้อยก็เท่ากับการสมมติฐาน DDH ในแบบจำลองออราเคิลแบบสุ่ม หากฝ่ายตรงข้ามสามารถทำลายการรักษาความลับของข้อความแบบพาสซีฟของ X3DH ได้ พวกเขาก็สามารถทำลาย DDH ได้เช่นกัน

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

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

โครงการที่คล้ายกันนี้ยังได้พิสูจน์แล้วว่าการใช้งาน TLS และส่วนอื่นๆ ของการเข้ารหัสภายในเบราว์เซอร์นั้นมีความปลอดภัย

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

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

อย่างไรก็ตาม มีข้อควรระวังที่สำคัญบางประการที่ควรคำนึงถึง โดยเฉพาะอย่างยิ่งเกี่ยวกับความหมายที่แท้จริงของคำว่า "ปลอดภัย" ซึ่งเป็นคำสำคัญอย่างยิ่ง

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

การตั้งสมมติฐานโดยไม่ตั้งใจลงไปในการพิสูจน์นั้นเป็นเรื่องง่าย ซึ่งในที่สุดแล้วสมมติฐานเหล่านั้นก็อาจไม่เป็นจริง นอกจากนี้ การตัดสินใจว่าเพียงส่วนใดส่วนหนึ่งของระบบเท่านั้นที่จำเป็นต้องได้รับการพิสูจน์อย่างเป็นทางการก็เป็นเรื่องง่ายเช่นกัน แต่กลับพบว่าส่วนอื่นๆ (แม้แต่ฮาร์ดแวร์) มีช่องโหว่ร้ายแรง

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

การตรวจสอบอย่างเป็นทางการ เกิดมาเพื่อความปลอดภัย

ข้อผิดพลาดในโค้ดคอมพิวเตอร์นั้นน่ากลัวมาก

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

เมื่อระบบทั้งหมดนี้ถูกห่อหุ้มด้วยการพิสูจน์แบบไร้ความรู้ ข้อผิดพลาดก็จะยิ่งน่ากลัวมากขึ้น เพราะหากใครสามารถแฮ็กเข้าไปในระบบพิสูจน์แบบไร้ความรู้ได้ พวกเขาก็สามารถถอนเงินทั้งหมดออกมาได้ และเราก็จะไม่รู้ว่าอะไรผิดพลาด (ที่แย่กว่านั้นคือ เราไม่รู้ด้วยซ้ำว่ามันผิดพลาดเมื่อไหร่)

เมื่อเรามีโมเดล AI ที่ทรงพลังอย่างเช่น Claude Mythos ในอีกสองปีข้างหน้า ซึ่งสามารถค้นหาข้อผิดพลาดเหล่านี้ได้โดยอัตโนมัติ ข้อผิดพลาดในโค้ดก็จะยิ่งน่ากลัวมากขึ้นไปอีก

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

คำคมบางส่วน:

ในการเสริมความแข็งแกร่งให้กับระบบ คุณต้องใช้โทเค็นมากกว่าจำนวนโทเค็นที่ผู้โจมตีใช้ในการโจมตีช่องโหว่

และ:

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

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

ที่แย่ไปกว่านั้น บางคนเชื่อว่าทางออกเดียวคือการละทิ้งซอฟต์แวร์โอเพนซอร์ส

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

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

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

ผมไม่เห็นด้วย ผมมองอนาคตของความปลอดภัยทางไซเบอร์ในแง่ดีมากกว่า

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

Mozilla เห็นด้วยกับความคิดเห็นของฉัน นี่คือคำพูดของพวกเขา:

คุณอาจต้องปรับลำดับความสำคัญของทุกสิ่งทุกอย่างใหม่ และทุ่มเทพลังงานอย่างต่อเนื่องและมุ่งมั่นให้กับงานนี้ แต่แสงสว่างอยู่ปลายอุโมงค์แน่นอน

เรารู้สึกภาคภูมิใจอย่างยิ่งที่ทีมของเรากำลังรับมือกับความท้าทายนี้ได้อย่างดีเยี่ยม และคนอื่นๆ ก็จะทำได้เช่นกัน งานของเรายังไม่เสร็จสิ้น แต่เราได้ฝ่าฟันพายุมาได้แล้ว และมองเห็นอนาคตที่ไม่เพียงแต่จะตามทันเท่านั้น แต่ยังดีกว่ามากด้วย

ในที่สุดฝ่ายป้องกันก็มีโอกาสที่จะคว้าชัยชนะอย่างเด็ดขาด... ข้อบกพร่องมีจำกัด และเรากำลังเข้าสู่โลกที่เราสามารถค้นหาข้อบกพร่องทั้งหมดได้ในที่สุด

หากคุณค้นหาคำว่า "formal" และ "verification" ในโพสต์ของ Mozilla โดยใช้ Ctrl+F คุณจะไม่พบผลลัพธ์ใดๆ เลย อนาคตที่ดีของความปลอดภัยทางไซเบอร์ไม่ได้ขึ้นอยู่กับการตรวจสอบอย่างเป็นทางการหรือเทคโนโลยีใดเทคโนโลยีหนึ่งเพียงอย่างเดียว

มันขึ้นอยู่กับอะไร? โดยพื้นฐานแล้วก็คือแผนภูมินี้:

แนวโน้มของช่องโหว่ CVE เมื่อเวลาผ่านไป

ตลอดหลายทศวรรษที่ผ่านมา เทคโนโลยีมากมายได้มีส่วนช่วยลดจำนวนช่องโหว่ลง:

ระบบประเภท

ภาษาที่ปลอดภัยต่อหน่วยความจำ

การปรับปรุงสถาปัตยกรรมซอฟต์แวร์ (รวมถึงแซนด์บ็อกซ์ การควบคุมสิทธิ์ และการแยกแยะ "ฐานการประมวลผลที่เชื่อถือได้" ออกจาก "โค้ดอื่นๆ" อย่างชัดเจนยิ่งขึ้น)

วิธีการทดสอบที่ดีกว่า

ฐานความรู้ที่ขยายตัวอย่างต่อเนื่องเกี่ยวกับรูปแบบการเขียนโค้ดที่ปลอดภัยและไม่ปลอดภัย

จำนวนไลบรารีซอฟต์แวร์ที่เขียนและตรวจสอบแล้วล่วงหน้าเพิ่มมากขึ้น

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

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

STARK เป็นซอฟต์แวร์ที่ซับซ้อนมาก แต่คุณสมบัติด้านความปลอดภัยหลักที่มันนำมาใช้นั้นเข้าใจและกำหนดเป็นรูปแบบได้ง่าย กล่าวคือ หากคุณเห็นแฮช H ชี้ไปยังโปรแกรม P อินพุต x และเอาต์พุต y แสดงว่า (i) อัลกอริทึมแฮชที่ใช้ใน STARK ถูกเจาะแล้ว หรือ (ii) P(x) = y

ดังนั้นเราจึงมีโครงการ Arklib ซึ่งพยายามสร้างการใช้งาน STARK ที่ได้รับการตรวจสอบอย่างเป็นทางการอย่างสมบูรณ์ (ดู VCV-io ซึ่งเป็นโครงสร้างพื้นฐานการคำนวณออราเคิลสำหรับการตรวจสอบอย่างเป็นทางการของโปรโตคอลการเข้ารหัสลับอื่นๆ อีกมากมาย ซึ่งหลายอย่างเป็นส่วนประกอบของ STARK)

ที่ทะเยอทะยานยิ่งกว่านั้นคือ evm-asm: โครงการที่จะสร้างระบบ EVM ที่ได้รับการตรวจสอบอย่างเป็นทางการอย่างสมบูรณ์ทั้งระบบ

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

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

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

อีกสองด้านที่สำคัญได้แก่:

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

ภาษาการเขียนโปรแกรมสัญญาอัจฉริยะ: ดูการตรวจสอบอย่างเป็นทางการใน Vyper และ Verity

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

สำหรับมนุษย์ การคิดวิเคราะห์เกี่ยวกับระบบทั้งหมดตั้งแต่ต้นจนจบนั้นยากเกินไป แต่ระบบตรวจสอบกฎอัตโนมัติสามารถทำได้

การตรวจสอบอย่างเป็นทางการ เกิดขึ้นเพื่อประสิทธิภาพ

ลองมาดู evm-asm กันอีกครั้ง นี่คือการใช้งาน EVM แต่เป็นการใช้งาน EVM ที่เขียนโดยตรงด้วยภาษาแอสเซมบลี RISC-V

แท้จริง.

นี่คือคำสั่ง ADD:

import EvmAsm.Rv64.Program

เนมสเปซ EvmAsm.Evm64

เปิด EvmAsm.Rv64

/-- การบวก EVM 256 บิต: ไบนารี ดึงข้อมูล 2 รายการ ผลักข้อมูล 1 รายการ

แขนขา 0: LD, LD, ADD, SLTU (ถือ), SD (คำสั่ง 5 ข้อ)

แขนขา 1-3: LD, LD, ADD, SLTU (แบก 1), ADD (แบกเข้า), SLTU (แบก 2), OR (แบกออก), SD (อย่างละ 8 ครั้ง)

จากนั้น ADDI sp, sp, 32.

รีจิสเตอร์: x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/

def evm_add : Program :=

-- ส่วนที่ 0 (5 คำสั่ง)

LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;

ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;

-- ส่วนที่ 1 (8 คำสั่ง)

LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;

เพิ่ม .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

เพิ่ม .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

หรือ .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;

-- ส่วนที่ 2 (8 คำแนะนำ)

LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;

เพิ่ม .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

เพิ่ม .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

หรือ .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;

-- ส่วนที่ 3 (8 คำแนะนำ)

LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;

เพิ่ม .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

เพิ่ม .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

หรือ .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;

-- การปรับค่า sp

ADDI .x12 .x12 32

สิ้นสุด EvmAsm.Evm64

เหตุผลที่เลือกใช้ RISC-V ก็เพราะว่าโดยทั่วไปแล้วตัวพิสูจน์ ZK-EVM ที่กำลังสร้างอยู่จะทำงานโดยการพิสูจน์ RISC-V และคอมไพล์ไคลเอ็นต์ Ethereum ไปเป็น RISC-V ดังนั้น หากคุณมีการใช้งาน EVM ที่เขียนโดยตรงใน RISC-V นี่ควรจะเป็นการใช้งานที่เร็วที่สุดที่คุณจะได้รับ

RISC-V สามารถจำลองได้อย่างมีประสิทธิภาพมากบนคอมพิวเตอร์ทั่วไป (และมีแล็ปท็อป RISC-V วางจำหน่ายในตลาด)

แน่นอนว่า เพื่อให้ได้ผลลัพธ์แบบครบวงจรอย่างแท้จริง คุณต้องตรวจสอบการทำงานของ RISC-V เอง (หรือการคำนวณของตัวพิสูจน์) อย่างเป็นทางการ แต่ไม่ต้องกังวลไป เพราะมีงานวิจัยในด้านนี้อยู่แล้ว

การเขียนโค้ดโดยตรงด้วยภาษาแอสเซมบลีเป็นสิ่งที่เราเคยทำเมื่อห้าสิบปีก่อน ตั้งแต่นั้นมา เราได้ละทิ้งวิธีการนี้และหันมาเขียนโค้ดด้วยภาษาโปรแกรมระดับสูงแทน

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

ด้วยการผสานรวมการตรวจสอบอย่างเป็นทางการและปัญญาประดิษฐ์ เราจึงมีโอกาสที่จะ "ย้อนเวลากลับไปสู่อนาคต"

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

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

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

ผู้ใช้สามารถตรวจสอบหลักฐานนั้นได้ (โดยอัตโนมัติ) เพียงครั้งเดียว จากนั้นก็เพียงแค่เรียกใช้เวอร์ชันที่รวดเร็วเท่านั้น

แนวทางนี้ทรงพลังอย่างเหลือเชื่อ และมีเหตุผลที่โยอิจิ ฮิไร เรียกมันว่า "รูปแบบขั้นสุดยอดของการพัฒนาซอฟต์แวร์"

การตรวจสอบอย่างเป็นทางการไม่ใช่ทางออกเดียวที่จะแก้ปัญหาได้ทุกอย่าง

ในสาขาวิทยาการเข้ารหัสลับและวิทยาศาสตร์คอมพิวเตอร์ มีประเพณีที่เก่าแก่เกือบเท่ากับประวัติศาสตร์ของวิธีการเชิงรูปธรรมเอง นั่นคือประเพณีของการวิพากษ์วิจารณ์วิธีการเชิงรูปธรรม (หรือในวงกว้างกว่านั้นคือ การพึ่งพา "การพิสูจน์")

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

ในปี 1979 ราบินได้เสนอฟังก์ชันการเข้ารหัสที่ "พิสูจน์ได้" ว่ามีความปลอดภัยในแง่หนึ่ง ซึ่งหมายความว่ามันมีคุณสมบัติความปลอดภัยแบบลดทอน

คำแถลงด้านความปลอดภัยแบบลดทอนระบุว่า ใครก็ตามที่สามารถค้นหาข้อความ m จากข้อความเข้ารหัส y ได้ จะต้องสามารถแยกตัวประกอบ n ได้ด้วย ... ไม่นานหลังจากที่ Rabin เสนอแผนการเข้ารหัสของเขา Rivest ชี้ให้เห็นว่า ในทางกลับกัน คุณสมบัติที่ให้ความปลอดภัยเพิ่มเติมนี้ จะนำไปสู่การล่มสลายอย่างสมบูรณ์หากเผชิญกับผู้โจมตีที่เรียกว่า "ข้อความเข้ารหัสที่เลือก"

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

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

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

ปัญหา CompCert ข้อที่สองที่เราพบนั้นปรากฏในรูปแบบของบั๊กสองจุดที่นำไปสู่การสร้างโค้ดต่อไปนี้: stwu r1, -44432(r1) ซึ่งมีการจัดสรรเฟรมสแต็ก PowerPC ขนาดใหญ่

ปัญหาคือฟิลด์การเลื่อนตำแหน่ง 16 บิตนั้นเกิดการโอเวอร์โฟลว์ ความหมายของ PPC ที่ CompCert กำหนดไว้ไม่ได้ระบุขีดจำกัดความกว้างของค่าคงที่นี้ โดยสันนิษฐานว่าแอสเซมเบลอร์จะตรวจจับค่าที่อยู่นอกช่วงได้

นอกจากนี้ยังมีบทความฉบับปี 2022 อีกด้วย:

ใน CompCert-KVX การแก้ไขใน commit e2618b31 พบว่าคำสั่ง "nand" ถูกพิมพ์เป็น "and" ซึ่ง "nand" นั้นใช้เฉพาะในรูปแบบ ~ (a & b) ที่พบได้น้อยเท่านั้น ข้อผิดพลาดนี้ถูกค้นพบจากการคอมไพล์โปรแกรมที่สร้างขึ้นแบบสุ่ม

และในวันนี้ ปี 2026 นี่คือวิธีที่ Nadim Kobeissi อธิบายถึงช่องโหว่ในซอฟต์แวร์ที่ได้รับการตรวจสอบอย่างเป็นทางการใน Cryspen:

ในเดือนพฤศจิกายนปี 2025 Filippo Valsorda ได้รายงานอย่างอิสระว่า libcrux-ml-dsa เวอร์ชัน 0.0.3 สร้างคีย์สาธารณะและลายเซ็นที่แตกต่างกันบนแพลตฟอร์มต่างๆ เมื่อใช้ข้อมูลป้อนเข้าแบบกำหนดได้ชุดเดียวกัน

ข้อผิดพลาดดังกล่าวเกิดขึ้นในฟังก์ชันการห่อหุ้มภายใน vxarqu64 ซึ่งใช้การดำเนินการ XAR ในการเรียงสับเปลี่ยน Keccak-f ของ SHA-3 กลไกการสำรองข้อมูลส่งพารามิเตอร์ที่ไม่ถูกต้องไปยังการดำเนินการเลื่อน ทำให้ค่าแฮช SHA-3 เสียหายบนแพลตฟอร์ม ARM64 ที่ไม่มีการรองรับ SHA-3 ในฮาร์ดแวร์

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

และ:

ไลบรารี libcrux-psq ใช้โปรโตคอลคีย์ร่วมก่อนแบบโพสต์ควอนตัม ในเมธอด decrypt_out เส้นทางการถอดรหัส AES-GCM 128 จะเรียกใช้ .unwrap() บนผลลัพธ์การถอดรหัสแทนที่จะส่งต่อข้อผิดพลาด การเข้ารหัสที่ไม่ถูกต้องอาจทำให้กระบวนการล้มเหลวได้

ปัญหาทั้งสี่ข้อนี้จัดอยู่ในสองประเภทต่อไปนี้:

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

กรณีที่ผู้เขียนลืมระบุคุณสมบัติสำคัญที่จำเป็นต้องได้รับการพิสูจน์

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

สุดท้ายนี้ เราสามารถพิจารณาความล้มเหลวของการตรวจสอบอย่างเป็นทางการที่บริเวณรอยต่อระหว่างซอฟต์แวร์และฮาร์ดแวร์ได้ ปัญหาที่พบบ่อยในที่นี้คือการตรวจสอบความต้านทานต่อการโจมตีแบบช่องทางด้านข้าง (side-channel attacks)

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

นี่คือบทความเกี่ยวกับ "การวิเคราะห์กำลังเชิงอนุพันธ์" ซึ่งเป็นตัวอย่างที่เข้าใจกันดีของเทคนิคดังกล่าว: บทความ

การวิเคราะห์กำลังไฟฟ้าเชิงอนุพันธ์เป็นรูปแบบหนึ่งของการโจมตีแบบช่องทางด้านข้างที่พบได้ทั่วไป ที่มา: วิกิพีเดีย

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

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

ดังที่ได้กล่าวไว้ในบทความนี้ ปัญหาทั่วไปอย่างหนึ่งคือการรั่วไหลชั่วคราว: หากคุณสามารถสังเกตสัญญาณที่ขึ้นอยู่กับไม่เพียงแต่ค่า ณ ตำแหน่งใดตำแหน่งหนึ่งเท่านั้น แต่ยังขึ้นอยู่กับการเปลี่ยนแปลงของค่านั้นด้วย ซึ่งมักจะเพียงพอที่จะกู้คืนข้อมูลที่คุณต้องการจากสองค่า (ค่าเก่าและค่าใหม่) แทนที่จะใช้เพียงค่าเดียว

บทความนี้กล่าวถึงการจำแนกประเภทของการรั่วไหลรูปแบบอื่นๆ

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

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

แต่ไม่ว่าคำทางการตลาดจะทำให้การตรวจสอบอย่างเป็นทางการฟังดูเหมือนว่าจะทำให้คุณได้รับ "ความถูกต้องที่พิสูจน์ได้" อย่างไรก็ตาม "ความถูกต้องที่พิสูจน์ได้" นั้นโดยพื้นฐานแล้วไม่ได้พิสูจน์ว่าซอฟต์แวร์ (หรือฮาร์ดแวร์) นั้น "ถูกต้อง"

ตามความเข้าใจของมนุษย์ส่วนใหญ่ คำว่า "ถูกต้อง" หมายถึง "พฤติกรรมของสิ่งต่างๆ สอดคล้องกับความเข้าใจของผู้ใช้เกี่ยวกับเจตนาของผู้พัฒนา"

และคำว่า "ปลอดภัย" หมายถึง "พฤติกรรมของสิ่งต่างๆ ไม่ขัดต่อความคาดหวังของผู้ใช้ และไม่ก่อให้เกิดความเสียหายต่อผลประโยชน์ของผู้ใช้"

ในทั้งสองกรณี ความถูกต้องและความปลอดภัยนั้นขึ้นอยู่กับการเปรียบเทียบระหว่างวัตถุทางคณิตศาสตร์กับเจตนาหรือความคาดหวังของมนุษย์

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

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

ในทางปฏิบัติแล้ว ความคิดและความคาดหวังของเราเปรียบเสมือนกล่องดำ เราเข้าใจความคิดและความคาดหวังของเราได้ก็เพราะแต่ละคนมีประสบการณ์หลายปีในการสังเกตความคิดของตนเองและคาดเดาความคิดของผู้อื่น

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

ดังนั้น "ความถูกต้องที่พิสูจน์ได้" และ "ความปลอดภัยที่พิสูจน์ได้" จึงไม่ได้พิสูจน์ "ความถูกต้อง" และ "ความปลอดภัย" ในแบบที่มนุษย์เราเข้าใจอย่างแท้จริง ไม่มีสิ่งใดทำได้เช่นนั้น เว้นแต่เราจะสามารถจำลองสมองของมนุษย์ได้อย่างสมบูรณ์

แล้วมันมีประโยชน์อย่างไร?

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

โดยพื้นฐานแล้ว วิธีการเหล่านี้เกี่ยวข้องกับการระบุเจตนาของเราซ้ำซ้อนในหลายๆ วิธี จากนั้นจึงตรวจสอบโดยอัตโนมัติว่าข้อกำหนดต่างๆ เหล่านั้นเข้ากันได้หรือไม่

ลองพิจารณาโค้ด Python นี้เป็นตัวอย่าง:

def fib(n: int) -> int:

ถ้า n < 0:

raise Exception("ไม่รองรับค่าลบ")

elif 0 <= n < 2:

ส่งคืน n

อื่น:

คืนค่า fib(n-1) + fib(n-2)

ถ้า __name__ == '__main__':

assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

assert fib(15) == 610

ในส่วนนี้ คุณสามารถแสดงเจตนาของคุณได้สามวิธีที่แตกต่างกัน:

กล่าวคือ โดยการนำสูตรฟิโบนาชี่มาใช้ในโค้ด

โดยปริยาย ผ่านระบบประเภทข้อมูล (ซึ่งระบุว่าอินพุต เอาต์พุต และขั้นตอนกลางในการเรียกซ้ำทั้งหมดเป็นจำนวนเต็ม)

โดยใช้วิธี "ชุดตัวอย่าง": กรณีทดสอบ

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

ระบบประเภทข้อมูลมักเป็นวิธีที่ดีในการตรวจสอบงานในวิชาฟิสิกส์: หากคุณกำลังคำนวณความเร่ง แต่ได้คำตอบเป็นเมตร/วินาที แทนที่จะเป็นเมตร/วินาที² คุณก็รู้ว่าคุณทำผิดพลาดแล้ว

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

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

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

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

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

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

แล้วฉันจะเริ่มต้นได้อย่างไร?

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

/-- ตัวช่วย: การเปรียบเทียบแบบจุดต่อจุด ≤ ที่ระดับ foldl พร้อมตัวสะสม -/

private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (ab : Nat) (hAcc : a ≤ b)

(hLE : Forall₂ (· ≤ ·) ds1 ds2) :

List.foldl (λ acc d => acc * w + d) a ds1 ≤

List.foldl (λ acc d => acc * w + d) b ds2 := by

จับคู่ ds1, ds2, hLE กับ

| [], [], .nil => hAcc ที่แน่นอน

| d1::ds1', d2::ds2', .cons hd htl =>

simp [List.foldl]

refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl

แน่นอน Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

(หากคุณสงสัย นี่เป็นหนึ่งในบทพิสูจน์ย่อยหลายข้อในข้อพิสูจน์ของข้อความความปลอดภัยเฉพาะสำหรับรูปแบบหนึ่งของลายเซ็น SPHINCS)

โดยเฉพาะอย่างยิ่ง ข้อความดังกล่าวคือ: เว้นแต่จะเกิดการชนกันของค่าแฮช ลายเซ็นของข้อความที่สร้างขึ้นจากค่าแฮชไดเจสต์หนึ่ง (dig1) จะต้องมีค่าสูงกว่าอย่างน้อยในบางจุดบนบันไดแฮช เมื่อเทียบกับลายเซ็นของข้อความอื่นใด ดังนั้นจึงมีข้อมูลที่ไม่สามารถคำนวณได้จากลายเซ็นอื่นนั้น)

คุณไม่จำเป็นต้องเขียนโค้ดและพิสูจน์ด้วยตนเอง คุณเพียงแค่ปล่อยให้ AI เขียนโปรแกรมให้คุณ (ไม่ว่าจะโดยตรงในรูปแบบ Lean หรือเพื่อความเร็วในภาษาแอสเซมบลี) และพิสูจน์คุณสมบัติที่ต้องการในกระบวนการนั้น

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

ผลลัพธ์ที่แย่ที่สุดคือ มันหมุนอยู่กับที่โดยไม่คืบหน้า (หรืออย่างที่เครื่องมือ Leanstral ของผมเคยทำ คือ มันแทนที่ข้อความที่ถูกขอให้พิสูจน์เพื่อลดภาระงาน)

สุดท้ายแล้ว สิ่งเดียวที่คุณต้องตรวจสอบคือว่าข้อสรุปที่ได้นั้นตรงตามความต้องการของคุณหรือไม่

ในกรณีของรูปแบบลายเซ็น SPHINCS ข้อความสุดท้ายมีดังนี้:

ทฤษฎีบท wots_fullDigits_incomparable

{dig1 dig2 : List Nat} {w l1 l2 : Nat}

(hw : 0 < w)

(hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)

(hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)

(hL2suff : l1 * (w - 1) < w ^ l2)

(hNeq : dig1 ≠ dig2) :

¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧

¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

นี่แทบจะอ่านไม่ออกเลยจริงๆ:

หากตัวเลขที่ได้จากการคำนวณแฮชไดเจสต์ครั้งหนึ่ง (dig1) ไม่เท่ากับตัวเลขที่ได้จากการคำนวณแฮชไดเจสต์อีกครั้งหนึ่ง (dig2)

ดังนั้นเงื่อนไขสองข้อต่อไปนี้จึงไม่เป็นจริง:

สำหรับตัวเลขทั้งหมด ตัวเลขจาก dig1 ≤ ตัวเลขจาก dig2

สำหรับตัวเลขทั้งหมด ตัวเลขจาก dig2 ≤ ตัวเลขจาก dig1

ใน "ตัวเลขที่ขยายแล้ว" (wotsFullDigits) ที่สร้างขึ้นโดยการบวกค่าตรวจสอบความถูกต้อง นั่นคือ ในส่วนขยายของ dig1 จะมีบางจุดที่ตัวเลขสูงกว่า ในขณะที่ในจุดอื่นๆ ตัวเลขในส่วนขยายของ dig2 จะสูงกว่าอย่างหลีกเลี่ยงไม่ได้

ในแง่ของการใช้โมเดลภาษาขนาดใหญ่ในการเขียนพิสูจน์ ผมพบว่าทั้ง Claude และ Deepseek 4 Pro ต่างก็มีความสามารถ ส่วน Leanstral เป็นโมเดลถ่วงน้ำหนักแบบโอเพนซอร์สขนาดเล็กกว่า ที่ได้รับการปรับแต่งมาเป็นพิเศษเพื่อการเขียน Lean และเป็นอีกทางเลือกที่น่าสนใจ

โมเดลนี้มีพารามิเตอร์ 119 พันล้านตัว โดยแต่ละโทเค็นจะเปิดใช้งาน 6 พันล้านตัว และสามารถรันได้ในเครื่องของคุณเอง แม้ว่าจะช้ากว่า (ประมาณ 15 โทเค็นต่อวินาทีบนแล็ปท็อปของผม) จากผลการทดสอบประสิทธิภาพ Leanstral มีประสิทธิภาพเหนือกว่าโมเดลทั่วไปขนาดใหญ่หลายตัว:

จากประสบการณ์ส่วนตัวของผมในปัจจุบัน ประสิทธิภาพของมันอาจด้อยกว่า Deepseek 4 Pro เล็กน้อย แต่ก็ยังคงมีประสิทธิภาพมากอยู่ดี

การตรวจสอบอย่างเป็นทางการไม่สามารถแก้ปัญหาทั้งหมดของเราได้

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

การตรวจสอบเอกสารอย่างเป็นทางการโดยใช้ AI ช่วยให้เราก้าวไปอีกขั้นในการบรรลุเป้าหมายนี้

เช่นเดียวกับบล็อกเชนและ ZK-SNARK ปัญญาประดิษฐ์และการตรวจสอบอย่างเป็นทางการก็เป็นเทคโนโลยีที่ส่งเสริมซึ่งกันและกันอย่างมากเช่นกัน

เทคโนโลยีบล็อกเชนช่วยให้คุณตรวจสอบได้อย่างเปิดเผยและต้านทานการเซ็นเซอร์ได้ แต่ต้องแลกมาด้วยความเป็นส่วนตัวและความสามารถในการขยายขนาด ในขณะที่ ZK-SNARK คืนความเป็นส่วนตัวและความสามารถในการขยายขนาดให้กับคุณ (ที่จริงแล้ว มากกว่าที่คุณเคยมีมาก่อนด้วยซ้ำ)

ปัญญาประดิษฐ์ทำให้คุณสามารถเขียนโค้ดได้มากมาย แต่ต้องแลกมาด้วยความแม่นยำที่ลดลง ในขณะที่การตรวจสอบอย่างเป็นทางการจะคืนความแม่นยำให้กับคุณ (ที่จริงแล้ว อาจแม่นยำกว่าที่คุณเคยมีมาก่อนด้วยซ้ำ)

โดยปกติแล้ว AI จะสร้างโค้ดที่เร่งรีบมากเกินไปเป็นจำนวนมาก และจำนวนข้อผิดพลาดก็จะเพิ่มขึ้น

อันที่จริง ในบางกรณี การยอมให้มีจำนวนข้อผิดพลาดเพิ่มขึ้นบ้างก็ถือเป็นการแลกเปลี่ยนที่ถูกต้องแล้ว เพราะหากข้อผิดพลาดเหล่านั้นเล็กน้อย ซอฟต์แวร์ที่มีข้อผิดพลาดก็ยังดีกว่าไม่มีซอฟต์แวร์เลยด้วยซ้ำ

แต่ในที่นี้ ความปลอดภัยทางไซเบอร์มีอนาคตที่สดใส: ซอฟต์แวร์จะ (ยังคง) แบ่งออกเป็น "ส่วนขอบที่ไม่ปลอดภัย" รอบ "แกนหลักที่ปลอดภัย"

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

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

เมื่อพูดถึงส่วนแกนหลักที่ปลอดภัย เราไม่สามารถปล่อยให้โค้ดที่มีข้อผิดพลาดแพร่กระจายได้ เราจะดำเนินการอย่างเด็ดขาดเพื่อรักษาขนาดของแกนหลักที่ปลอดภัยให้เล็ก และอาจลดขนาดลงไปอีก

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

ส่วนหลักของระบบปฏิบัติการ (หรืออย่างน้อยก็บางส่วนของมัน) จะกลายเป็นแกนหลักที่มีความปลอดภัยสูง

Ethereum ก็จะเป็นอีกหนึ่งตัวอย่าง

หวังว่า อย่างน้อยที่สุด สำหรับการคำนวณที่ไม่ต้องการประสิทธิภาพสูงมากนัก ฮาร์ดแวร์ที่คุณใช้จะกลายเป็นปัจจัยที่สาม

ระบบที่เกี่ยวข้องกับอินเทอร์เน็ตของสรรพสิ่ง (IoT) จะเป็นระบบที่สี่

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

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