Exploiting and Securing Docker containers and Kubernetes pods from a MitM attack
该论文聚焦容器化环境（Docker 容器与 Kubernetes Pod）中的中间人（MitM）攻击防护问题。作者指出，容器内工作负载与传统非容器环境一样面临钓鱼、应用层漏洞利用与网络入侵等威胁，但由于容器网络叠加层、服务网格、动态调度与多
#formal-verification
共收录 95 条相关情报。
← 返回所有主题Analyzing Multi-Factor Authentication Through Cryptographic Security Properties
该论文聚焦于现代身份认证体系中的多因素认证（MFA）平台，试图用密码学安全属性的形式化视角来审视其安全性，而不是依赖经验性的渗透测试或厂商自述。研究背景是：认证系统从早期的单一机制（用户名/口令、物理令牌、生物特征）逐步演变为把多种机制组合
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
本文提出了一套面向密码学软件的全新形式化验证方法论，其核心取向是直接验证“生产级代码”，而不是为了便于验证而专门改写代码。作者选择 Rust 作为目标语言，看重的是它在性能与系统集成方面的优势：Rust 的所有权机制使 Aeneas 工具链
Efficient Branch-and-Bound Testing and Verification of zkVMs
零知识虚拟机（zkVM）通过把虚拟机语义翻译成执行轨迹上的代数约束，使通用程序能够被可验证地执行。这些约束的正确性至关重要：一条错误的约束可能使系统处于欠约束（under-constrained）状态，从而接受伪造的证明；也可能因过约束（o
On Identifying Sound Conditions for Frontrunning Resistance
该论文研究区块链智能合约中的抢跑（frontrunning）攻击与抗抢跑性质的形式化定义问题。背景上，智能合约通过共识执行，但交易排序本质上是异步的：交易由矿工（或验证者）决定打包、排序与延迟。由于用户必须通过交易与合约交互，掌握排序权的节
Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning
该论文关注现代语义丰富系统与应用中的“应用逻辑漏洞”（application logic flaws）。这类漏洞与业务语义和威胁模型深度绑定，难以通过传统的模糊测试或静态分析规模化发现：真实系统往往包含多样的应用特性、复杂的协议逻辑与领域专
CertiFlash: A Formal Verification Framework for Flash Translation Layers in Computational Solid State Drives
该论文聚焦于以存储为中心的计算（storage-centric computing）场景下固态硬盘（SSD）固件——闪存转换层（FTL）——的安全与正确性问题。研究背景是：数据密集型应用需要把大量数据从存储搬运到计算单元，产生显著的数据移动
Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits
本文研究的是零知识机器学习（ZKML）电路中的「冗余检查」问题及其可证明安全的去膨胀（debloating）技术。背景是：面向神经网络推理的零知识证明系统会把模型编译成大规模算术约束系统，其中包含大量范围证明、符号查找（sign looku
AutoTrans: AI-Assisted Automatic Translation of Security Assertions for RISC-V Processors
该论文聚焦 RISC-V 处理器硬件安全验证中的一大效率瓶颈：把一组已在某个处理器目标上通过验证的安全断言（security assertions）复用到另一个 RISC-V 核上。这一过程目前主要依靠人工完成，单条断言的翻译往往要耗费数小
Dependency-Aware ROM/CBD Correctness Bounds for ML-KEM-768 at the Heuristic Failure Scale
该论文研究 ML-KEM-768（即 FIPS 203 标准化的 Kyber 密钥封装）在诚实解封装条件下失败概率上界的严格认证问题。ML-KEM 的安全性论证长期依赖一个启发式结论：解封装失败率约为 2^-164 量级，但近期的形式化评估
FoldNTT: A Multiplier- and Twiddle-Lean NTT Core with Formally Verified Arithmetic for Proth Primes
在后量子密码学中，基于格的方案（如Falcon/FN-DSA）需要高效的数论变换（NTT）硬件实现，而传统NTT核心的模乘器和旋转因子存储占用了大量芯片面积。本文提出FoldNTT，对TCHES 2022发布的radix-2 CFNTT加速
Scratchy: Visual-Scratchpad Multimodal Reasoning for Cryptographic Proof Generation in EasyCrypt
该论文提出了一种名为 Scratchy 的视觉暂存器多模态推理方法，旨在解决大语言模型（LLM）在生成密码学形式化证明时面临的结构性依赖难题。在密码学领域，计算安全性论证要求证明必须协调概率、对抗游戏、不变量、假设和界限等要素，而 Easy
A Non-Formulable Theorem: A Fundamental Limit of Finite Syntactic Systems and Its Consequences for Security and AI
该论文提出并证明了一个元定理：对于任何一致且具有足够表达能力的有限句法系统S，必然存在至少一个该定理无法自主产生的定理。所谓“有限句法系统”涵盖形式逻辑系统、形式验证器、安全机制、AI系统、法律与经济模型等所有基于有限规则和符号生成机制的体
Compositional Verification of Composite Byzantine Protocols.
拜占庭容错（BFT）协议是分布式系统中最难设计和推理的组件之一。近年来，形式化验证领域发展出多种计算机辅助方法，能够对独立（standalone）BFT 协议的安全性与活性进行自动化验证；与此同时，分布式计算社区也尝试将复杂协议拆分为更简单
Griotte: Verified Compartmentalisation via Capabilities
本文提出 Griotte 和 Griotte OS，这是对 CHERIoT 硬件能力机器与 CHERIoT RTOS 的抽象化但忠实的建模，旨在为 CHERIoT 的分区隔离（compartmentalisation）安全保证提供形式化验证
Towards Formal Verification of State Continuity for Enclave Programs.
本文面向可信执行环境（TEE）中飞地程序的安全性问题，特别是状态连续性（State Continuity）的验证，提出了一种形式化验证方法。状态连续性指飞地程序在执行过程中，即使遭遇异常中断、迁移或恶意系统软件干扰，其内部状态仍能保持一致和
Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence
该论文针对安全代币（Security Tokens）标准中监管操作语义不明确的问题，提出了一种机械化（machine-checked）的参考执行语义。安全代币标准通常暴露特权转移、冻结、恢复和合规机制，但机制本身并不标识其执行的法律效果或附
ARMOR: A Formally Verified Implementation of X.509 Certificate Chain Validation.
本文提出了 ARMOR，这是首个针对 X.509 证书链验证逻辑（CCVL）的大规模形式化验证实现，旨在为 RFC 5280 的大部分内容提供机器可检查的正确性保证。ARMOR 的设计目标有两个：一是作为 RFC 规范的形式化、机器可检查的
Less is more: refinement proofs for probabilistic proofs.
本文提出一个名为 Distiller 的通用框架，旨在优化概率证明系统（包括交互式证明 IP、简洁非交互式论证 SNARK、概率可检验证明 PCP 等）的前端开销。在过去十年中，概率证明的实现虽受广泛关注，但由于前端需要将抽象计算转换为等价
Finding Specification Blind Spots via Fuzz Testing.
该论文针对形式化验证程序中的一个关键盲区：即便程序通过了形式化验证，其正确性仍受限于规范（SPEC）的完整性。若规范本身存在漏洞或不完整，验证结果将失去意义。作者提出了一种名为 Fast（Fuzzing-Assisted Specifica