蘋果OS新推出的基礎密碼學程式庫內建兩種量子安全演算法，並推出形式驗證工具

在此同時，為了提升關鍵軟體安全保障，使其達到最先進的水準，蘋果也發布自行建立的形式驗證（formal verification）程式庫與工具，可針對任何廣泛部署的相關演算法實作，提供已知最強的正確性驗證結果。

為了及早因應未來的量子電腦帶來的加密遭破解威脅，蘋果2024年在corecrypto加入後量子加密，並持續在最有可能發揮作用的領域當中，例如涉及通訊與其他敏感資訊加密處理的應用，像是iMessage、VPN、TLS網路連線，率先開發與部署強力的量子安全密碼學技術；此外，2025年秋季蘋果發布的Apple CryptoKit，也內含多種支援量子安全機制的API，開發者得以在他們的應用程式當中，採用具有量子安全特性的加密與身分驗證技術。

而在審閱ML-KEM與ML-DSA設計附帶的實作後，蘋果確認當中有顯著的改善空間，他們套用數學最佳化的處理，即可在不需變更底層演算法的狀況下，增進效能，也謹慎改寫對效能與安全性影響相當敏感的子程序，以便充分利用蘋果的處理器硬體特性，像是資料獨立計時（Data Independent Timing，DIT），以及指標認證（Pointer Authentication，PAC）。基於他們對於蘋果晶片的專業知識，透過這些經過手動最佳化的做法，也使他們能精準控制處理器的行為，進而預防可能將機密暴露的時序旁路攻擊（timing side channels）。

由於ML-KEM與ML-DSA背後的數學原理是近年才出現的，在實際產品中，IT業界以安全方式實作這些演算法的集體經驗仍很有限，蘋果表示，他們積極致力於避免再度發生業界早期部署橢圓曲線密碼學的問題，當時因為其中存在隱晦且易遭利用的漏洞，而阻礙這類技術的普及。

為了因應支援多種語言、快速程式碼演化，以及使用現有開發者工具等多種需求，蘋果最終自行設計了形式驗證方法。他們結合原本使用的工具與新工具，並實現自上而下的驗證，範圍橫跨針對ML-KEM與ML-DSA訂定的FIPS規範與最終實作。

在這次發表的消息中，蘋果介紹4種用於形式化驗證的開放原始碼工具，分別是：驗證複雜數學證明的Isabelle、形式驗證軟體程式屬性的Software Analysis Workbench（SAW）、與SAW搭配的形式語言Cryptol、將Cryptol演算法模型轉換為Isabelle公式的cryptol-to-isabelle。