The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - May/June (2011 vol.9)
pp: 18-25
Jason Bau , Stanford University
John C. Mitchell , Stanford University
ABSTRACT
Security modeling centers on identifying system behavior, including any security defenses; the system adversary's power; and the properties that constitute system security. Once a security model is clearly defined, security analysis evaluates whether the adversary, interacting with the system, can defeat the desired security properties. Although the authors illustrate security analysis using model checking, analysts can use various methods and tools to evaluate system security, including manual and automated theorem-proving tools that provide assurance about the absence of attacks in a specified threat model. This article describes a uniform approach for evaluating system security and illustrates the approach by summarizing three case studies. Security modeling and analysis also provides a basis for comparative evaluation and some forms of security metrics.
INDEX TERMS
Security modeling, formal methods, model checking, security analysis
CITATION
Jason Bau, John C. Mitchell, "Security Modeling and Analysis", IEEE Security & Privacy, vol.9, no. 3, pp. 18-25, May/June 2011, doi:10.1109/MSP.2011.2
REFERENCES
1. D. Lie et al., "Specifying and Verifying Hardware for Tamper-Resistant Software," Proc. 2003 IEEE Symp. Security and Privacy, IEEE CS Press, 2003, pp. 166–177.
2. G. Klein et al., "seL4: Formal Verification of an OS Kernel," Proc. ACM SIGOPS 22nd Symp. Operating Systems Principles, ACM Press, 2009, pp. 207–220.
3. W. Shin et al., "Towards Formal Analysis of the Permission-Based Security Model for Android," Proc. 5th Int'l Conf. Wireless and Mobile Comm., IEEE CS Press, 2009, pp. 87–92.
4. D. Akhawe et al., "Towards a Formal Foundation of Web Security," Proc. 23rd IEEE Computer Security Foundations Symp., IEEE CS Press, 2010, pp. 290–304.
5. C. Flanagan and S. Qadeer, "Predicate Abstraction for Software Verification," Proc. 29th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL 02), ACM Press, 2002, pp. 191–202.
6. L.C. Paulson, "The Inductive Approach to Verifying Cryptographic Protocols," J. Computer Security, vol. 6, vol. 1–2, 1998, p. 85128.
7. M. Arnaud, V. Cortier, and S. Delaune, "Modeling and Verifying Ad Hoc Routing Protocols," Proc. 23rd IEEE Computer Security Foundations Symp., IEEE CS Press, 2010, pp. 59–74.
8. M. Bruso, K. Chatzikokolakis, and J. den Hartog, "Formal Verification of Privacy for RFID Systems," Proc. 23rd IEEE Computer Security Foundations Symp., IEEE CS Press, 2010, pp. 75–88.
9. R.M. Needham and M.D. Schroeder, "Using Encryption for Authentication in Large Networks of Computers," Comm. ACM, vol. 21, no. 12, 1978, pp. 993–999.
10. G. Lowe, "Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR," Proc. 2nd Int'l Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACA 96), Springer-Verlag, 1996, pp. 147–166.
11. D.L. Dill, "The Murphi Verification System," Proc. 8th Int'l Conf. Computer Aided Verification (CAV 96), Springer-Verlag, 1996, pp. 390–393.
12. J. Mitchell, M. Mitchell, and U. Stern, "Automated Analysis of Cryptographic Protocols Using Murphi," Proc. 1997 IEEE Symp. Security and Privacy, IEEE CS Press, 1997, pp. 141–151.
13. J. Yang et al., "Using Model Checking to Find Serious File System Errors," ACM Trans. Computer Systems, vol. 24, no. 4, 2006, pp. 393–423.
14. A. Barth, C. Jackson, and J.C. Mitchell, "Robust Defenses for Cross-Site Request Forgery," Proc. 15th ACM Conf. Computer and Comm. Security (CCS 08), ACM Press, 2008, pp. 75–88.
15. A. Barth, "The Web Origin Concept,"26 Nov. 2010; http://tools.ietf.org/htmldraft-abarth-origin .
30 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool