亞馬遜近期推出了一款名為Mlkem-native的后量子密碼學方案，該方案基于C語言實現，兼具高保障性和高性能特點。這一創新成果將ML-KEM標準的參考實現與前沿研究優化及形式化驗證技術相結合，為云計算環境下的數據安全提供了全新解決方案。
在開發過程中，團隊采用了CBMC和SLOTHY等自動化工具構建安全防線。這些工具通過數學方法驗證代碼的內存安全性、類型安全性及功能正確性，使開發人員能夠在確保絕對安全的前提下進行深度匯編優化。這種"安全優先"的開發模式有效避免了傳統優化過程中可能引入的安全漏洞，實現了性能與安全性的雙重保障。
性能測試數據顯示，Mlkem-native在不同規格的EC2實例上均展現出顯著優勢。其每秒操作數較ML-KEM原始實現提升2.0至2.4倍，這種提升在保持代碼可維護性的同時實現，特別適用于需要處理海量加密請求的云計算場景。對于云服務提供商而言，這意味著可以在不增加硬件投入的情況下，將系統加密性能提升至新高度。
該方案的推出恰逢量子計算技術快速發展之際。傳統加密算法在量子計算機面前面臨被破解的風險，而ML-KEM作為NIST標準化的抗量子密碼算法，其高效實現具有戰略意義。亞馬遜通過Mlkem-native為AWS等云平臺構建了量子時代的防御體系，確保用戶數據在量子計算普及后仍能保持安全。
技術專家指出，Mlkem-native的創新不僅體現在性能突破上，更在于其開發范式的革新。通過將形式化驗證與性能優化深度融合，該方案為后量子密碼學的工程化實踐樹立了新標桿。這種開發模式有望推動更多抗量子算法從理論走向實際應用，加速全球密碼基礎設施的升級進程。
目前，亞馬遜已將Mlkem-native的核心代碼開源，供全球安全社區審查驗證。這一舉措不僅體現了對技術透明度的追求，也為其他開發者提供了參考范本。隨著量子計算威脅的日益臨近，此類經過嚴格驗證的高效實現將成為保障數字世界安全的關鍵基礎設施。
