การแนะนำ
ความปลอดภัยของ Bitcoin และบล็อกเชนอื่น ๆ เช่น Liquid ขึ้นอยู่กับการใช้อัลกอริธึมลายเซ็นดิจิทัล เช่น ลายเซ็น ECDSA และ Schnorr ไลบรารี AC ชื่อ libsecp256k1 ซึ่งตั้งชื่อตามเส้นโค้งวงรีที่ไลบรารีทำงานนั้น ถูกใช้โดยทั้ง Bitcoin Core และ Liquid เพื่อจัดเตรียมอัลกอริธึมลายเซ็นดิจิทัลเหล่านี้ อัลกอริธึมเหล่านี้ใช้การคำนวณทางคณิตศาสตร์ที่เรียกว่าก ผกผันแบบโมดูลาร์ซึ่งเป็นส่วนประกอบที่ค่อนข้างแพงในการคำนวณ
ใน “การคำนวณ gcd ในเวลาคงที่ที่รวดเร็วและการผกผันแบบโมดูลาร์” Daniel J. Bernstein และ Bo-Yin Yang พัฒนาอัลกอริธึมการผกผันแบบโมดูลาร์ใหม่ ในปี 2021 อัลกอริทึมนี้เรียกว่า “safegcd” ดำเนินการ สำหรับ libsecp256k1 โดย Peter Dettman ในฐานะส่วนหนึ่งของกระบวนการตรวจสอบอัลกอริธึมใหม่นี้ Blockstream Analysis เป็นคนแรกที่ดำเนินการ a การตรวจสอบอย่างเป็นทางการ ของการออกแบบอัลกอริธึมโดยใช้ตัวช่วยพิสูจน์ Coq เพื่อตรวจสอบอย่างเป็นทางการว่าอัลกอริธึมยุติจริงด้วยผลลัพธ์การผกผันโมดูลาร์ที่ถูกต้องบนอินพุต 256 บิต
ช่องว่างระหว่างอัลกอริทึมและการนำไปใช้
ความพยายามในการเตรียมการอย่างเป็นทางการในปี 2021 แสดงให้เห็นเพียงว่าอัลกอริทึมที่ออกแบบโดยเบิร์นสไตน์และหยางทำงานได้อย่างถูกต้อง อย่างไรก็ตาม การใช้อัลกอริทึมนั้นใน libsecp256k1 จำเป็นต้องมีการนำคำอธิบายทางคณิตศาสตร์ของอัลกอริทึม safegcd ไปใช้งานภายในภาษาการเขียนโปรแกรม C ตัวอย่างเช่น คำอธิบายทางคณิตศาสตร์ของอัลกอริธึมจะทำการคูณเมทริกซ์ของเวกเตอร์ที่สามารถกว้างได้ถึงจำนวนเต็มที่มีเครื่องหมาย 256 บิต อย่างไรก็ตาม ภาษาการเขียนโปรแกรม C จะให้จำนวนเต็มดั้งเดิมสูงสุด 64 บิตเท่านั้น (หรือ 128 บิตที่มีนามสกุลบางภาษา)
การใช้อัลกอริทึม safegcd จำเป็นต้องมีการเขียนโปรแกรมการคูณเมทริกซ์และการคำนวณอื่นๆ โดยใช้จำนวนเต็ม 64 บิตของ C นอกจากนี้ การเพิ่มประสิทธิภาพอื่น ๆ อีกมากมาย ได้รับการเพิ่มเพื่อให้การดำเนินการรวดเร็ว ในท้ายที่สุด มีการใช้งานอัลกอริธึม safegcd ใน libsecp256k1 สี่แบบแยกกัน: อัลกอริธึมเวลาคงที่สองอัลกอริธึมสำหรับการสร้างลายเซ็น หนึ่งอัลกอริธึมปรับให้เหมาะสมสำหรับระบบ 32 บิต และหนึ่งอัลกอริธึมปรับให้เหมาะสมสำหรับระบบ 64 บิต และอัลกอริธึมเวลาแปรผันสองอัลกอริธึมสำหรับการตรวจสอบลายเซ็นอีกครั้ง หนึ่งอันสำหรับระบบ 32 บิตและอีกอันสำหรับระบบ 64 บิต
ตรวจสอบได้ C
เพื่อตรวจสอบว่าโค้ด C ใช้งานอัลกอริธึม safegcd อย่างถูกต้อง จะต้องตรวจสอบรายละเอียดการใช้งานทั้งหมด เราใช้ ตรวจสอบได้ Cซึ่งเป็นส่วนหนึ่งของ Verified Software program Toolchain สำหรับการให้เหตุผลเกี่ยวกับโค้ด C โดยใช้ตัวพิสูจน์ทฤษฎีบท Coq
การตรวจสอบจะดำเนินการโดยการระบุเงื่อนไขเบื้องต้นและเงื่อนไขภายหลังโดยใช้ตรรกะการแยกสำหรับทุกฟังก์ชันที่อยู่ระหว่างการตรวจสอบ ตรรกะการแยก เป็นตรรกะเฉพาะสำหรับการให้เหตุผลเกี่ยวกับรูทีนย่อย การจัดสรรหน่วยความจำ การทำงานพร้อมกัน และอื่นๆ
เมื่อแต่ละฟังก์ชันได้รับข้อกำหนดเฉพาะแล้ว การตรวจสอบจะดำเนินการโดยเริ่มต้นจากเงื่อนไขเบื้องต้นของฟังก์ชัน และสร้างค่าคงที่ใหม่หลังจากแต่ละคำสั่งในเนื้อความของฟังก์ชัน จนกระทั่งสร้างเงื่อนไขหลังที่ส่วนท้ายของส่วนฟังก์ชันหรือส่วนท้ายของฟังก์ชันแต่ละรายการในที่สุด คำสั่งส่งคืน ความพยายามในการจัดรูปแบบส่วนใหญ่จะใช้เวลา “ระหว่าง” บรรทัดของโค้ด โดยใช้ค่าคงที่เพื่อแปลการดำเนินการดิบของนิพจน์ C แต่ละรายการเป็นคำสั่งระดับที่สูงกว่าเกี่ยวกับสิ่งที่โครงสร้างข้อมูลที่ถูกจัดการเป็นตัวแทนทางคณิตศาสตร์ ตัวอย่างเช่น สิ่งที่ภาษา C ถือว่าเป็นอาร์เรย์ของจำนวนเต็ม 64 บิต จริงๆ แล้วอาจเป็นการแสดงจำนวนเต็ม 256 บิต
ผลลัพธ์สุดท้ายก็คือ หลักฐานที่เป็นทางการซึ่งตรวจสอบโดยผู้ช่วยพิสูจน์ Coq ว่าการใช้งานเวลาแปรผัน 64 บิตของ libsecp256k1 ของอัลกอริธึมผกผันโมดูลาร์ safegcd นั้นทำงานได้ถูกต้อง
ข้อจำกัดของการตรวจสอบ
มีข้อจำกัดบางประการในการพิสูจน์ความถูกต้องของฟังก์ชัน ตรรกะการแยกที่ใช้ใน Verifiable C จะใช้สิ่งที่เรียกว่า ความถูกต้องบางส่วน– นั่นหมายความว่าจะพิสูจน์เฉพาะรหัส C ที่ส่งคืนพร้อมกับผลลัพธ์ที่ถูกต้องเท่านั้น ถ้า มันกลับมา แต่มันไม่ได้พิสูจน์ว่าการยุตินั้นเอง เราลดข้อจำกัดนี้โดยใช้ หลักฐาน Coq ก่อนหน้าของเรา ของขอบเขตบนอัลกอริธึม safegcd เพื่อพิสูจน์ว่าค่าตัวนับลูปของลูปหลักในความเป็นจริงจะไม่เกิน 11 รอบ
อีกประเด็นหนึ่งคือภาษา C เองไม่มีข้อกำหนดที่เป็นทางการ โปรเจ็กต์ Verifiable C ใช้ โครงการคอมไพเลอร์ CompCert เพื่อให้ข้อกำหนดอย่างเป็นทางการของภาษา C สิ่งนี้รับประกันว่าเมื่อโปรแกรม C ที่ตรวจสอบแล้วถูกคอมไพล์ด้วยคอมไพเลอร์ CompCert รหัสแอสเซมบลีที่ได้จะเป็นไปตามข้อกำหนด (ภายใต้ข้อจำกัดข้างต้น) อย่างไรก็ตาม นี่ไม่ได้รับประกันว่าโค้ดที่สร้างโดย GCC, clang หรือคอมไพเลอร์อื่นๆ จะใช้งานได้ ตัวอย่างเช่น คอมไพเลอร์ภาษาซีได้รับอนุญาตให้มีลำดับการประเมินที่แตกต่างกันสำหรับอาร์กิวเมนต์ภายในการเรียกใช้ฟังก์ชัน และแม้ว่าภาษา C จะมีข้อกำหนดที่เป็นทางการก็ตาม คอมไพเลอร์ที่ไม่ได้รับการรับรองอย่างเป็นทางการก็ยังสามารถคอมไพล์โปรแกรมผิดได้ นี้ทำ เกิดขึ้น ในทางปฏิบัติ
สุดท้าย Verifiable C ไม่รองรับการส่งผ่านโครงสร้าง การส่งคืนโครงสร้าง หรือการกำหนดโครงสร้าง ในขณะที่อยู่ใน libsecp256k1 โครงสร้างจะถูกส่งผ่านโดยตัวชี้เสมอ (ซึ่งได้รับอนุญาตใน Verifiable C) มีบางครั้งที่มีการใช้การกำหนดโครงสร้าง สำหรับการพิสูจน์ความถูกต้องผกผันแบบโมดูลาร์ มีการกำหนด 3 แบบที่ต้องแทนที่ด้วยการเรียกฟังก์ชันพิเศษที่ดำเนินการกำหนดโครงสร้างแบบฟิลด์ต่อฟิลด์
สรุป
Blockstream Analysis ได้ตรวจสอบความถูกต้องของฟังก์ชันผกผันแบบโมดูลาร์ของ libsecp256k1 อย่างเป็นทางการ งานนี้ให้หลักฐานเพิ่มเติมว่าการตรวจสอบรหัส C เป็นไปได้ในทางปฏิบัติ การใช้ตัวช่วยพิสูจน์วัตถุประสงค์ทั่วไปช่วยให้เราสามารถตรวจสอบซอฟต์แวร์ที่สร้างขึ้นจากข้อโต้แย้งทางคณิตศาสตร์ที่ซับซ้อน
ไม่มีสิ่งใดขัดขวางฟังก์ชันที่เหลือที่ใช้ใน libsecp256k1 จากการตรวจสอบเช่นกัน ดังนั้นจึงเป็นไปได้ที่ libsecp256k1 จะได้รับการรับประกันความถูกต้องของซอฟต์แวร์สูงสุดที่เป็นไปได้
นี่คือแขกโพสต์โดย Russell O’Connor และ Andrew Poelstra ความคิดเห็นที่แสดงออกนั้นเป็นความคิดเห็นของตนเองทั้งหมด และไม่จำเป็นต้องสะท้อนถึงความคิดเห็นของ BTC Inc หรือ Bitcoin Journal
