论文标题
机械化的非干预逐渐安全性
Mechanized Noninterference for Gradual Security
论文作者
论文摘要
本文介绍了对具有逐渐信息流控制的语言的第一个机器检查的证据，从而为安全编程语言建立了坚实的基础，从而使程序员在运行时与编译时执行之间进行了选择。一路上，我们在文献中的一个非干预证明中发现了一个缺陷，并为主要引理之一提供了反例。本文研究的特定语言，$λ_{\ mathtt {sec}}}^\ star $，基于Azevedo de Amorim等人的胶质语言。 [2020]。为了使设计更容易被其他研究人员访问，本文贡献了该语言的第一个传统语义，也就是说，我们将汇编从$λ_ {\ Mathtt {sec}}}^\ star $转换为铸造的castculus，并设计了后者的简化语义，包括责备跟踪。除了非干预证明外，我们还将机械化类型安全性，确定性和汇编的证明保留了类型。
This paper presents the first machine-checked proof of noninterference for a language with gradual information-flow control, thereby establishing a rock solid foundation for secure programming languages that give programmers the choice between runtime versus compile-time enforcement. Along the way we uncovered a flaw in one of the noninterference proofs in the literature, and give a counterexample for one of the main lemmas. The particular language studied in this paper, $λ_{\mathtt{SEC}}^\star$, is based on the GLIO language of Azevedo de Amorim et al. [2020]. To make the design more accessible to other researchers, this paper contributes the first traditional semantics for the language, that is, we define compilation from $λ_{\mathtt{SEC}}^\star$ to a cast calculus and design a reduction semantics for the latter that includes blame tracking. In addition to the proof of noninterference, we also mechanize proofs of type safety, determinism, and that compilation preserves types.
