Please use this identifier to cite or link to this item:
Title: Refinement-based specification and security analysis of separation kernels
Authors: Zhao, Yongwang
Sanan, David
Zhang, Fuyuan
Liu, Yang
Keywords: Engineering::Computer science and engineering
Issue Date: 2019
Source: Zhao, Y., Sanan, D., Zhang, F., & Liu, Y. (2019). Refinement-Based Specification and Security Analysis of Separation Kernels. IEEE Transactions on Dependable and Secure Computing, 16(1), 127–141. doi:10.1109/tdsc.2017.2672983
Journal: IEEE Transactions on Dependable and Secure Computing
Abstract: Assurance of information-flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for improving safety, ARINC 653 has been complied with by mainstream separation kernels. Due to the new trend of integrating safe and secure functionalities into one separation kernel, security analysis of ARINC 653 as well as a formal specification with security proofs are thus significant for the development and certification of ARINC 653 compliant Separation Kernels (ARINC SKs). This paper presents a specification development and security analysis method for ARINC SKs based on refinement. We propose a generic security model and a stepwise refinement framework. Two levels of functional specification are developed by the refinement. A major part of separation kernel requirements in ARINC 653 are modeled, such as kernel initialization, two-level scheduling, partition and process management, and inter-partition communication. The formal specification and its security proofs are carried out in the Isabelle/HOL theorem prover. We have reviewed the source code of one industrial and two open-source ARINC SK implementations, i.e., VxWorks 653, XtratuM, and POK, in accordance with the formal specification. During the verification and code review, six security flaws, which can cause information leakage, are found in the ARINC 653 standard and the implementations.
ISSN: 1545-5971
DOI: 10.1109/TDSC.2017.2672983
Rights: © 2017 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. The published version is available at:
Fulltext Permission: open
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Journal Articles

Files in This Item:
File Description SizeFormat 
Refinement based specification and security analysis of separation kernels.pdf809.41 kBAdobe PDFView/Open

Citations 20

Updated on Mar 5, 2021

Page view(s)

Updated on Jun 30, 2022

Download(s) 50

Updated on Jun 30, 2022

Google ScholarTM




Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.