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 条
[61]  
LynuxWorks Inc., 2012, TECHNICAL REPORT
[62]   A generic approach to the security of multi-threaded programs [J].
Mantel, H ;
Sabelfeld, A .
14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, :126-142
[63]   Formal construction of the mathematically analyzed separation kernel [J].
Martin, W ;
White, P ;
Taylor, FS ;
Goldberg, A .
FIFTEENTH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2000, :133-141
[64]   Creating high confidence in a separation kernel [J].
Martin W.B. ;
White P.D. ;
Taylor F.S. .
Automated Software Engineering, 2002, 9 (3) :263-284
[65]   Re-engineering Xen internals for higher-assurance security [J].
Center for High Assurance Computer Systems, Naval Research Laboratory, United States .
Inf Secur Tech Rep, 2008, 1 (17-24) :17-24
[66]  
McDermott J, 2012, 28TH ANNUAL COMPUTER SECURITY APPLICATIONS CONFERENCE (ACSAC 2012), P419
[67]  
McDermott John., 2008, P 6 ACM WORKSHOP FOR, P43, DOI DOI 10.1145/1456396.1456401
[68]  
Murray Toby, 2012, Certified Programs and Proofs. Second International Conference (CPP 2012). Proceedings, P126, DOI 10.1007/978-3-642-35308-6_12
[69]   seL4: from General Purpose to a Proof of Information Flow Enforcement [J].
Murray, Toby ;
Matichuk, Daniel ;
Brassil, Matthew ;
Gammie, Peter ;
Bourke, Timothy ;
Seefried, Sean ;
Lewis, Corey ;
Gao, Xin ;
Klein, Gerwin .
2013 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP), 2013, :415-429
[70]  
National Security Agency, 2007, TECHNICAL REPORT
12345678910