蘋果OS新推出的基礎密碼學程式庫內建兩種量子安全演算法，並推出形式驗證工具
來源: iThome | 日期: 2026-05-27 | URL: https://www.ithome.com.tw/news/176143
核心重點
蘋果 SEAR 團隊與硬體技術正式驗證團隊合作，發布：
- 新版基礎密碼學程式庫 corecrypto（開源）
- 自建形式驗證（Formal Verification）程式庫與工具
量子安全演算法
- 實作兩種後量子演算法：ML-KEM、ML-DSA
- 符合美國聯邦標準：FIPS 203（ML-KEM）、FIPS 204（ML-DSA）
- 附數學證明供專家獨立評估
部署時間軸
| 時間 | 行動 |
|---|---|
| 2024年 | corecrypto 加入後量子加密 |
| 已部署 | iMessage、VPN、TLS 網路連線 |
| 2025年秋季 | Apple CryptoKit 內含量子安全 API |
效能與安全性最佳化
- 套用數學最佳化提升效能（不變更底層演算法）
- 利用蘋果晶片特性：DIT（資料獨立計時）、PAC（指標認證）
- 目標：防止時序旁路攻擊
形式驗證工具（4種開源工具）
| 工具 | 用途 |
|---|---|
| Isabelle | 驗證複雜數學證明 |
| SAW（Software Analysis Workbench） | 形式驗證軟體程式屬性 |
| Cryptol | 與 SAW 搭配的形式語言 |
| cryptol-to-isabelle | 將 Cryptol 演算法模型轉換為 Isabelle 公式 |
背景動機
蘋果積極致力於避免再度發生業界早期部署橢圓曲線密碼學的問題。ML-KEM/ML-DSA 屬近年新興數學，業界安全實作經驗仍有限，形式驗證為自行設計以因應多語言支援、快速程式碼演化等需求。
衍生頁面
- 蘋果corecrypto後量子密碼學程式庫與形式驗證工具發布 — 核心概念頁
- apple — Apple 公司頁