Advertisement

A Switch, in Time

  • Lenore D. Zuck
  • Sanjiva PrasadEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9533)

Abstract

Communication networks are quintessential concurrent and distributed systems, posing verification challenges concerning network protocols, reliability, resilience and fault-tolerance, and security. While techniques based on logic and process calculi have been employed in the verification of various protocols, there is a mismatch between the abstractions used in these approaches and the essential structure of networks. In particular, the formal models do not accurately capture the organization of networks in terms of (fast but dumb) table-based switches forwarding structured messages, with intelligence/control located only at the end-points.

To bridge this gap, we propose an extension of the axiomatic basis of communication proposed by Karsten et al. In this paper, a simple model of abstract switches and table-based prefix rewriting is characterized axiomatically using temporal logic. This formulation is able to address reconfigurations over time of the network. We illustrate our framework with simple examples drawn from SDNs, IPv6 mobility and anonymous routing protocols.

Keywords

Abstract switches Network protocols Data plane Control Time-dependent behavior Correctness 

Notes

Acknowledgements

The authors thank the anonymous referees for their valuable suggestions.

References

  1. 1.
    Abadi, M., Fournet, C.: Private authentication. Theor. Comput. Sci. 322(3), 427–476 (2004)CrossRefMathSciNetzbMATHGoogle Scholar
  2. 2.
    Amadio, R.M., Prasad, S.: Modelling IP mobility. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 301–316. Springer, Heidelberg (1998)Google Scholar
  3. 3.
    Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  4. 4.
    Armando, A., Basin, D.A., Cuéllar, J., Rusinowitch, M., Viganò, L.: Automated reasoning for security protocol analysis. J. Autom. Reason. 36(1–2), 1–3 (2006)CrossRefMathSciNetGoogle Scholar
  5. 5.
    Clark, D.: The design philosophy of the DARPA internet protocols. In: Proceedings of SIGCOMM 1988: ACM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, vol. 8, pp. 106–114. ACM (1988)Google Scholar
  6. 6.
    Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 24–37. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  7. 7.
    Delzanno, G., Ganty, P.: Automatic verification of time sensitive cryptographic protocols. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 342–356. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Dingledine, R., Mathewson, N., Syverson, P.F.: Tor: The second-generation onion router. In: Proceedings of 13th USENIX Security Symposium, SSYM 2004, pp. 303–320. USENIX Association (2004)Google Scholar
  9. 9.
    Dolev, D., Yao, A.C.C.: On the security of public key protocols. IEEE Trans. Inf. Theor. 29(2), 198–207 (1983)CrossRefMathSciNetzbMATHGoogle Scholar
  10. 10.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.:Knowledge-based programs. In: Proceedings of PODC 1995: 14th Annual ACM Symposium on Principles of Distributed Computing, pp. 153–163. ACM (1995)Google Scholar
  11. 11.
    Guttman, J.D., Thayer, F.J., Zuck, L.D.: The faithfulness of abstract protocol analysis: message authentication. J. Comput. Secur. 12(6), 865–891 (2004)Google Scholar
  12. 12.
    Halpern, J.Y., Zuck, L.D.: A little knowledge goes a long way: Knowledge-based derivations and correctness proofs for a family of protocols. J. ACM 39(3), 449–478 (1992)CrossRefMathSciNetzbMATHGoogle Scholar
  13. 13.
    Hughes, D.J.D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. J. Comput. Secur. 12(1), 3–36 (2004)Google Scholar
  14. 14.
    Karsten, M., Keshav, S., Prasad, S., Beg, M.: An axiomatic basis for communication. In: Proceedings of SIGCOMM 2007:ACM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, pp. 217–228. ACM (2007)Google Scholar
  15. 15.
    Kreutz, D., Ramos, F.M.V., Veríssimo, P.J.E., Esteve Rothenberg, C., Azodolmolky, S., Uhlig, S.: Software-defined networking: a comprehensive survey. Proc. IEEE 103(1), 14–76 (2015)CrossRefGoogle Scholar
  16. 16.
    Lamport, L.: What good is temporal logic? In: Information Processing 83 - Proceedings of WCC 1983: 9th IFIP World Computer Congress, pp. 657–668. North-Holland/IFIP (1983)Google Scholar
  17. 17.
    Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  18. 18.
    Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  19. 19.
    Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes I. Inf. Comput. 100(1), 1–40 (1992)CrossRefMathSciNetzbMATHGoogle Scholar
  20. 20.
    Perkins, C.E., Johnson, D.B.: Mobility support in IPv6. In: Proceedings of MobiCom 1996: 2nd Annual International Conference on Mobile Computing and Networking, pp. 27–37, New York, NY, USA. ACM (1996)Google Scholar
  21. 21.
    Prasad, S.: Abstract switches: A distributed model of communication and computation. In: Perspectives in Concurrency Theory. CRC Press (2009)Google Scholar
  22. 22.
    Sangiorgi, D., Walker, D.W.: On barbed equivalences in \(\pi \)-Calculus. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 292–304. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  23. 23.
    Zuck, L.D., Prasad, S.: Limited mobility, eventual stability. In: Piterman, N., et al. (eds.) HVC 2015. LNCS, vol. 9434, pp. 139–154. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-26287-1_9 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.University of Illinois at ChicagoChicagoUSA
  2. 2.Indian Institute of Technology DelhiNew DelhiIndia

Personalised recommendations