基于通道通信的分离内核的信息流安全性推理
软件工程
2015-10-20 v1 密码学与安全
摘要
在分离内核的安全认证中，通过形式化方法保证信息流安全性是强制要求的。作为分离内核的工业标准，ARINC 653已被主流分离内核所遵循。因此，ARINC 653中定义的功能的安全性对于分离内核的开发和认证非常重要。本文提出了首个对具有ARINC 653基于通道通信的分离内核进行形式化规约与验证的工作。我们在Isabelle/HOL中提供了可复用的分离内核形式化规约和安全证明。在对信息流安全性进行推理的过程中，我们发现了ARINC 653标准中的一些安全缺陷，这些缺陷可能导致信息泄露，并在我们的规约中对其进行了修复。我们还在两个开源的符合ARINC 653的分离内核中验证了这些安全缺陷的存在。
引用
@article{arxiv.1510.05091,
title = {Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication},
author = {Yongwang Zhao and David Sann and Fuyuan Zhang and Yang Liu},
journal= {arXiv preprint arXiv:1510.05091},
year = {2015}
}
备注
17 pages, 4 figures