A survey on formal specification and verification of separation kernels

被引：8
作者：
Zhao, Yongwang [1 ]
Yang, Zhibin [1 ,2 ,3 ]
Ma, Dianfu [1 ]
机构：
[1] Beihang Univ, Sch Comp Sci & Engn, State Key Lab Software Dev Environm NLSDE, Beijing 100191, Peoples R China
[2] Nanjing Univ Aeronaut & Astronaut, Coll Comp Sci & Technol, Nanjing 210016, Jiangsu, Peoples R China
[3] Collaborat Innovat Ctr Novel Software Technol & I, Nanjing 210016, Jiangsu, Peoples R China
来源：
FRONTIERS OF COMPUTER SCIENCE | 2017年 / 11卷 / 04期
基金：
中国国家自然科学基金;
关键词：
real-time operating systems; separation kernel; survey; formal specification; formal verification; SECURITY; SOFTWARE; DECOMPOSITION;
D O I：
10.1007/s11704-016-4226-2
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Separation kernels are fundamental software of safety and security-critical systems, which provide their hosted applications with spatial and temporal separation as well as controlled information flows among partitions. The application of separation kernels in critical domain demands the correctness of the kernel by formal verification. To the best of our knowledge, there is no survey paper on this topic. This paper presents an overview of formal specification and verification of separation kernels. We first present the background including the concept of separation kernel and the comparisons among different kernels. Then, we survey the state of the art on this topic since 2000. Finally, we summarize research work by detailed comparison and discussion.
引用
收藏
页码：585 / 607
页数：23
相关论文
共 97 条
  • [1] Abrial J. -R., 2006, 28th International Conference on Software Engineering Proceedings, P761, DOI 10.1145/1134285.1134406
  • [2] Abrial J. R., 1980, On the construction of programs, P343
  • [3] Abrial J.R., 1996, B BOOK ASSIGNING PRO
  • [4] Abrial JR, 2007, FUND INFORM, V77, P1
  • [5] Alves-foss J, 2004, P ACL2 WORKSH
  • [6] Alves-Foss J., 2011, SPRINGER ENCY CRYPTO, P815
  • [7] Alves-Foss J, 2006, INT J EMBED SYST, V2, P239, DOI 10.1504/IJES.2006.014859
  • [8] AMES SR, 1983, COMPUTER, V16, P14, DOI 10.1109/MC.1983.1654439
  • [9] Andre P., 2009, P ESA WORKSH AV DAT
  • [10] [Anonymous], 2012, COMM CRIT INF TECHN
12345678910