验证编译器保持并发值依赖信息流安全性

通过推理源代码来证明程序不泄露敏感数据是一种常见做法。但这样做在推理与现实之间留下了一个缺口，只有考虑编译器的行为才能填补。当程序实施值依赖信息流安全属性（其中位置的分类可随其他位置中的值而变化）时，该任务变得复杂，而当程序利用共享变量并发时则更为复杂。先前工作已形式化定义了保持值依赖安全属性的并发感知精化概念。然而，该概念比编译器语义保持验证中通常应用的标准精化定义要复杂得多。迄今为止仍不清楚它是否能应用于现实编译器，因为不存在将其分解为更小的、更熟悉的证明义务的通用分解原则。在本工作中，我们提供这样一种分解原则，并展示其几乎能将证明安全精化的复杂性减半。此外，我们通过在 Isabelle/HOL 中证明一个从命令式 While 语言到通用 RISC 风格汇编语言的概念验证编译器对带有由锁原语中介的共享内存并发的程序保持值依赖安全性，展示了其对安全编译的适用性。最后，我们在 Isabelle 中于 Cross Domain Desktop Compositor 的 While 语言模型上执行我们的编译器，据我们所知展示了首次将编译器验证结果用于将信息流安全属性下达到一个非平凡并发程序的汇编级模型。