English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Assurance of information-flow security by formal methods is mandated insecurity certification of separation kernels. As an industrial standard forimproving safety, ARINC 653 has been complied with by mainstream separationkernels. Due to the new trend of integrating safe and secure functionalitiesinto one separation kernel, security analysis of ARINC 653 as well as a formalspecification with security proofs are thus significant for the development andcertification of ARINC 653 compliant Separation Kernels (ARINC SKs). This paperpresents a specification development and security analysis method for ARINC SKsbased on refinement. We propose a generic security model and a stepwiserefinement framework. Two levels of functional specification are developed bythe refinement. A major part of separation kernel requirements in ARINC 653 aremodeled, such as kernel initialization, two-level scheduling, partition andprocess management, and inter-partition communication. The formal specificationand its security proofs are carried out in the Isabelle/HOL theorem prover. Wehave reviewed the source code of one industrial and two open-source ARINC SKimplementations, i.e. VxWorks 653, XtratuM, and POK, in accordance with theformal specification. During the verification and code review, six securityflaws, which can cause information leakage, are found in the ARINC 653 standardand the implementations.

Refinement-based Specification and Security Analysis of Separation Kernels