Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 325
  • Download : 64
One of the prerequisites for information society is secure and reliable communication among computing systems. Accordingly, network security appliances become key components of infrastructure, not only as security guardians, but also as reliable network components. Thus, for both fault tolerance and high network throughput, multiple security appliances are often deployed together in a group and managed via High- Availability (HA) protocol. In this paper, we present our experience of formally modeling and verifying the HA protocol used for commercial network security appliances through model checking. In addition, we applied a new debugging technique to detect multiple bugs without modifying/fixing the HA model by analyzing all counter examples. Throughout these formal analysis, we could effectively detect several design flaws.
Publisher
Springer Verlag
Issue Date
2007
Citation

ATVA

URI
http://hdl.handle.net/10203/24743
Appears in Collection
CS-Conference Papers(학술회의논문)

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0