A program logic for verifying secure routing protocols

DOI10.2168/LMCS-11(4:19)2015MaRDI QIDQ3460424zbMATH OpenOpenAlexFDO

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

Publication date 7 January 2016

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1510.03531

zbMATH Keywords

declarative networkingprogram logicrouting protocols

Mathematics Subject Classification ID

Logic in computer science (03B70) Internet topics (68M11) Network protocols (68M12) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: 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.

Recommendations

• Formal verification of standards for distance vector routing protocols
• Analyzing Internet Routing Security Using Model Checking
• Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study
• Epistemic Cord logic: verifying anonymous routing protocols in Ad Hoc network
• scientific article; zbMATH DE number 1926618

Cited in

(4)

• SANDLog
• VCGen
• Analyzing Internet Routing Security Using Model Checking
• Truth in advertising, lightweight verification of route integrity

Describes a project that uses

Uses Software

• Coq
• ProVerif
• RapidNet
• HOL/SPIN

This page was built for publication: A program logic for verifying secure routing protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460424)