# Refinement-based Specification and Security Analysis of Separation Kernels

## TL;DR

This paper introduces a formal refinement-based approach for specifying and analyzing the security of ARINC 653 compliant separation kernels, identifying security flaws through formal proofs and code review.

## Contribution

It presents a novel refinement framework for formal specification and security analysis of ARINC 653 separation kernels, including security proofs in Isabelle/HOL.

## Key findings

- Identified six security flaws in ARINC 653 standard and implementations
- Developed formal specifications covering key kernel functionalities
- Verified security properties using theorem proving in Isabelle/HOL

## 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.