Project Overview

Configuring 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.

Contributors

Kevin Dackow, Andrew Wagner, Tim Nelson, Shriram Krishnamurthi, Theophilus A. Benson

Relevant Links

Solver-Aided Multi-Party Configuration Paper