A model for the analysis of security policies in service function chains

TL;DR

This paper introduces a formal model to verify security policy correctness in Service Function Chains (SFCs), addressing configuration and ordering challenges in SDN and NFV environments to prevent security flaws.

Contribution

It proposes a novel formal model for analyzing and verifying security policies in SFCs, facilitating the detection of incorrect SF interactions.

Findings

Model enables verification of security policy enforcement

Tools based on the model can detect security flaws

Addresses configuration and ordering issues in SFCs

Abstract

Two emerging architectural paradigms, i.e., Software Defined Networking (SDN) and Network Function Virtualization (NFV), enable the deployment and management of Service Function Chains (SFCs). A SFC is an ordered sequence of abstract Service Functions (SFs), e.g., firewalls, VPN-gateways,traffic monitors, that packets have to traverse in the route from source to destination. While this appealing solution offers significant advantages in terms of flexibility, it also introduces new challenges such as the correct configuration and ordering of SFs in the chain to satisfy overall security requirements. This paper presents a formal model conceived to enable the verification of correct policy enforcements in SFCs. Software tools based on the model can then be designed to cope with unwanted network behaviors (e.g., security flaws) deriving from incorrect interactions of SFs in the same SFC.