XiaoMi-AI文件搜索系统
World File Search System源程序
snip：编译器转换的投机执行和非干预保存
我们解决了在投机语义下在编译器转换之间保留非干预的问题。我们开发了一种证明方法，以确保在所有源程序中均匀保存。我们证明方法的基础是一种新的模拟关系形式。它通过指令进行操作，该指令对攻击者对微构造状态的控制进行建模，并且它解释了编译器转换可能会改变微构造状态对执行（以及指令）的影响。使用我们的证明方法，我们显示了消除死亡代码的正确性。当我们试图证明注册分配正确时，我们确定了以前未知的弱点，该弱点会引入非干预。我们已经证实了libsodium密码库中代码上主流编译器的弱点。为了再次获得安全性，我们开发了一种新颖的静态分析，该分析可在源程序和寄存器分配程序的产品上运行。使用分析，我们向现有的注册分配实现提供了一个自动修复程序。我们通过证明方法证明了固定寄存器分配的正确性。
FSLH：灵活的机械化投机载荷硬化
摘要 - 幽灵投机侧通道攻击构成了计算机系统安全的巨大威胁。研究表明，使用选择性载荷硬化（SLH）的选择性变体可以有效地保护密码恒定时间代码。slh还不够强大，无法保护非晶型代码，从而引入了Ultimate SLH，该代码为任意程序提供了保护，但对于一般使用的开销太大，因为它保守地假定所有数据都是秘密的。在本文中，我们引入了一个灵活的SLH概念，该概念通过正式概括选择性和最终的SLH来实现两全其美。我们为保护任意程序的此类转换提供了适当的安全定义：运行猜测的任何转换程序都不会泄漏源程序依次泄漏。我们正式证明使用ROCQ权METER证明两个灵活的SLH变体强制执行此相对安全保证。作为简单的推论，我们还获得了最终的SLH执行我们的相对安全性概念，还可以使Value SLH的选择性变体和地址SLH执行投机性恒定时间安全性。关键字 - 侧通道攻击，投机执行，规格，安全汇编，投机负载硬化，投机性恒定时间，相对安全性，正式验证，ROCQ，COQ