This is a formal specification and its security proofs for separation kernels in Isabelle/HOL. We provide a mechanically checked formal specification which comprises a generic execution model for separation kernels and an event specification for ARINC 653. We define a set of information flow security properties and an inference framework to sketch out the implications between security properties. We provide the security proofs to indicate information flow security of the specification.
The Isabelle/HOL source files are at please "http://securify.sce.ntu.edu.sg/skspecv1/".
A research paper is available at "http://arxiv.org/abs/1510.05091".
Created by Yongwang Zhao (zhaoyongwang@gmail.com, zhaoyw@buaa.edu.cn, ywzhao@ntu.edu.sg),
School of Computer Engineering, Nanyang Technological University, Singapore.
School of Computer Science & Engineering, BeiHang Unversity (BUAA), Beijing, P.R.China.