How Do Asynchronous Communication Models Impact the Composability of Information Flow Security?

Information flow security is not guaranteed to be preserved when a system is being composed of secure components. Whereas asynchronous communication is known to mitigate this problem in principle, the concrete impact of specific communication models on composability has not been investigated so far. We address this problem by formalizing seven asynchronous communication models from the literature in the Uppaal environment. On this basis, we capture a negative example, where information flow security is not composable, and contrast it with the formalized communication models to investigate their impact on composability. Our investigation shows that six out of seven asynchronous communication models ensure composability of information flow security.