Logic in the Service of System Configurations
Programming is glamorous; everyone has ideas for how it should be done better. System configuration, in contrast, lacks panache; it seems to consist mainly of fiddling with lots of little settings across devices. However, configuration actually performs a very difficult task: the devices are heterogenous, they work at different levels of abstraction (databases, servers, networks), and they form a distributed system that must act in concert to achieve a subtle (often unstated) goal. Indeed, many security and correctness problems stem not from incorrect programs (for which people constantly produce new verifiers) but rather from subtle configuration errors.
There are several modalities of action: e.g., verification (given a configuration and a property, does the configuration match the property?); differential analysis (given two configurations, how are they different?); and synthesis (given a specification, can we generate a configuration?). All these can be unified under the rubric of mathematical logic. We will see how the tools of logic can address several of these problems in a somewhat uniform way.
The talk will be self-contained, but does expect that the listener has a basic knowledge of logic (namely that the upside-down A is for-all and the backward E is there-exists).
This session is held on in Talks #1