Towards A Secure and Verifiable Future Internet

In recent years, there have been strong interests in the networking community in designing new Internet architectures. One of the driving forces behind these “clean-slate” designs is the need to address pressing security concerns of the Internet. As a consequence, recent architectures, such as SCION [8] and ICING [5], provide radically new architectures that claim to provide stronger security guarantees. One of the limitations of current proposals is that security claims of these new designs lack formal security proofs – these protocols are evaluated primarily via experimental evaluations and argued via informal reasoning. In this paper, we outline our research agenda on programming language support for implementing secure Internet protocols, and verifying the security properties of these implementations. Central to our work is the use of Secure Network Datalog (SeNDLog) [9], a declarative networking [4] language with cryptographic primitives. SeNDLog extends the Network Datalog (NDLog) declarative networking language with user-defined cryptographic functions. Specifically, our project aims to achieve the following goals. First, we plan to demonstrate that most existing secure Internet routing architectures can be easily expressed in SeNDLog. Second, to facilitate formal proofs of security, we are developing a set of sound reasoning principles over SeNDLog. Using these reasoning principles, we would be able to extract proof obligations in the form of first-order logic formulas given any SeNDLog program and the security properties in question.