This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Threat-Driven Modeling and Verification of Secure Software Using Aspect-Oriented Petri Nets
April 2006 (vol. 32 no. 4)
pp. 265-278
ASCII Text
x 
 
Dianxiang Xu, Kendall E. Nygard, "Threat-Driven Modeling and Verification of Secure Software Using Aspect-Oriented Petri Nets," IEEE Transactions on Software Engineering, vol. 32, no. 4, pp. 265-278, April, 2006.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2006.40,
author = {Dianxiang Xu and Kendall E. Nygard},
title = {Threat-Driven Modeling and Verification of Secure Software Using Aspect-Oriented Petri Nets},
journal ={IEEE Transactions on Software Engineering},
volume = {32},
number = {4},
issn = {0098-5598},
year = {2006},
pages = {265-278},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2006.40},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Threat-Driven Modeling and Verification of Secure Software Using Aspect-Oriented Petri Nets
IS - 4
SN - 0098-5598
SP265
EP278
EPD - 265-278
A1 - Dianxiang Xu,
A1 - Kendall E. Nygard,
PY - 2006
KW - Software security
KW - modeling
KW - verification
KW - threat modeling
KW - Petri nets
KW - aspect-oriented Petri nets
KW - aspect-oriented software development.
VL - 32
JA - IEEE Transactions on Software Engineering
ER -
 
Design-level vulnerabilities are a major source of security risks in software. To improve trustworthiness of software design, this paper presents a formal threat-driven approach, which explores explicit behaviors of security threats as the mediator between security goals and applications of security features. Security threats are potential attacks, i.e., misuses and anomalies that violate the security goals of systems' intended functions. Security threats suggest what, where, and how security features for threat mitigation should be applied. To specify the intended functions, security threats, and threat mitigations of a security design as a whole, we exploit aspect-oriented Petri nets as a unified formalism. Intended functions and security threats are modeled by Petri nets, whereas threat mitigations are modeled by Petri net-based aspects due to the incremental and crosscutting nature of security features. The unified formalism facilitates verifying correctness of security threats against intended functions and verifying absence of security threats from integrated functions and threat mitigations. As a result, our approach can make software design provably secured from anticipated security threats and, thus, reduce significant design-level vulnerabilities. We demonstrate our approach through a systematic case study on the threat-driven modeling and verification of a real-world shopping cart application.

[1] I. Alexander, “Misuse Cases: Use Cases with Hostile Intent,” IEEE Software, pp. 58-66, Jan./Feb. 2003.
[2] J. Allen et al., “State of the Practice of Intrusion Detection Technologies,” Technical Report CMU/SEI-99-TR-028, 2000.
[3] L. Buttyan, “Formal Methods in the Design of Cryptographic Protocols— State of the Art,” Technical Report No. SSC/1999/038, Inst. Computer Comm. and Applications, Swiss Federal Inst. Tech nology, 1999.
[4] H. Chen, D. Dean, and D. Wagner, “Model Checking One Million Lines of C Code,” Proc. 11th Ann. Network and Distributed System Security Symp., pp. 171-185, 2004.
[5] B. De Win, B. Vanhaute, and B. De Decker, “Security through Aspect-Oriented Programming,” Advances in Network and Distributed Systems Security, pp. 125-138, 2001.
[6] Y. Deng, J. Wang, J. Tsai, and J.K. Beznosov, “An Approach for Modeling and Analysis of Security System Architectures,” IEEE Trans. Knowledge and Data Eng., vol. 15, no. 5, pp. 1099-1119, Sept./Oct. 2003.
[7] P.T. Devanbu and S. Stubblebine, “Software Engineering for Security: A Roadmap,” The Future of Software Eng., pp. 227-239, 2000.
[8] J. Ding, D. Xu, Y. Deng, P.J. Clarke, and X. He, “Design an Interoperable Mobile Agent System Based on Predicate Transition Net Models,” Proc. 17th Int'l Conf. Software Eng. and Knowledge Eng. pp. 560-565, July, 2005.
[9] Department of Defense Trusted Computer System Evaluation Criteria, (a.k.a. “The Orange Book”), US Dept. of Defense Standard 5200.28-STD, 1985, http://www. radium. ncsc. mil/tpep/library rainbow.
[10] D. Dolev and A. Yao, “On the Security of Public Key Protocols,” IEEE Trans. Information Theory, vol. 29, no. 2, pp. 198-208, 1983.
[11] R.J. Feiertag and P.G. Neumann, “The Foundations of a Provably Secure Operating System (PSOS),” Proc. Nat'l Computer Conf., pp. 329-334, 1979.
[12] R.E. Filman, T. Elrad, S. Clarke, and M. Aksit, Aspect-Oriented Software Development. Addison-Wesley, 2005.
[13] D.G. Firesmith, “Security Use Cases,” J. Object-Technology, vol. 2, no. 3, pp. 53-64, 2003.
[14] Garner Group, Quotation at htpp:/www.securityinnovation. com.
[15] H.J. Genrich, “Predicate/Transition Nets,” Petri Nets: Central Models and Their Properties, W. Brauer, W. Resig, and G. Rozenberg, eds., pp. 207-247, 1987.
[16] D. Gollmann, “Facets of Security,” Global Computing, C. Priami, ed., pp. 192-202. Springer-Verlag, 2003.
[17] C.B. Haley, R.C. Laney, and B. Nuseibeh, “Deriving Security Requirements from Crosscutting Threat Descriptions,” Proc. Int'l Conf. Aspect-Oriented Software Development, pp. 112-121, 2004.
[18] X. He, “A Formal Definition of Hierarchical Predicate Transition Nets,” Application and Theory of Petri Nets, pp. 212-229, 1996,
[19] G. Helmer, J. Wong, M. Slagell, V. Honavar, L. Miller, and R. Lutz, “A Software Fault Tree Approach to Requirements Analysis of an Intrusion Detection System,” Requirements Eng., vol. 7, no. 4, pp. 177-220, 2002.
[20] Y. Ho, D. Frincke, and D. TobinJr., “Planning, Petri Nets, and Intrusion Detection,” Proc. 21st Nat'l Information Systems Security Conf., 1998.
[21] G. Hoglund and G. McGraw, Exploiting Software: How to Break Code. Addison-Wesley, 2004.
[22] M. Howard and D. Leblanc, Writing Secure Code, second ed. Microsoft Press, 2003.
[23] I. Jacobson, M. Christerson, P. Jonsson, and G. Overgaard, Object-Oriented Software Engineering: A Use Case Driven Approach. Addison-Wesley, 1994.
[24] K. Jensen, Coloured Petri Nets: Basic Concepts, Analysis Methods And Practical Use, vol. 26. Springer-Verlag, 1992.
[25] G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C.V. Lopes, J.M. Loingtier, and J. Irwin, “Aspect Oriented Programming,” Proc. European Conf. Object-Oriented Programming, pp. 220-242, 1997.
[26] C.E. Landwehr, “Formal Models for Computer Security,” ACM Computing Surveys, vol. 13, no. 3, pp. 247-278, 1981.
[27] T. Lodderstedt, D. Basin, and J. Doser, “SecureUML: A UML-Based Modeling Language for Model-Driven Security,” Proc. Unified Modeling Language Conf., 2002.
[28] V. Lotz, “Threat Scenarios as a Means to Formally Develop Secure Systems,” J. Computer Security, vol. 5, pp. 31-67, 1997.
[29] M.A. Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, Modeling with Generalized Stochastic Petri Nets. John Wiley and Sons, 1995.
[30] S. McClure, S. Shah, and S. Shah, Web Hacking: Attacks And Defense. Addison-Wesley, 2003.
[31] J. McDermott, “Abuse-Case-Based Assurance Arguments,” Proc. 17th Ann. Computer Security Application Conf., pp. 366-374, 2001.
[32] J. McDermott, “Attack Net Penetration Testing,” Proc. Workshop New Security Paradigms, pp. 15-21, 2000.
[33] T. Murata, “Petri Nets: Properties, Analysis and Applications,” Proc. IEEE, vol. 77, no. 4, pp. 541-580, 1989.
[34] P.G. Neumann, Principled Assuredly Trustworthy Composable Architectures, project report, computer science laboratory, SRI Int'l, 2004.
[35] J. Pauli and D. Xu, “Threat-Driven Architectural Design of Secure Information Systems,” Proc. Seventh Int'l Conf. Enterprise Information Systems, pp. 136-143, 2005.
[36] I. Ray, R. France, N. Li, and G. Georg, “An Aspect-Based Approach to Modeling Access Control Concerns,” Information and Software Technology, vol. 46, no. 9, pp. 575-587, 2004.
[37] B. Schneier, “Attack Trees,” Dr. Dobb's J. Software Tools, vol. 24, no. 12, pp. 21-29, 1999.
[38] O. Sheyner and J. Wing, “J. Tools for Generating and Analyzing Attack Graphs,” Proc. Symp. Formal Methods for Components and Objects, pp. 344-371, 2004.
[39] G. Sindre and A.L. Opdahl, “Eliciting Security Requirements by Misuse Cases,” Proc. Conf. Technology of Object-Oriented Languages and Systems, pp. 120-131, 2000.
[40] F. Swiderski and W. Snyder, Threat Modeling. Microsoft Press, 2004.
[41] A. Van Lamsweerde, “Elaborating Security Requirements by Construction of Intentional Anti-Models,” Proc. Int'l Conf. Software Eng., pp. 148-157, 2004.
[42] J. Viega and G. McGraw, Building Secure Software: How to Avoid Security Problems in the Right Way. Addison Wesley, 2002.
[43] J. Viega, J.T. Bloch, and P. Chandra, ”Applying Aspect-Oriented Programming to Security,” Cutter IT J., vol. 14, no. 2, pp. 31-39, 2001.
[44] C. Weissman, Handbook for the Computer Security Certification of Trusted Systems, NRL Technical Memorandum 5540:082A, security penetration testing guideline, 1995.
[45] J. Wing, “A Symbiotic Relationship between Formal Methods and Security,” Proc. NSF Workshop Computer Security, Fault Tolerance, and Software Assurance: From Needs to Solution, 1998.
[46] X. Xie and S.M. Shatz, “An Approach to Using Formal Methods in Aspect Orientation,” Proc. Int'l Conf. Parallel and Distributed Processing Techniques and Applications, pp. 263-269, 2000.
[47] D. Xu, R.A. Volz, T.R. Joerger, and J. Yen, “Modeling and Analyzing Multi-Agent Behaviors Using Predicate/Transition Nets,” Int'l J. Software Eng. Knowledge Eng., vol. 13, no. 1, pp. 103-124, 2003.
[48] D. Xu, J. Yin, Y. Deng , and J. Ding, “A Formal Architectural Model for Logical Agent Mobility,” IEEE Trans. Software Eng., vol. 29, no. 1, pp. 31-45, Jan. 2003.

Index Terms:
Software security, modeling, verification, threat modeling, Petri nets, aspect-oriented Petri nets, aspect-oriented software development.
Citation:
Dianxiang Xu, Kendall E. Nygard, "Threat-Driven Modeling and Verification of Secure Software Using Aspect-Oriented Petri Nets," IEEE Transactions on Software Engineering, vol. 32, no. 4, pp. 265-278, April 2006, doi:10.1109/TSE.2006.40
Usage of this product signifies your acceptance of the Terms of Use.