มีการประกาศว่าแผนริเริ่มการแทนที่การใช้งาน Python ของอัลกอริทึมการเข้ารหัสที่นำเสนอในโมดูล hashlib และ hmac ด้วยเวอร์ชันที่ได้รับการพิสูจน์ทางคณิตศาสตร์ซึ่งเตรียมไว้โดยโครงการ HACL* เสร็จสมบูรณ์เรียบร้อยแล้ว การทำงานในการสลับไปใช้ฟังก์ชันที่มีการพิสูจน์ความน่าเชื่อถือทางคณิตศาสตร์ได้ดำเนินการอย่างต่อเนื่องตั้งแต่ปี 2022 และเริ่มต้นหลังจากการค้นพบบัฟเฟอร์โอเวอร์โฟลว์ในการใช้งานอัลกอริทึม SHA3 ที่ใช้ในโมดูล hashlib ของ Python
ที่เก็บข้อมูลหลักของโครงการ CPython ยอมรับโค้ดที่มีการใช้งานฟังก์ชันแฮชการเข้ารหัสและอัลกอริทึม HMAC (กลไกการตรวจสอบข้อความ) ใหม่ ฟังก์ชันแฮชเริ่มต้นและ HMAC ที่มีให้ใน Python ทั้งหมดได้ถูกแทนที่ด้วยตัวแปรที่ตรวจยืนยันแล้ว นอกจากนี้ ยังมีการเพิ่มการใช้งาน HMAC-BLAKE2 ซึ่งใช้คำสั่ง AVX2 SIMD เพื่อเร่งความเร็วการคำนวณ คาดว่าโค้ดที่ตรวจสอบแล้วจะรวมอยู่ใน Python 3.14 รุ่นฤดูใบไม้ร่วง
การใช้งานใหม่ของฟังก์ชันการเข้ารหัสนั้นพอร์ตมาจากไลบรารี HACL* ซึ่งกำลังได้รับการพัฒนาโดยนักวิจัยจากสถาบันวิจัยเทคโนโลยีสารสนเทศและระบบอัตโนมัติแห่งชาติของฝรั่งเศส (INRIA) ซึ่งเป็นแผนกหนึ่งของ Microsoft Research และมหาวิทยาลัยคาร์เนกีเมลลอน ไลบรารี HACL* รองรับฟังก์ชันการเข้ารหัสทั่วไปที่เพียงพอสำหรับ TLS 1.3 และรองรับ API ของ NaCl (ไลบรารีเครือข่ายและการเข้ารหัส) อย่างเต็มรูปแบบ เช่น Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, SHA-3, HMAC และ HKDF ในด้านประสิทธิภาพการทำงาน ไลบรารี HACL* นั้นใกล้เคียงกับ OpenSSL แต่ต่างจาก OpenSSL ตรงที่ให้การรับประกันเพิ่มเติมด้านความน่าเชื่อถือและความปลอดภัย
โค้ด HACL* เขียนด้วยชุดย่อยของภาษาฟังก์ชัน F* ซึ่งจัดให้มีระบบของประเภทที่ขึ้นอยู่กับตัวแปรและการปรับแต่งที่ช่วยให้สามารถระบุข้อมูลจำเพาะที่แม่นยำ (แบบจำลองทางคณิตศาสตร์) และรับประกันว่าการใช้งานจะไม่มีข้อผิดพลาดโดยใช้สูตร SMT และเครื่องมือพิสูจน์เสริม โค้ดอ้างอิง F* จะถูกแปลเป็นโค้ด C โดยใช้คอมไพเลอร์ KaRaMeL และพร้อมสำหรับการบูรณาการกับโปรเจ็กต์อื่นๆ
การดำเนินการตรวจสอบเกี่ยวข้องกับการกำหนดข้อกำหนดโดยละเอียดที่อธิบายพฤติกรรมที่เป็นไปได้ทั้งหมดของโปรแกรม และการสร้างหลักฐานทางคณิตศาสตร์ว่าโค้ดที่เขียนนั้นสอดคล้องกับข้อกำหนดที่เตรียมไว้อย่างครบถ้วน การตรวจสอบช่วยให้มั่นใจได้ว่าโปรแกรมจะทำงานตามที่นักพัฒนาตั้งใจไว้เท่านั้น และไม่มีข้อผิดพลาดบางประเภท เช่น บัฟเฟอร์ล้น การยกเลิกการอ้างอิงตัวชี้ การเข้าถึงพื้นที่หน่วยความจำที่ได้รับการปลดปล่อยแล้ว หรือการปล่อยซ้ำสองครั้ง กระบวนการคอมไพล์จะช่วยให้แน่ใจว่ามีการตรวจสอบประเภทและค่าอย่างเคร่งครัด ซึ่งส่วนประกอบหนึ่งจะไม่ส่งพารามิเตอร์ไปยังส่วนประกอบอื่นที่ไม่ตรงกับข้อกำหนด และจะไม่สามารถเข้าถึงสถานะภายในของส่วนประกอบอื่นได้
กระบวนการเปลี่ยนไปใช้รหัสที่ได้รับการตรวจสอบใช้เวลาสองปีครึ่ง และต้องมีการพัฒนาไลบรารี HACL* ซึ่งมีการขยายฟังก์ชันการทำงานด้วยความสามารถที่จำเป็นสำหรับการแทนที่ฟังก์ชันการทำงานที่มีอยู่ของ hashlib อย่างโปร่งใส ตัวอย่างเช่น HACL* ได้เพิ่มการสนับสนุนสำหรับโหมดสตรีมมิ่งของการดำเนินการ HMAC, ให้โหมดการดำเนินการเพิ่มเติมสำหรับอัลกอริทึม Blake2, นำ API ใหม่สำหรับ SHA3 มาใช้ซึ่งครอบคลุมอัลกอริทึมตระกูล Keccak ทุกรูปแบบ, ให้วิธีการแจ้งเตือนข้อผิดพลาดที่จำเป็น (เช่น ในกรณีที่มีปัญหาในการจัดสรรหน่วยความจำ) และพัฒนาสคริปต์สำหรับการทำอัตโนมัติในการถ่ายโอนเวอร์ชันใหม่ของ HACL* ไปยังที่เก็บ Python
ที่มา: opennet.ru
