Verifying Secure Interface Composition for Component-Based System Designs

Information flow security has been considered as a critical requirement on software systems, especially when heterogeneous components from different parties cooperate to achieve end-to-end enforcement on data confidentiality. Enforcing the information flow security properties on complicated systems faces a great challenge because the properties cannot be preserved under composition and most of the current approaches are not scalable enough. To address this problem, there have been several recent efforts on the compositional information flow analyses developed for different abstraction levels. But these approaches have rarely been considered to incorporate with the process of system design. Integrating the security enforcement with the model-based development process can provide the designer with ability to verify information flow security in the early stage of system development. We propose a compositional information flow verification which is integrated with model-based system design in Sys ML by an automated model translation from semi-formal behavior and structure models to interface automata. Our compositional approach is general to support the complex security lattices and a variety of in distinguish ability relations. The evaluation results show the usability of our approach on practical system designs and the scalability of the compositional verification.