Abstract
With the continuous expansion of software application range and the frequent occurrence of software security accidents, software security has become the focus of attention. This paper proposes a security software formal modeling and verification method, which uses UML to organize the basic structure of software, and uses Z specification to supply security semantics for UML model in order to support formal model verification. This method can guarantee the security of software design, while reducing the complexity of formal modeling. On this basis, this paper also introduces a website register function as case study and discovers the security flaws in the system design; the effectiveness and practicality of this method is then demonstrated.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Michael, H., David, L.: Writing Secure Code, 2nd edn. Microsoft Press, Redmond (2003)
Xu, D.: Threat-Driven Modeling and Verification of Secure Software Using Aspect-Oriented Petri Nets. IEEE Transactions on Software Engineering 32(4), 265–278 (2006)
Bau, J., Mitchell, J.C.: Security Modeling and Analysis. IEEE Security & Privacy 9(3), 18–25 (2011)
Ali, Y., El Kassas, S., Mahmoud, M.: A Rigorous Methodology for Security Architecture Modeling and Verification. In: 42nd Hawaii International Conference on System Sciences, pp. 1–10 (2009)
Burrows, M., Abadi, M., Needham, R.: A Logic of Authentication. ACM Transactions on Computer Systems 8(1), 16–18 (1990)
Classen, A., Heymans, P., Schobbens, P.-Y., Legay, A.: Symbolic Model Checking of Software Product Lines. In: 33rd International Conference on Software Engineering. ACM Network, NY (2011)
Sutcliffe, G., Gables, C.: The 5th IJCAR Automated Theorem Proving System Competition. AI Communications 24(1), 75–89 (2011)
Yoo, J., Jee, E., Cha, S.: Formal Modeling and Verification of Safety-Critical Software. IEEE Software 26(3), 42–49 (2009)
Khan, S.A., Zafar, N.A.: Towards the Formalization of Railway Interlocking System using. Z- Notations IC4, 1–6 (2009)
Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice Hall International (1996)
Bartels, B., Glesner, S.: Formal Modeling and Verification of Low-Level Software Programs. In: 10th International Conference on Quality Software, pp. 200–207 (2010)
Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating Specification and Programs for System Modeling and Verification. In: IEEE International Symposium on Theoretical Aspects of Software Engineering (2009)
Zhang, X., Liu, Y., Auguston, M.: Modeling and Analyzing Timed Security Protocols Using Extended Timed CSP. In: SSIRI 2010, pp. 217–226 (2010)
Hei, X., Chang, L., Ma, W., Gao, J., Xie, G.: Automatic Transformation from UML Statechart to Petri Nets for Safety Analysis and Verification. In: ICQR2MSE, pp. 948–951 (2011)
Moebius, N., Stenzel, K., Reif, W.: Generating Formal Specifications for Security-Critical Applications – A Model-Driven Approach. In: SESS 2009, pp. 68–74 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cao, K., Li, X., Xing, J. (2012). Security Software Formal Modeling and Verification Method Based on UML and Z. In: Khachidze, V., Wang, T., Siddiqui, S., Liu, V., Cappuccio, S., Lim, A. (eds) Contemporary Research on E-business Technology and Strategy. iCETS 2012. Communications in Computer and Information Science, vol 332. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34447-3_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-34447-3_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34446-6
Online ISBN: 978-3-642-34447-3
eBook Packages: Computer ScienceComputer Science (R0)