Compositional Non-Interference for Fine-Grained Concurrent Programs
Compositional Non-Interference for Fine-Grained Concurrent Programs
复制标题
细粒度并发程序的组合互不干扰
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
L. Birkedal
中科院分区：
文献类型：
--
作者：
D. Frumin;Robbert Krebbers;L. Birkedal
互不干扰是确保信息不会泄露的程序属性。在编程语言的上下文中，有两种常见的方法来建立互不干涉：类型系统和程序逻辑。类型系统提供了强大的自动化(通过类型检查)，但它们在支持的程序类型上受到固有的限制。程序逻辑支持具有挑战性的程序，但它们通常需要大量的人工帮助，并且不能处理模块或高阶程序。为了将这两种方法联系起来，我们提出了SeLoC-一种无干扰的分离逻辑，并在其基础上使用逻辑关系技术构建了类型系统。通过在分离逻辑之上构建类型系统，我们可以从成分上验证由类型化和非类型化部分组成的程序。前一部分通过类型检查进行验证，后一部分通过手动验证进行验证。SeLoC的核心技术贡献是一种最弱前提的关系形式，可以利用分离的逻辑资源跟踪信息流。SeLoC完全经过机器检查，并且构建在用于Coq中的并发分离逻辑的IRIS框架之上。与IRIS的集成提供了对细粒度并发的无缝支持，这超出了现有类型系统和程序逻辑的无干扰能力范围。
Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing non-interference: type systems and program logics. Type systems provide strong automation (by means of type checking), but they are inherently restrictive in the kind of programs they support. Program logics support challenging programs, but they typically require significant human assistance, and cannot handle modules or higher-order programs.To connect these two approaches, we present SeLoC—a separation logic for non-interference, on top of which we build a type system using the technique of logical relations. By building a type system on top of separation logic, we can compositionally verify programs that consist of typed and untyped parts. The former parts are verified through type checking, while the latter parts are verified through manual proof.The core technical contribution of SeLoC is a relational form of weakest preconditions that can track information flow using separation logic resources. SeLoC is fully machine-checked, and built on top of the Iris framework for concurrent separation logic in Coq. The integration with Iris provides seamless support for fine-grained concurrency, which was beyond the reach of prior type systems and program logics for non-interference.
信息流控制的类型：标记粒度和语义模型
DOI：
10.1109/csf.2018.00024
发表时间：
2018
期刊：
2018 IEEE 31st Computer Security Foundations Symposium (CSF)
影响因子：
--
作者：
Vineet Rajani;Deepak Garg
通讯作者：
Deepak Garg