  Assurance of information flow security by formal methods is mandated in
security certification of separation kernels. As an industrial standard for
separation kernels, ARINC 653 has been complied with by mainstream separation
kernels. Security of functionalities defined in ARINC 653 is thus very
important for the development and certification of separation kernels. This
paper presents the first effort to formally specify and verify separation
kernels with ARINC 653 channel-based communication. We provide a reusable
formal specification and security proofs for separation kernels in
Isabelle/HOL. During reasoning about information flow security, we find some
security flaws in the ARINC 653 standard, which can cause information leakage,
and fix them in our specification. We also validate the existence of the
security flaws in two open-source ARINC 653 compliant separation kernels.
