Please use this identifier to cite or link to this item:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorZhao, Yongwangen_US
dc.contributor.authorSanan, Daviden_US
dc.contributor.authorZhang, Fuyuanen_US
dc.contributor.authorLiu, Yangen_US
dc.identifier.citationZhao, 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.2672983en_US
dc.description.abstractAssurance 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.en_US
dc.description.sponsorshipNational Research Foundation (NRF)en_US
dc.relation.ispartofIEEE Transactions on Dependable and Secure Computingen_US
dc.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:
dc.subjectEngineering::Computer science and engineeringen_US
dc.titleRefinement-based specification and security analysis of separation kernelsen_US
dc.typeJournal Articleen
dc.contributor.schoolSchool of Computer Science and Engineeringen_US
dc.description.versionAccepted versionen_US
dc.subject.keywordsSeparation Kernelsen_US
dc.subject.keywordsARINC 653en_US
dc.description.acknowledgementWe would like to thank David Basin of Department of Com-puter Science, ETH Zurich, Gerwin Klein and Ralf Huuck ofNICTA, Australia for their suggestions. This research is sup-ported in part by the National Research Foundation, Prime Minister’s Office, Singapore under its National Cybersecurity R&D Program (Award No. NRF2014NCR-NCR001-30) and administered by the National Cybersecurity R&D Directorate.en_US
item.fulltextWith 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.