Chen, Chen and Jia, Limin and Xu, Hao and Luo, Cheng and Zhou, Wenchaoet al. - A Program Logic for Verifying Secure Routing Protocols

lmcs:1620 - Logical Methods in Computer Science, December 29, 2015, Volume 11, Issue 4
A Program Logic for Verifying Secure Routing Protocols

Authors: Chen, Chen and Jia, Limin and Xu, Hao and Luo, Cheng and Zhou, Wenchao and Loo, Boon Thau

The Internet, as it stands today, is highly vulnerable to attacks. However, little has been done to understand and verify the formal security guarantees of proposed secure inter-domain routing protocols, such as Secure BGP (S-BGP). In this paper, we develop a sound program logic for SANDLog-a declarative specification language for secure routing protocols for verifying properties of these protocols. We prove invariant properties of SANDLog programs that run in an adversarial environment. As a step towards automated verification, we implement a verification condition generator (VCGen) to automatically extract proof obligations. VCGen is integrated into a compiler for SANDLog that can generate executable protocol implementations; and thus, both verification and empirical evaluation of secure routing protocols can be carried out in this unified framework. To validate our framework, we encoded several proposed secure routing mechanisms in SANDLog, verified variants of path authenticity properties by manually discharging the generated verification conditions in Coq, and generated executable code based on SANDLog specification and ran the code in simulation.


Source : oai:arXiv.org:1510.03531
DOI : 10.2168/LMCS-11(4:19)2015
Volume: Volume 11, Issue 4
Published on: December 29, 2015
Submitted on: December 2, 2014
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 98 times.
This article's PDF has been downloaded 61 times.