The FVR project addresses a long-standing challenge in networking research -- bridging the gap between formal theories and actual implementations. We have developed the FSR (Formally Safe Routing) toolkit that unifies research in routing algebras with declarative networking to produce provably correct distributed implementations for inter-domain routing. In addition to the FSR toolkit, the FVR project has also explored the use of theorem proving and rewriting logic techniques to verify routing protcols.

Operators of distributed systems often find themselves needing to answer forensic questions, to perform a variety of managerial tasks. NetTrails is a novel provenance-based approach that provides the fundamental functionality required for answering forensic questions -- the capability to "explain" the existence (or change) of a distributed system state at a given time in a potentially adversarial environment. We evaluate our techniques in the context of concrete applications, such as Hadoop MapReduce or BGP interdomain routing.

The DS2 project explores a unified declarative platform for specifying, implementing, and analyzing secure extensible distributed systems. Our work is motivated by the proliferation of large-scale network information systems currently deployed for a variety of application domains including network monitoring infrastructures, cloud computing, content distribution networks, and network routing.