Model Checking Invariant Security Properties in OpenFlow Conference Paper

abstract

• The OpenFlow (OF) switching specification represents an innovative and open standard for enabling the dynamic programming of flow control policies in production networks. Unfortunately, thus far researchers have paid little attention to the development of methods for verifying that dynamic flow policies inserted within an OpenFlow network do not violate the network's underlying security policy. We introduce Flover, a model checking system which verifies that the aggregate of flow policies instantiated within an OpenFlow network does not violate the network's security policy. We have implemented Flover using the Yices SMT solver, which we then integrated into NOX, a popular OpenFlow network controller. Flover provides NOX a formal validation of the OpenFlow network's security posture. 2013 IEEE.

name of conference

• 2013 IEEE International Conference on Communications (ICC)

authors

• Gu, Guofei

published proceedings

• 2013 IEEE INTERNATIONAL CONFERENCE ON COMMUNICATIONS (ICC)

altmetric score

• 3

author list (cited authors)

• Son, S., Shin, S., Yegneswaran, V., Porras, P., & Gu, G.

citation count

• 123

complete list of authors

• Son, Sooel||Shin, Seungwon||Yegneswaran, Vinod||Porras, Phillip||Gu, Guofei

publication date

• January 2013

publisher

• Institute of Electrical and Electronics Engineers (IEEE)  Publisher

published in

• 2013 National Conference on Communications, NCC 2013  Journal

keywords

• Business Communication
• Dynamic Flow Policies
• Dynamic Programming
• Educational Institutions
• Flover
• Flow Control Policies
• Formal Validation
• Formal Verification
• Model Checking
• Model Checking Invariant Security Properties
• Model Checking System
• Nox
• Open Standard
• Open Systems
• Openflow Network Controller
• Openflow Switching Specification
• Ports (computers)
• Production Networks
• Security
• Security Policy
• Standards
• Switches
• Telecommunication Control
• Yices Smt Solver

Digital Object Identifier (DOI)

• 10.1109/icc.2013.6654813

International Standard Book Number (ISBN) 13

• 9781467331227

start page

• 1974

end page

• 1979

URL

• http://dx.doi.org/10.1109/icc.2013.6654813