AdaCore 用 AI 生成并验证 SPARK 密码学实现
热点事件持续更新
AdaCore 用 AI 生成并验证 SPARK 密码学实现
1 篇报道1 个报道来源58 分钟前更新
先了解这件事
AI 综述
AdaCore 称借助前沿 AI 自动生成了 AES（128/192/256）、SHA-256 和 HMAC-SHA-256 的 SPARK 形式化规范与实现，达到 SPARK Platinum 级完整功能正确性，全程无需人工直接干预。 但 AdaCore 明确表示，在安全真正重要的场景中不要使用这些代码；该工作完全未涉及侧信道攻击这类非功能属性。此外，SAW 证明需要 GNAT Pro 27 与 LLVM 后端，GitHub 仓库的 CI 因缺少该环境而不运行这些证明。
AI 根据报道生成 · 45 分钟前更新
最新进展10月28日 21:23
AdaCore 用 AI 在 SPARK 中完成 AES、SHA-256 与 HMAC 的形式化验证报道时间线
沿着报道，了解事件的不同侧面。
10月28日
- Hacker NewsAdaCore 用 AI 在 SPARK 中完成 AES、SHA-256 与 HMAC 的形式化验证
AdaCore 借助前沿 AI 自动生成 AES（128/192/256）、SHA-256 和 HMAC-SHA-256 的 SPARK 形式化规范与实现，达到 SPARK Platinum 级完整功能正确性，全程无需人工直接干预。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。