Typing High-Speed Cryptography against Spectre v1.
该论文针对密码学软件中的瞬态执行攻击（尤其是Spectre v1）提出了一种基于类型系统的方法，以确保推测性常数时间（Speculative Constant-Time），从而在保持高性能的同时为密码实现提供形式化保证。当前密码库的黄金标准
#形式化验证
共收录 3 条相关情报。
← 返回所有主题EOSAFE: Security Analysis of EOSIO Smart Contracts.
本论文提出 EOSAFE，一个针对 EOSIO 智能合约的自动化安全分析框架。EOSIO 是一种新兴的区块链平台，其智能合约使用 C++ 编写，且具有独特的通信模型和资源管理机制，导致传统分析工具难以直接应用。EOSAFE 结合了静态分析和
The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware
该论文是系列正式验证分析掩码NTT（数论变换）硬件安全性论文的第7篇，针对后量子密码（PQC）硬件中的侧信道泄漏问题。论文证明了在任意深度k级流水线中，采用新鲜中间掩码和每级PF-PINI(≤2)小工具（gadgets）的掩码NTT实现，每