Verification of the Instantiation and Integration of Security Patterns

  • Tu Peng School of Computer Science and Technology, Beijing Institute of Technology, Beijing, 100081, China
  • Shuliang Wang School of Computer Science and Technology, Beijing Institute of Technology, Beijing, 100081, China
  • Jing Geng School of Computer Science and Technology, Beijing Institute of Technology, Beijing, 100081, China
  • Qinsi Wang Department of Computer Science, Carnegie Mellon University, Pittsburgh, USA
  • Yun Yang School of Software and Electrical Engineering, Swinburne University of Technology, PO Box 218, Hawthorn, Melbourne, Australia 3122
  • Kang Zhang Department of Computer Science, University of Texas at Dallas, Richardson, TX 75083, USA
Keywords: Software engineering, software safety, software verification

Abstract

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

Download data is not yet available.

Author Biographies

Tu Peng, School of Computer Science and Technology, Beijing Institute of Technology, Beijing, 100081, China

Tu Peng received his B.Sc. and M.Sc. degrees in Mathematics from Peking University, China; and Ph.D. degree in Software Engineer from University of Texas at Dallas, USA. He is currently an associate professor in school of computer science, Beijing Institute of Technology. His research interests include software testing, verification, architecture and machine learning.

Shuliang Wang, School of Computer Science and Technology, Beijing Institute of Technology, Beijing, 100081, China

Shuliang Wang received his Ph.D. degree in Computer Science from Wuhan University, China. He is currently a professor in Beijing Institute of Technology, China. His research interests include spatial data mining, and software engineering. For his innovatory study of spatial data mining, he was awarded the Fifth Annual InfoSciÒ-Journals Excellence in Research Awards of IGI Global, and one of the best national thesis in China.

Jing Geng, School of Computer Science and Technology, Beijing Institute of Technology, Beijing, 100081, China

Jing Geng received her B.Eng. degree in Software Engineer from University of Electronic Science and Technology of China; and Ph.D. degree in Photogrammetry and Remote Sensing from WuHan University, China. She is currently an assistant research fellow in Beijing Institute of Technology. Her research interests include spatial data mining, Geospatial knowledge service.

Qinsi Wang, Department of Computer Science, Carnegie Mellon University, Pittsburgh, USA

Qinsi Wang is an independent postdoctoral researcher in the group of Prof. Jean Yang at Carnegie Mellon University. She received her PhD in Computer Science at CMU under the supervision of Prof. Edmund M. Clarke (Turing Award 2007) in Sep 2016. Her research interest is to develop formal specification and verification techniques for real-world systems with the emphasis on statistical model checking for models of biological signaling networks, stochastic SMT-based methods for stochastic hybrid systems, and combining model checking techniques with machine learning methods for the study of biological systems and causal networks.

Yun Yang, School of Software and Electrical Engineering, Swinburne University of Technology, PO Box 218, Hawthorn, Melbourne, Australia 3122

Yun Yang is part of the Swinburne University School of Software and Electrical Engineering. His research expertise spans areas including cloud computing, workflows, distributed systems, software development environments and service-oriented computing. Alongside his teaching and research responsibilities, Professor Yang is also the leader of Swinburne’s Next Generation Software Platform focus area and Associate Editor of IEEE Transactions on Cloud Computing.

Kang Zhang, Department of Computer Science, University of Texas at Dallas, Richardson, TX 75083, USA

Kang Zhang received his B.Eng. degree in Computer Engineering from University of Electronic Science and Technology of China; and Ph.D. degree in Computer Science from the University of Brighton, UK. He is currently a professor in department of computer science, the University of Texas at Dallas, USA.

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.

Published
2020-08-20
Section
Advanced Practice in Web Engineering