TechNETium: Atomic Predicates and Model Driven Development to Verify Security Network Policies

Fifth-generation (5G) networks will deliver unprecedented levels of quality of service for online gaming and multimedia-rich social interaction, providing virtual environments optimized for vertical applications through innovative approaches to physical resource management. These techniques must consider security aspects in all phases and at every layer. Trusted communications between individuals and reliable platforms running services for social good depend on the resiliency to network-level attacks such as hijacking and denial-of-service. The verification of topological properties represents a well-suited approach to address these issues in a 5G environment. This paper illustrates moves from formal methods existing in literature, namely atomic predicates (AP) and header space analysis (HSA). It describes a method of integrating AP in Software Defined Network architectures, achieving the same expressive power as HSA without its performance hit, to make topology verification viable for real-time security applications.