基于精化的隔离内核规约与安全分析
软件工程
2017-02-21 v1 密码学与安全
摘要
在隔离内核的安全认证中，形式化方法对信息流安全的保证是强制要求的。作为提升安全性的工业标准，主流隔离内核均已遵循 ARINC 653。由于将安全与安保功能集成到单一隔离内核的新趋势，对 ARINC 653 的安全分析以及带有安全证明的形式化规约，对于开发和认证符合 ARINC 653 的隔离内核（ARINC SKs）具有重要意义。本文提出一种基于精化的 ARINC SKs 规约开发与安全分析方法。我们提出一个通用安全模型和逐步精化框架。通过精化开发了两级功能规约。对 ARINC 653 中隔离内核需求的主要部分进行了建模，例如内核初始化、两级调度、分区与进程管理以及分区间通信。形式化规约及其安全证明在 Isabelle/HOL 定理证明器中完成。我们根据形式化规约审查了一个工业级和两个开源 ARINC SK 实现（即 VxWorks 653、XtratuM 和 POK）的源代码。在验证和代码审查过程中，在 ARINC 653 标准和实现中发现了六个可能导致信息泄露的安全缺陷。
引用
@article{arxiv.1702.05997,
title = {Refinement-based Specification and Security Analysis of Separation Kernels},
author = {Yongwang Zhao and David Sanan and Fuyuan Zhang and Yang Liu},
journal= {arXiv preprint arXiv:1702.05997},
year = {2017}
}
备注
manuscript of accepted paper by IEEE Transactions on Dependable and Secure Computing