Formally specifying and checking policies and anomalies in service function chaining. (15th November 2019)

• Record Type: Journal Article
• Authors: Valenza, Fulvio; Spinoso, Serena; Sisto, Riccardo
• Is Part Of: Journal of network and computer applications. Volume 146(2019)
• Publication Date: 2019-11-15
• Subjects: Service function chaining -- Forwarding policies -- Formal verification; Microcomputers -- Periodicals; Computer networks -- Periodicals; Application software -- Periodicals; Micro-ordinateurs -- Périodiques; Réseaux d'ordinateurs -- Périodiques; Logiciels d'application -- Périodiques; Application software; Computer networks; Microcomputers; Periodicals; 004.05; 004
• DOI: 10.1016/j.jnca.2019.102419
• Languages: English
• ISSNs: 1084-8045

Abstract

Abstract: One of the proposed management strategies for SDN networks is to specify traffic forwarding through policies, where each policy rule identifies a traffic flow and its traversed service chains. While network operators need to check network configurations as soon as possible, the SDN verification literature focuses on checking policy correctness during or after their deployment. This paper, instead, proposes early verification of forwarding policies before their deployment, by looking for the presence of anomalies that can potentially lead to erroneous and unexpected network behaviour. The proposed verification relies on a formal model that enables high flexibility in specifying both a forwarding policy and the set of anomalies to verify. The presented approach is efficient and highly scalable, as confirmed by tests with large networks.