Model checking invariant security properties in OpenFlow

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.
Publisher
Institute of Electrical and Electronics Engineers Inc.
Issue Date
2013-06-10
Language
English
Citation

International Conference on Communications, ICC 2013, pp.1974 - 1979

DOI
10.1109/ICC.2013.6654813
URI
http://hdl.handle.net/10203/225453
Appears in Collection
CS-Conference Papers(학술회의논문)
Files in This Item
There are no files associated with this item.
  • Hit : 28
  • Download : 0
  • Cited 0 times in thomson ci

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0