- อัลกอริทึมแฮชพื้นฐานและ HMAC ของ Python ถูกแทนที่ด้วย โค้ดเข้ารหัสลับที่ผ่านการพิสูจน์แล้ว อย่าง HACL* แล้ว
- มีการผสาน โค้ดภาษา C ราว 15,000 บรรทัด จาก HACL* เข้าสู่โค้ดเบสของ Python โดยอัตโนมัติ
- มีการออกแบบและพิสูจน์ความถูกต้องของ Streaming API แบบทั่วไป เพื่อรองรับบล็อกอัลกอริทึมที่หลากหลาย
- รองรับประเด็นวิศวกรรมขั้นสูง เช่น การจัดการความล้มเหลวของการจัดสรรหน่วยความจำ, การแก้ปัญหาการคอมไพล์ AVX2, และ การปรับแต่งสภาพแวดล้อม CI
- ความร่วมมือระหว่างชุมชน Python และชุมชนคริปโตช่วยให้ได้ทั้งความปลอดภัยและความสามารถในการบำรุงรักษาในทางปฏิบัติ
Python นำโค้ดตรวจสอบความถูกต้องของอัลกอริทึมเข้ารหัสลับมาใช้เต็มรูปแบบ
- หลังจากเกิด CVE-2022-37454 ที่เกี่ยวข้องกับการใช้งาน SHA3 ในปี 2022 ก็มีการตั้งประเด็นว่า Python ควรเปลี่ยนโครงสร้างพื้นฐานด้านแฮชไปใช้โค้ดที่ผ่านการพิสูจน์แล้ว
- ตลอดระยะเวลา 2 ปีครึ่งหลังจากนั้น Python ได้แทนที่อัลกอริทึมแฮชและ HMAC ที่มีมาให้ในระบบทั้งหมดด้วยอิมพลีเมนเทชันที่ผ่านการพิสูจน์แล้วบนพื้นฐานของ HACL*
- การเปลี่ยนแปลงนี้เกิดขึ้นแบบ โปร่งใสต่อผู้ใช้ทั้งหมด และไม่มีการสูญเสียความสามารถในการใช้งาน
- HACL* ยังเพิ่มความสามารถที่ Python ต้องการเข้ามาอีก เช่น โหมดต่าง ๆ ของ Blake2, API สำหรับรองรับ Keccak รูปแบบแปรผันของ SHA3, และการปรับแต่งประสิทธิภาพการสตรีมของ HMAC
- การนำเวอร์ชันใหม่เข้ามาใช้นั้น ทำงานอัตโนมัติผ่านสคริปต์ ทำให้ดูแลรักษาได้ง่าย
ทำความเข้าใจ Streaming API
- อัลกอริทึมเข้ารหัสลับส่วนใหญ่เป็น บล็อกอัลกอริทึม ซึ่งต้องประมวลผลอินพุตเป็นหน่วยบล็อก
- แต่ในสภาพแวดล้อมการใช้งานจริง มักป้อนข้อมูลเป็นหน่วยบล็อกได้ยาก จึงจำเป็นต้องมี Streaming API
- Streaming API ทำงานได้โดยไม่ขึ้นกับความยาวของอินพุต และยังสามารถดึงผลลัพธ์ระหว่างทางได้
- การทำอิมพลีเมนเทชันแบบสตรีมต้องจัดการสถานะที่ซับซ้อน และอิมพลีเมนเทชัน SHA3 ก่อนหน้านี้เคยมี ช่องโหว่ด้านความปลอดภัยร้ายแรง ที่เกี่ยวข้องกับเรื่องนี้
- แฮชอัลกอริทึมแต่ละตัวมีวิธีประมวลผลต่างกัน ทำให้ความซับซ้อนเพิ่มขึ้น เช่น Blake2 ไม่ยอมรับบล็อกว่าง, HMAC สามารถลบคีย์ได้หลังจากเริ่มต้นค่าแล้ว เป็นต้น
การพิสูจน์ความถูกต้องของอัลกอริทึมสตรีมแบบทั่วไป
- แนวทางที่นำเสนอในงานวิจัยเมื่อปี 2021 คือ ทำ abstraction ของบล็อกอัลกอริทึม แล้วนิยามอัลกอริทึมสตรีมแบบทั่วไปไว้บนชั้นนั้น
- จากนั้นจึง นำไปใช้เหมือนเทมเพลต กับอัลกอริทึมแต่ละชนิด ทำให้สามารถนำกลับมาใช้ซ้ำได้
- มีการทำให้เป็นแบบทั่วไปโดยครอบคลุมเงื่อนไขพิเศษที่หลากหลายทั้งหมด:
- สามารถกำหนดความยาวผลลัพธ์ได้หรือไม่ (SHA3 vs Shake)
- ต้องมีอินพุตก่อนการประมวลผลหรือไม่ (เช่น บล็อกคีย์ของ Blake2)
- ความแตกต่างของวิธีจัดการบล็อกสุดท้าย
- ข้อมูลเพิ่มเติมที่ต้องเก็บไว้ในสถานะภายใน
- วิธีคัดลอกสถานะเพื่อดึงผลลัพธ์ระหว่างทาง (stack vs heap)
- กลยุทธ์การใช้ API แบบแยกตามอัลกอริทึมหรือแบบ family API
สร้างความมั่นคงของการบิลด์เพื่อการรวมเข้ากับ Python
- CI ของ Python ตรวจสอบกับ ทูลเชนและสถาปัตยกรรมมากกว่า 50 แบบ ทำให้แม้ปัญหาเล็กน้อยก็ถูกเปิดเผย
- ระหว่างการทำ HMAC implementation พบปัญหาเรื่องการรองรับคำสั่ง AVX2:
- คอมไพเลอร์บางตัวไม่สามารถจัดการเฮดเดอร์
immintrin.h ได้หากไม่มี AVX2
- เพื่อแก้ปัญหานี้จึงใช้ แพตเทิร์น abstract struct ของภาษา C
- เนื่องจากมีความต่างระหว่าง แนวคิด abstraction ใน C กับโค้ดภาษา C ที่สร้างจาก F* จึงต้องเพิ่มฟีเจอร์วิเคราะห์ visibility อย่างละเอียดให้กับคอมไพเลอร์
krml
การรับมือกับความล้มเหลวของการจัดสรรหน่วยความจำ
- โมเดล F* เดิมสามารถจำลองความล้มเหลวของหน่วยความจำได้ในทางทฤษฎีอยู่แล้ว แต่ครั้งนี้เป็นการนำไปใช้จริงเป็นครั้งแรก
- ตามข้อกำหนดของ Python จึงมีการปรับปรุงให้โครงสร้างสถานะ นิยามอัลกอริทึม และโครงสร้างการสตรีมทั้งหมด สามารถส่งต่อความล้มเหลวของการจัดสรรได้
- ใน F* ใช้ชนิด
option และเมื่อคอมไพล์เป็น C จะกลายเป็น tagged union
- ในอนาคตอาจเปลี่ยนไปใช้ วิธี runtime failure flag เพื่อลดความซับซ้อน
การทำให้การอัปเดตโค้ดของ HACL* เป็นอัตโนมัติ
- PR แรกของ Python ใช้
sed เพื่อลบนิยามเฮดเดอร์ที่ไม่จำเป็น ปรับพาธ และงานลักษณะใกล้เคียงกัน
- หลังจากยืนยันได้ว่าโค้ด HACL* มีเสถียรภาพแล้ว
sed ที่ซับซ้อนก็ถูกถอดออก และแทนที่ด้วย สคริปต์แบบเรียบง่าย
- เมื่อใช้สคริปต์นี้ ทุกคนก็สามารถ อัปเดตโค้ด HACL* เป็นเวอร์ชันล่าสุดในซอร์สทรีของ Python ได้อย่างง่ายดาย
บทสรุป
- โค้ดเข้ารหัสลับที่ผ่านการพิสูจน์แล้วถูกรวมเข้ากับ Python ซึ่งเป็น สภาพแวดล้อมโปรดักชันตัวแทนสำคัญ ได้สำเร็จ
- นี่เป็นกรณีตัวอย่างที่พิสูจน์ว่าเทคโนโลยีนี้ไม่ได้หยุดอยู่แค่ในระดับงานวิจัยเชิงวิชาการ แต่ ใช้งานได้จริงและบำรุงรักษาได้ ในซอฟต์แวร์จริง
- ยังเป็นตัวอย่างที่ดีของความร่วมมือระหว่างชุมชน Python กับนักพัฒนา HACL* และอาจส่งอิทธิพลต่อโครงการอื่นในอนาคต
2 ความคิดเห็น
อย่างที่มีการกล่าวถึงในความเห็นบน Hacker News เช่นกัน มันยากที่จะเข้าใจว่าระบบนิเวศของ Python ได้บรรลุอะไรบางอย่างที่ "ก้าวข้ามขั้นการวิจัยเชิงวิชาการไปสู่สิ่งที่ใช้งานได้จริงและบำรุงรักษาได้ในซอฟต์แวร์จริง" กันแน่
ถ้าสิ่งที่อยากจะพูดคือมีการทำงานเพื่อทำให้อัลกอริทึมแบบสตรีมมิงเป็นนามธรรมเหนือโครงสร้างพื้นฐานแฮชเดิมที่ยังไม่ได้รับการตรวจพิสูจน์ แบบนี้ก็คงเป็นแค่การเล่นคำสไตล์ "Pythonic" อีกครั้งเท่านั้น
ความคิดเห็นจาก Hacker News
ไม่ได้ระบุเวอร์ชันของ Python ไว้ จากที่ตรวจดู ฟีเจอร์นี้มีกำหนดจะรวมในเวอร์ชัน 3.14 คงยังไม่ได้เห็นจนกว่าจะถึงเดือนตุลาคม
ได้นำไลบรารี C ที่ผ่านการพิสูจน์ความถูกต้องซึ่งสร้างจาก F* ของ Microsoft มาใส่ใน CPython และเขียน C extension ขึ้นมา
สงสัยว่าจะรองรับเอาต์พุตแบบ "streaming" ของ SHAKE ด้วยหรือไม่
การเข้ารหัสสมัยใหม่ที่ใช้งานกันอย่างแพร่หลายแทบจะเจาะไม่ได้ในทางปฏิบัติ และสงครามคริปโตในยุค 90 ตอนนี้ก็ดูค่อนข้างล้าสมัยไปแล้ว สงสัยว่ามีใครมีความเห็นเกี่ยวกับผลกระทบของเรื่องนี้ต่อสังคมหรือไม่
สงสัยว่าเฟรมเวิร์กการพิสูจน์ความถูกต้องแบบสตรีมมิงทั่วไปจะนำกลับมาใช้ซ้ำกับอย่างอื่นนอกเหนือจาก cryptographic hash ได้มากแค่ไหน
สงสัยว่าทุกอย่างที่ import โมดูลเข้ารหัสนี้จะต้องมี G++ หรืออย่างอื่นรวมมาด้วยหรือไม่ หรือมันถูกคอมไพล์เข้าไปในตัว CPython เอง
ไม่ค่อยรู้อะไรเกี่ยวกับการเข้ารหัสนัก สงสัยว่านี่มีความหมายอย่างไรสำหรับ Python
สงสัยว่าส่วนไหนของการพัฒนาที่ได้รับการพิสูจน์ความถูกต้องแล้วบ้าง และมันครอบคลุมอะไรบ้าง
จำนวนบรรทัดของโค้ดเป็นตัวชี้วัดที่ไม่เหมาะสมอย่างมาก โดยเฉพาะยิ่งในบริบทของโค้ดเข้ารหัส เมื่อมีการโอ้อวดตัวเลขที่มาก