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

Onos Architecture
In 2020 IEEE 17th Annual Consumer Communications & Networking Conference (CCNC)

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.

Andrea Melis
Andrea Melis
Adjunct Professor
Post-Doc Researcher

Security Enthusiast, CTF Player, Half Nerd/Half Geek.