Verification of the Instantiation and Integration of Security Patterns
DOI:
https://doi.org/10.13052/jwe1540-9589.19347Keywords:
Software engineering, software safety, software verificationAbstract
As software applications suffer from increasing malicious attacks, security becomes a critically important issue for software development. To avoid security problems and increase efficiency, a large software system design may reuse good security solutions for existing security patterns. While security patterns document expert solutions to common security problems and capture well-examined practices on secure software design, implementing them in a particular context (pattern instantiation) and composing them with other related patterns (pattern integration) are prone to flaws and may break expected security properties. In this paper, we present an approach to verify security patterns instantiation and integration automatically. We offer formal definitions for security pattern instantiation and integration, and establish rules to transform sequence diagrams (representing the behaviors of security patterns) to expressions in Milner’s Calculus of Communicating Systems (CCS). We prove the correctness of the proposed transformation, and propose an algorithm to carry out this transformation automatically. In particular, we formally specify the alternative flows of UML sequence diagrams guarded by constraint conditions, which allows us to model choice making behaviors of security patterns precisely. The properties of the instantiation and integration can be verified by model checking against their CCS expressions. Flaws of instantiation and integration can, therefore, be discovered early in the design stage. We use two case studies to illustrate our approach and show the capability to prove security in integration and detect design errors in instantiation respectively.
Downloads
References
Abrial, J. R. 1996. The B-book. Cambridge University Press Cambridge. DOI: http://dx.doi.org/10.1017/CBO9780511624162
Cleaveland, R., Parrow, J. and Steffen, B. The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems. ACM Trans. on Prog. Lang. and Systems. 15,1 (1993), 36–72. DOI: http://dx.doi.org/10.1145/151646.151648
Browne, M., Clarke, E. and Dill, D. Automatic Verification of Sequential Circuits Using Temporal Logic. IEEE Transactions on Computer. C-35,12 (1986), 1035–1044.
Dong, J., Peng, T. and Qiu, Z. Commutability of Design Pattern Instantiation and Integration. In the Proceedings of the First IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering (TASE). China, June 2007, pp. 283–292. DOI: http://dx.doi.org/10.1109/TASE.2007.14
Dong, J., Peng, T. and Zhao, Y. Automated Verification of Security Pattern Compositions. In Information and Software Technology (IST), Elsevier-Science. 53,3 (2010), 274–295. DOI: http://dx.doi.org/10.1016/j.infsof.2009.10.001
Dong, J., Peng, T. and Zhao, Y. On Instantiation and Integration Commutability of Design Pattern. The Computer Journal, Oxford University Press. 54, 1 (Jan. 2011), 164–184. DOI: http://dx.doi.org/10.1093/comjnl/bxp125
Peng, T., Dong, J. and Zhao, Y. Verifying Behavioral Correctness of Design Pattern Implementation. In the Proceedings of the 20th International Conference on Software Engineering and Knowledge Engineering (SEKE). CA, USA, July 2008, pp. 454–459.
Peng, T. and Ding, G. Formal Specification and Automated Verification of UML2.0 Sequence Diagrams. In 2012 IEEE International Conference on Granular Computing. Hangzhou, China, 370–375. DOI: http://dx.doi.org/10.1109/GrC.2012.6468641
Dwyer, M., Avrunin, G. and Corbett, J. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering. Los Angeles, USA, May 1999, pp. 411–420.
Emersion, E. and Halpern, J. ‘Sometime’ and ‘not never’ revisited: on branching versus linear time temporal logic. Journal of the Association for Computing Machinery. 33,1 (1986), 151–178.
Eshuis, Rik, and Roel Wieringa. 2004. Tool support for verifying UML activity diagrams. Software Engineering. IEEE Transactions. 30,7 (2004), 437–447. DOI: http://dx.doi.org/10.1109/TSE.2004.33
Gamma, E., Helm, R., Johnson, R. and Vlissides, J. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley.
Holzmann, G. The Model Checker SPIN. IEEE Transactions on Software Engineering. 23,5 (1997), 279–295. DOI: http://dx.doi.org/10.1109/32.588521
Li, J. and Chen, F. The Z specification-based method for the semantic analysis of UML sequence diagrams. Journal of Xidian University (Natural Science). 30,4 (2003), 519–524 (in Chinese with English abstract).
Kong, J., Zhang, K., Dong, J. and Xua D. 2009. Specifying behavioral semantics of UML diagrams through graph transformations. Journal of Systems and Software. 82,2 (2009), 292–306. DOI: http://dx.doi.org/10.1016/j.jss.2008.06.030
Johan, L., and Paltor, I. vUML: A tool for verifying UML models. In 14th IEEE International Conference on Automated Software Engineering. Cocoa Beach, Florida, 255. DOI: http://dx.doi.org/10.1109/ASE.1999.802301
Li, X., Liu Z., and He, J. A Formal Semantics of UML Sequence Diagrams. In The Proceedings of ASWEC2004. Melbourne, Australia, pp. 13–16.
Lima, V., Talhi, C., Mouheb, D., Debbabi, M. and Wang, L. Formal Verification and Validation of UML 2.0 Sequence Diagrams using Source and Destination of Messages. Electronic Notes in Theoretical Computer Science. 254 (2009), 143–160.
Mikkonen, T. Formalizing Design Pattern. In Proceedings of the 20th International Conference on Software Engineering. Kyoto, Japan, April 1998, pp.115–124. DOI: http://dx.doi.org/10.1109/ICSE.1998.671108
Pnueli, A. and Harel, E. Applications of Temporal Logic to the Specification of Real-time Systems. Springer. DOI: http://dx.doi.org/10.1007/3-540-50302-1_4
Meyer, B. Applying “design by contract”. IEEE Computer. 25,10 (1992), 40–51.
Milner, R. Communication and Concurrency. International Series in Computer Science. Prentice Hall.
Saeki, M. Behavioral specification of GOF design patterns with LOTOS. In Proceedings of the Seventh Asia-Pacific Software Engineering Conference (APSEC). Singapore, 408–415.
Storrle, H. Trace Semantics of Interactions in UML2.0. Technical report, LMU Munchen.
Yoshioka, N., Honiden, S. and Finkelstein, A. Security patterns: a method for constructing secure and efficient inter-company coordination systems. In Proceedings of Enterprise Distributed Object computing Conference 2004 (EDOC’04). 87–97. DOI: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=1342507
Yoshioka, N., Washizaki, H. and Maruyma, K. A survey on security patterns. Progress in Informatics. No. 5 (March 2008), 35–47. DOI: 10.2201/NiiPi.2008.5.5
Steel, C., Nagappan, R. and Lai, R. Core Security Patterns: Best Practices and Strategies for J2EE, Web Services, and Identity Management. Prentice Hall PTR.
Toufik Taibia and David Chek Ling Ngo 2003. Formal specification of design pattern combination using BPSL. International Journal of Information and Software Technology. Elsevier-Science, 45,3 (2003), 157–170.
Viega, J. and McGraw, G. Building Secure Software: How to Avoid Security Problems the Right Way. Addison-Wesley.
Zhang, C., Duan Z. and Tian C. Specification and verification of UML2.0 Sequence diagram based on Event Deterministic Finite Automat. Journal of Software. 22,11 (2011), 2625–2638.
Zhou, X. and Shao., Z. ASM semantic modeling and checking for sequence diagrams. In Proc. of the 5th Int’l Conf. on Natural Computation. Washington: IEEE Computer Society, pp. 527–530.
IBM developers Work. 2004. UML basics of Sequence Diagrams. IBM developers Work. http://www.ibm.com/developerworks/rational/library/3101.html
Microsoft Corporation. 2006. Web Service Security Pattern and Practice. March 2006. 175–177.
Microsoft.com. 2005. Web Service Security. http://msdn.microsoft.com/en-us/library/aa480545.aspx; Microsoft.com. 2005. Brokered Authentication. http://msdn.microsoft.com/en-us/library/aa480560.aspx
Clarke, E. and Wang Q. 2^5 Years of Model Checking. Ershov Memorial Conference 2014: 26–40.
