该论文聚焦于分布式信息物理系统（如物联网、自动驾驶汽车）的安全建模与验证问题。传统建模方法在面对动态成员和复杂交互时变得笨重且不实用，例如多车交互场景中车辆相对位置和车道变化带来的挑战。为此，作者提出了一种以自我为中心的抽象方法，用于简洁地建模任意数量代理围绕一个自我代理的局部交互。这种模型抽象掉其他代理的详细行为，并忽略存在但物理上远离的代理。论文展示了该方法能够捕捉自动驾驶汽车责任敏感安全（RSS）框架中的有趣场景。作为分析示例，作者利用以自我为中心的模型证明了多个高速公路驾驶场景的安全性，证明过程中凸显了经典验证方法——归纳不变断言的力量。最后讨论了该分析方法向其他场景和应用的推广可能性。论文主要贡献在于提出了一种新颖的建模抽象，降低了分布式系统安全验证的复杂性，并通过自动驾驶案例验证了其有效性。适合研究形式化方法、系统安全验证以及自动驾驶安全的研究人员和工程师阅读。

本文针对密码系统侧信道攻击的掩码防御机制，提出了一种基于概率分离逻辑的形式化验证方法，用于自动验证掩码算法的非干扰性安全属性。作者首先建立了非干扰性与条件独立性之间的数学联系，从而将安全验证问题转化为条件独立性推理问题。随后，利用现有的Lilac分离逻辑框架（该框架专用于条件独立性推理）来执行验证，并设计了一系列新的证明规则，以支持探测安全性的高效验证。通过若干示例算法，论文展示了该方法能够有效验证典型掩码方案的安全性，同时相比传统手工证明或模型检验方法，降低了误判风险。该工作主要面向密码学实现者、安全验证工具开发者以及侧信道防御研究者，其核心贡献在于为掩码算法的形式化安全验证提供了更简洁、可自动化的理论框架。

该论文研究了认证数据结构（Authenticated Data Structures）的形式化验证问题。认证数据结构允许不可信的第三方执行操作并生成可验证操作输出的证明，但这类数据结构的正确实现具有挑战性。本文提出了一种基于关系分离逻辑（relational separation logic）的新方法，用于对使用抗碰撞哈希函数的程序进行推理。作者利用该逻辑构建了类型系统的两个语义模型，从而证明了自动生成认证数据结构的库在安全性和正确性方面的性质。此外，论文还验证了该库的若干优化，并展示了如何将优化的手写认证数据结构实现与自动生成的代码安全地链接。所有结果均在Coq证明助手中使用Iris框架进行了机械化。该工作为认证数据结构的可靠实现提供了理论基础，适合对形式化验证、程序逻辑和密码学协议感兴趣的研究人员阅读。

论文提出了一种混合形式化验证方法，结合高层演绎推理和电路级推理，用于高度优化的加密汇编代码。该方法在 EasyCrypt 证明助手中扩展实现，通过使用等价性检查将安全保障传播到同一计算的不同优化或不同架构的实现中，从而降低低级别函数的证明工作量，并分摊证明开销。论文以 ML-KEM（一种后量子密码算法）在 Jasmin 中的形式化验证实现为例，首次获得了在 x86-64 架构上性能与最快非验证实现相当的形式化验证实现。这证明了混合方法在兼顾性能与安全性方面的有效性。研究背景在于现有形式化验证方法在处理深度优化汇编代码时面临可扩展性挑战，而本文结合两种推理范式，利用电路级推理处理底层优化细节，利用演绎推理处理高层语义，显著提升了验证效率。实验结果表明，该方法能够在保持高性能的同时实现形式化安全保障，适合对密码学实现安全性和正确性有高要求的场景。

本论文针对后量子密码（PQC）硬件实现中的掩码Barrett reduction的侧信道泄漏问题，提出首个通用且机器验证的基数界限——1-Bit Barrier。Barrett reduction是基于NTT的PQC实现（如ML-KEM、ML-DSA）的非线性核心，但现有组合框架（ISW、t-SNI、PINI、DOM）仅针对GF(2)上的布尔掩码，无法直接应用于素域上的算术掩码。作者基于此前系列工作（QANARY、partial-NTT-masking margins、代数基础、蝴蝶组合），填补了这一空白。核心贡献在于：1）证明对于任意模数q>0和移位s，Barrett内部导线映射f_x(m) = ((x + 2^s - m) mod 2^s) mod q的原像基数属于{0,1,2}，绝不超过2——这一性质被称为1-Bit Barrier，意味着每条内部导线最多泄露1比特的最小熵；实际泄漏通常更少，因为计数为0的情况（不可达输出值）使界更为保守。2）引入PF-PINI（素域PINI）概念，证明Barrett满足PF-PINI(2)，Cooley-Tukey蝶形运算满足PF-PINI(1)，并观察到在阶段间加入新鲜掩码时，组合管线的最大原像基数为max(k1, k2)，因此1-Bit Barrier可传播。3）在Lean 4（Mathlib）中完成了12条定理的机器验证，无一个“sorry”，结果对所有q>0通用。4）指出Adams Bridge因缺少阶段间新鲜掩码而违反PF-PINI组合，解释了此前发现漏洞的原因。该工作为NIST IR 8547推荐的形式化方法在PQC实现验证中提供了首个通用机器验证的基数界，并给出1比特泄漏的直观解释。适合侧信道分析、PQC硬件安全、形式化验证领域的研究者和工程师阅读。