渐进安全的机械化非干扰
摘要：对具有渐进信息流控制的语言进行的非干扰性的首个机器验证证明，为给程序员提供运行时与编译时执行选择的安全编程语言奠定了坚实基础。在此过程中，我们发现了文献中一个非干扰性证明的错误，并给出了一个主要引理的反例。本文研究的特定语言$lambda\_{mathtt{SEC}}^star$基于Azevedo de Amorim等人的GLIO语言[2020]。为使该设计对其他研究人员更易于理解，本文首次提出了该语言的传统语义，即我们定义了从$lambda\_{mathtt{SEC}}^star$到一个强制转型演算的编译，并设计了后者的简化语义，其中包括归责跟踪。除了非干扰性证明之外，我们还机械化证明了类型安全性、确定性以及编译的类型保持性。
作者：Tianyu Chen and Jeremy G. Siek
论文ID：2211.15745
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-11-30