Skip to main content
BOB 2019

Logo of BOB 2019 BOB 2019

22nd March 2019

Berlin, Germany

Part of the BOB series

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