A Program Logic for Verifying Secure Routing Protocols

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 (1) encoded several proposed secure routing mechanisms in SANDLog, (2) verified variants of path authenticity properties by manually discharging the generated verification conditions in Coq, and (3) generated executable code based on SANDLog specification and ran the code in simulation.
Type de document :
Communication dans un congrès
Erika Ábrahám; Catuscia Palamidessi. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. Springer, Lecture Notes in Computer Science, LNCS-8461, pp.117-132, 2014, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-662-43613-4_8〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01398011
Contributeur : Hal Ifip <>
Soumis le : mercredi 16 novembre 2016 - 15:36:00
Dernière modification le : mercredi 16 novembre 2016 - 16:23:24
Document(s) archivé(s) le : jeudi 16 mars 2017 - 17:46:12

Fichier

978-3-662-43613-4_8_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Chen Chen, Limin Jia, Hao Xu, Cheng Luo, Wenchao Zhou, et al.. A Program Logic for Verifying Secure Routing Protocols. Erika Ábrahám; Catuscia Palamidessi. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. Springer, Lecture Notes in Computer Science, LNCS-8461, pp.117-132, 2014, Formal Techniques for Distributed Objects, Components, and Systems. 〈10.1007/978-3-662-43613-4_8〉. 〈hal-01398011〉

Partager

Métriques

Consultations de la notice

33

Téléchargements de fichiers

14