Confidentiality of Interactions in Concurrent Object-Oriented Systems

We consider a general concurrency model for distributed systems, based on concurrent objects communicating by asynchronous methods. This model is suitable for modeling of modern service-oriented systems, and gives rise to efficient interaction avoiding active waiting and low-level synchronization primitives such as explicit signaling and lock operations. This concurrency model has a simple semantics and allows us to focus on information flow at a high level of abstraction, and allows realistic analysis by avoiding unnecessary restrictions on information flow between confidential and non-confidential data. We formalize our approach by introducing a high-level language for this concurrency model, and we provide a secrecy-type system to capture inter-object communication. We prove soundness based on an operational semantics, which includes runtime secrecy levels.