Rewriting semantics of meta-objects and composable distributed services

Communication between distributed objects may have to be protected against random failures and malicious attacks; also, communication timeliness may be essential or highly desired. Therefore, a distributed application often has to be extended with communication services providing some kind of fault-tolerance, secrecy, or quality-of-service guarantees. Ideally, such services should be defined in a highly modular and dynamically composable way, so that the combined assurance of several services can be achieved by composition in certain cases, and so that services can be added or removed from applications at runtime in response to changes in the environment. To reason about the formal properties of such composable communication services one first needs to give them a precise semantics. This paper proposes a rewriting logic semantics for the so-called "onion skin" model of distributed object reflection, in which different meta-objects, providing different communication services, can be stacked on top of a basic application object. Since the correct behavior of a service depends on the type of hostile environment, against which the service must protect the application, rewriting logic should also be used to specify such hostile environments. The service guarantees are then guarantees about the behavior specified by the union of the rewrite theories specifying the basic application, the services, and the hostile environment.