Information Flow-Based Security Construction for Compositional Interface Automata

Abstract

Information flow has been considered as a critical requirement to solve security related issues for complicated component-based system. However, security conditions are often fragile and general security properties may be not available to enforce the composition. Thus, this paper gives the computation model of interface automata (IA) and studies how the compositional interfaces behave to capture the information leakage with security process algebra (SPA) language. And we find that persistent bisimulation-based non deducibility property is preserved under composition, while it is not fully applicable to IA model. So several sufficient conditions for the property is developed to apply for composition of interface automata. Those conditions are given as theorems and proved efficiently to analyze security. Finally, we cite a classical instance to handle the composition and use an automatic verification software to test the correctness of our algorithms on compositional conditions.