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
相关论文
共 50 条
  • [41] Formal specification and verification of the SET/A protocol with an integrated approach
    Lam, VSW
    Padget, J
    CEC 2004: IEEE INTERNATIONAL CONFERENCE ON E-COMMERCE TECHNOLOGY, PROCEEDINGS, 2004, : 229 - 235
  • [42] Formal Specification And Verification Of Reconfigurable Wireless Sensor Networks
    Grichi, Hanen
    Mosbahi, Olfa
    Khalgui, Mohamed
    2015 IEEE 12TH INTERNATIONAL MULTI-CONFERENCE ON SYSTEMS, SIGNALS & DEVICES (SSD), 2015,
  • [43] Error-Tolerant Processors: Formal Specification and Verification
    Golnari, Ameneh
    Vizel, Yakir
    Malik, Sharad
    2015 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2015, : 286 - 293
  • [44] A Formal Methods Approach to Security Requirements Specification and Verification
    Rouland, Quentin
    Hamid, Brahim
    Bodeveix, Jean-Paul
    Filali, Mamoun
    2019 24TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2019), 2019, : 236 - 241
  • [45] A formal requirements engineering method for specification, synthesis, and verification
    vonderBeeck, M
    Margaria, T
    Steffen, B
    8TH CONFERENCE ON SOFTWARE ENGINEERING ENVIRONMENTS - PROCEEDINGS, 1997, : 131 - 144
  • [46] Compositional Verification Using a Formal Component and Interface Specification
    Xing, Yue
    Lu, Huaixi
    Gupta, Aarti
    Malik, Sharad
    2022 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, ICCAD, 2022,
  • [47] FORMAL SPECIFICATION AND COMPOSITIONAL VERIFICATION OF AN ATOMIC BROADCAST PROTOCOL
    ZHOU, P
    HOOMAN, J
    REAL-TIME SYSTEMS, 1995, 9 (02) : 119 - 145
  • [48] A Summary of Formal Specification and Verification of Autonomous Robotic Systems
    Luckcuck, Matt
    Farrell, Marie
    Dennis, Louise A.
    Dixon, Clare
    Fisher, Michael
    INTEGRATED FORMAL METHODS, IFM 2019, 2019, 11918 : 538 - 541
  • [49] FORMAL TECHNIQUES FOR THE SPECIFICATION, VERIFICATION AND CONSTRUCTION OF COMMUNICATION PROTOCOLS
    CHOI, TY
    IEEE COMMUNICATIONS MAGAZINE, 1985, 23 (10) : 46 - 52
  • [50] Formal Specification and Verification of a Selective Defense for TDoS Attacks
    Dantas, Yuri Gil
    Lemos, Marcilio O. O.
    Fonseca, Iguatemi E.
    Nigam, Vivek
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2016, 2016, 9942 : 82 - 97
12345