Refinement-based specification and security analysis of separation kernels
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...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Journal Article |
| Language: | English |
| Published: |
2020
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/10356/144810 |
| _version_ | 1811686167519690752 |
|---|---|
| author | Zhao, Yongwang Sanan, David Zhang, Fuyuan Liu, Yang |
| author2 | School of Computer Science and Engineering |
| author_facet | School of Computer Science and Engineering Zhao, Yongwang Sanan, David Zhang, Fuyuan Liu, Yang |
| author_sort | Zhao, Yongwang |
| collection | NTU |
| description | 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. |
| first_indexed | 2024-10-01T04:56:07Z |
| format | Journal Article |
| id | ntu-10356/144810 |
| institution | Nanyang Technological University |
| language | English |
| last_indexed | 2024-10-01T04:56:07Z |
| publishDate | 2020 |
| record_format | dspace |
| spelling | ntu-10356/1448102020-11-25T03:35:20Z Refinement-based specification and security analysis of separation kernels Zhao, Yongwang Sanan, David Zhang, Fuyuan Liu, Yang School of Computer Science and Engineering Engineering::Computer science and engineering Separation Kernels ARINC 653 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. National Research Foundation (NRF) Accepted version We 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. 2020-11-25T03:35:20Z 2020-11-25T03:35:20Z 2019 Journal Article 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 1545-5971 https://hdl.handle.net/10356/144810 10.1109/TDSC.2017.2672983 1 16 127 141 en IEEE Transactions on Dependable and Secure Computing © 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: https://doi.org/10.1109/TDSC.2017.2672983. application/pdf |
| spellingShingle | Engineering::Computer science and engineering Separation Kernels ARINC 653 Zhao, Yongwang Sanan, David Zhang, Fuyuan Liu, Yang Refinement-based specification and security analysis of separation kernels |
| title | Refinement-based specification and security analysis of separation kernels |
| title_full | Refinement-based specification and security analysis of separation kernels |
| title_fullStr | Refinement-based specification and security analysis of separation kernels |
| title_full_unstemmed | Refinement-based specification and security analysis of separation kernels |
| title_short | Refinement-based specification and security analysis of separation kernels |
| title_sort | refinement based specification and security analysis of separation kernels |
| topic | Engineering::Computer science and engineering Separation Kernels ARINC 653 |
| url | https://hdl.handle.net/10356/144810 |
| work_keys_str_mv | AT zhaoyongwang refinementbasedspecificationandsecurityanalysisofseparationkernels AT sanandavid refinementbasedspecificationandsecurityanalysisofseparationkernels AT zhangfuyuan refinementbasedspecificationandsecurityanalysisofseparationkernels AT liuyang refinementbasedspecificationandsecurityanalysisofseparationkernels |