COVERN: A Logic for Compositional Verification of Information Flow Control
COVERN: A Logic for Compositional Verification of Information Flow Control
复制标题
COVERN：信息流控制的组合验证逻辑
DOI：
10.1109/eurosp.2018.00010
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Kai Engelhardt
中科院分区：
文献类型：
--
作者：
Toby C. Murray;Robert Sison;Kai Engelhardt
共享内存并发在现代编程中普遍存在，包括必须保护高度敏感数据的系统。最近，验证最终成为证明真实程序的有趣安全属性，尤其是信息流控制（IFC）安全性的实用工具。然而，尚无通用逻辑来验证共享内存并发程序的IFC安全性。在本文中，我们介绍了第一个这样的逻辑，Covern（非干预的组成验证）及其通过一般依赖依据的新通用框架IFC推理的新通用框架证明。我们将COVERN应用于建模并验证跨域桌面复合器的安全性关键软件功能，这是一种嵌入式设备，可促进与多个分类网络的同时且直观的用户交互，同时防止它们之间泄漏。据我们所知，这是文献中非平凡的共享记忆并发程序的IFC安全性的第一个基础，由机器检查的证明。
Shared memory concurrency is pervasive in modern programming, including in systems that must protect highly sensitive data. Recently, verification has finally emerged as a practical tool for proving interesting security properties of real programs, particularly information flow control (IFC) security. Yet there remain no general logics for verifying IFC security of shared-memory concurrent programs. In this paper we present the first such logic, COVERN (Compositional Verification of Noninterference) and its proof of soundness via a new generic framework for general rely-guarantee IFC reasoning. We apply COVERN to model and verify the security-critical software functionality of the Cross Domain Desktop Compositor, an embedded device that facilitates simultaneous and intuitive user interaction with multiple classified networks while preventing leakage between them. To our knowledge this is the first foundational, machine-checked proof of IFC security for a non-trivial shared-memory concurrent program in the literature.
CoSMeDis：具有正式验证的保密保证的分布式社交媒体平台
DOI：
10.1109/sp.2017.24
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Bauereiss T
通讯作者：
Bauereiss T
CoSMed：经过保密验证的社交媒体平台
DOI：
10.1007/s10817-017-9443-3
发表时间：
2017
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Bauereiß T
通讯作者：
Bauereiß T