Enforcing Generalized Refinement-Based Noninterference for Secure Interface Composition

摘要: Information flow security has been considered as a critical requirement on complicated component-based software. The recent efforts the compositional information analyses were limited expressiveness of lattice and efficiency enforcement. Extending these approaches to support more general lattices is usually nontrivial because compositionality properties should be properly treated. In this work, we present new extension interface automaton. On structure, propose two refinement-based properties, adaptable any finite lattice. For each property, prove condition that ensures property preserved under composition. Furthermore, implement refinement algorithms decision procedure. We demonstrate usability our approach with in-depth case studies. evaluation results show enforcement can effectively reduce verification cost compared global composite system.