Engineering Secured Networks with Scalable Network Verification
The Internet stands as one of the most complex and large-scale systems ever built by humankind. It consists of a vast array of software and protocols operating over hundreds of millions of hosts and thousands of competing Internet Service Providers. Unfortunately, like any complex system, it has proven very difficult to get its design right. And as the infrastructures and components of our daily lives become increasingly dependent on Internet operations, so has the importance of ensuring the system’s security and correct operation.
How can we build a secure and highly reliable Internet? During his Center appointment, Professor Caesar proposes to develop and evaluate foundational algorithms and novel applications enabled by a system, Veriflow, that provides a general platform for formal reasoning about network behavior. His central hypothesis is that Veriflow can be extended to verify automatically the security and correctness of computer networks in real time, yielding (a) provable guarantees of correctness or (b) the discovery of vulnerabilities and assistance to network operators in determining their cause.
First, his team will improve the generality and completeness of Veriflow by extending the core logic to model a wider range of invariants.
Specifically, they will develop invariants to check service quality (whether the network capacity between two computers is greater than a provided value), dynamics (whether the network meets an invariant at intermediate stages of network events, while forwarding tables are being updated), and performance areas related to security, cross-router-consistency checking, and constraints. They will also extend the core logic to handle more complex network devices.
The team will then aim to transition Veriflow into a practical implementation. They will investigate several optimizations of Veriflow’s analysis algorithms to improve performance, including the precomputation of likely future events and the caching of computations that are commonly performed. They will also stress Veriflow’s real-time capabilities to characterize its performance in realistic operational environments and in simulations of networks with increasing scale and increasing rates of dynamics. As an end result, Veriflow could automatically repair network errors that are discovered and analyze correlations in the errors to reveal unsafe practices by network operators.