Solver-Aided Multi-Party Configuration

ABSTRACTConfiguring a service mesh often involves multiple parties, each of whom is responsible for separate portions of the overall system. This can result in miscommunication, silent and sudden errors, or a failure to meet goals. We identify two distinct modes of configuration that call for different solutions. We use synthesis algorithms to extract a set of properties---the envelope ---that each party needs the other to obey. Administrators can use the envelope to aid verification and synthesis or to support fault-localization and negotiation when goals conflict. This paper introduces the problem, lays out the modes, presents algorithms for to each, and gives a prototype implementation. We use this to show the feasibility of the approach in the microservices access-control domain and raise new research questions.