Recent advances in software-defined networking (SDN) and programmable data planes allow datacenter and enterprise network operators to quickly deploy new protocols, customize network behavior, and develop innovative services. These advances promise to improve and streamline network operations, improving the quality of service provided to end users. However programmable data planes also introduce new complexities to network management, notably, ensuring that the network satisfies critical security properties. Current network verification and analysis tools cannot handle these complex new networks. This work aims to address three important problems at the intersection of networking and computer security: First, the work proposes to develop new techniques that allow operators to verify that their network satisfies security properties like tenant isolation in a cloud hosting environment. Second, this work proposes to use the data plane to implement a security mechanism to enforce security properties, an approach that complements verification as a way to ensure correct network behavior. Finally, the work proposes to develop new security services that leverage the capabilities of a programmable data plane. Results of the proposed work will promote the adoption of more secure and flexible next-generation networks by providing operators the tools necessary to verify and enforce critical network security properties. As programmable data planes are poised to transform modern the architecture of modern networks, the proposed work will advance the current state of the art in networking by extending verification and enforcement techniques to programmable data plane networks, for which neither network verification nor security policy mechanisms currently exist. To do so, investigators will transform data plane programs, expressed in P4, into assertions suitable for analysis using existing network verification tools based on SMT solvers. Investigators will also develop a security kernel implemented as a P4 data plane program to enforce network-wide security properties at run time. Finally, this work will also develop new data plane services that will enable a new class of security functions to be deployed in the network in order to improve the overall security of computer networks.
EAGER: USBRCCR: Collaborative: Securing Networks in the Programmable Data Plane Era