A Generalized Non-interference Based on Refinement of Interfaces

In the design and implementation of complicated component-based softwares, the security requirements on the whole system are hard to achieve due to the difficulty on enforcing the compositionality of the security properties. The specification and verification of security properties are the critical issues in the development of component-based softwares. In this paper, we focus on the generalization on the security lattice over the information flow security properties enforceable on the component-based softwares. The previous definitions of the information flow security properties in the component-based design are restricted on the binary security lattice model. In this work, we extend the interface structure for security to the generalized interface structure for security (GISS). We define a refinement relation and use this relation to give a non-interference definition (SME-NI) based on the principle of secure multi-execution. This is the first application of secure multi-execution on the information flow security verification of component-based systems. The new definition of non-interference can be adapted to any finite security lattice models. The Coq proof assistant is used to implement the certified library for interface automata, as well as the decision procedure for the refinement relation. The experimental results show the characteristics of SME-NI and the validity of decision procedure.