Property-testing real-world authorization systems
Pages 225 - 236
Abstract
We motivate and address the problem of testing for properties of interest in real-world implementations of authorization systems. We adopt a 4-stage process: (1) express a property precisely using existential second-order logic, (2) establish types of traces that are necessary and sufficient to establish a property, (3) adopt finitizing assumptions and show that under those assumptions, verifying a property is in PSPACE, and, (4) use a model-checker as a trace-generator to generate instances of traces, and exercise the implementation to check for those traces. We discuss our design of a corresponding testing-system, and its use to test for qualitatively different kinds of properties in two commercial authorization systems. One is a database system that we call the D system, and the other is a file-sharing system that we call the I system. (We use pseudonyms at the request of the respective vendors.) In the context of the D system, our testing has uncovered several issues with its authorization system in the context of procedures that aggregate SQL statements that, to our knowledge, are new to the research literature. For the I system, we have established that it possesses several properties of interest.
References
[1]
Nusmv. http://nusmv.fbk.eu/.
[2]
Mihhail Aizatulin, Andrew D. Gordon, and Jan Jürjens. Extracting and verifying cryptographic models from c protocol code by symbolic execution. In Proceedings of the 18th ACM conference on Computer and communications security, CCS '11, pages 331--340, New York, NY, USA, 2011. ACM.
[3]
Chris Anley. Advanced sql injection in sql server applications. White paper, Next Generation Security Software Ltd, 2002.
[4]
Lujo Bauer, Yuan Liang, Michael K. Reiter, and Chad Spensky. Discovering access-control misconfigurations: New approaches and evaluation methodologies. In CODASPY'12: Proceedings of the Second ACM Conference on Data and Application Security and Privacy, February 2012. To appear.
[5]
Hao Chen, David Wagner, and Drew Dean. Setuid demystified. In USENIX Security Symposium, pages 171--190, 2002.
[6]
Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT Press, 2001.
[7]
Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms (3. ed.). MIT Press, 2009.
[8]
E. M. Fayo. Advanced sql injection in oracle databases. Technical report, Argeniss Information Security, Black Hat Briefings, 2005.
[9]
Michael Huth and Mark Dermot Ryan. Logic in computer science - modelling and reasoning about systems (2. ed.). Cambridge University Press, 2004.
[10]
D. Jackson and C.A. Damon. Elements of style: analyzing a software design feature with a counterexample detector. Software Engineering, IEEE Transactions on, 22(7):484--495, jul 1996.
[11]
Yongdae Kim, Adrian Perrig, and Gene Tsudik. Simple and fault-tolerant key agreement for dynamic collaborative groups. In Proceedings of the 7th ACM Conference on Computer and Communications Security (CCS 2000), pages 235--244, November 2000.
[12]
Ninghui Li and Mahesh V. Tripunitara. Security analysis in role-based access control. ACM Transactions on Information and Systems Security (TISSEC), 9(4):391--420, November 2006.
[13]
Richard R. Linde. Operating system penetration. In Proceedings of the May 19--22, 1975, national computer conference and exposition, AFIPS '75, pages 361--368, New York, NY, USA, 1975. ACM.
[14]
Jianwei Niu, Ravi Sandhu, Ram Krishnan, and William H. Winsborough. Group-centric secure information sharing models for isolated groups. ACM Transactions on Information and System Security, 14(3):1--29, November 2011.
[15]
Corina S. Pasareanu. Combining model checking and symbolic execution for software testing. In Achim D. Brucker and Jacques Julliand, editors, TAP, volume 7305 of Lecture Notes in Computer Science, page 2. Springer, 2012.
[16]
Walter L. Ruzzo, Michael A. Harrison, and Jeffrey D. Ullman. Protection in operating systems. Communications of the ACM, 19(8):461--471, August 1976.
[17]
Ravi S. Sandhu. Undecidability of the safety problem for the schematic protection model with cyclic creates. Journal of Computer and System Sciences, 44(1):141--159, February 1992.
[18]
Deepak D. Souza, Raveendra Holla, K. R. Raghavendra, and Barbara Sprick. Model-checking trace-based information flow properties. Journal of Computer Security, 19(1):101--138, January 2011.
[19]
Wuliang Sun, Robert B. France, and Indrakshi Ray. Rigorous analysis of uml access control policy models. In POLICY, pages 9--16. IEEE Computer Society, 2011.
[20]
Lijun Yu, Robert B. France, Indrakshi Ray, and Wuliang Sun. Systematic scenario-based analysis of uml design class models. In Isabelle Perseil, Karin Breitman, and Marc Pouzet, editors, ICECCS, pages 86--95. IEEE Computer Society, 2012.
Index Terms
- Property-testing real-world authorization systems
Recommendations
Invariance in property testing
Property testingProperty testing considers the task of testing rapidly (in particular, with very few samples into the data), if some massive data satisfies some given property, or is far from satisfying the property. For "global properties", i.e., properties that ...
Invariance in property testing
Property testingProperty testing considers the task of testing rapidly (in particular, with very few samples into the data), if some massive data satisfies some given property, or is far from satisfying the property. For "global properties", i.e., properties that ...
A complete characterization of deterministic regular liveness properties
Many systems can be modeled formally by nondeterministic Buchi-automata. The complexity of model checking then essentially depends on deciding subset conditions on languages that are recognizable by these automata and that represent the system behavior ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2013
278 pages
ISBN:9781450319508
DOI:10.1145/2462410
- General Chair:
- Mauro Conti,
- Program Chairs:
- Jaideep Vaidya,
- Andreas Schaad
Copyright © 2013 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 12 June 2013
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
SACMAT '13
Sponsor:
SACMAT '13: 18th ACM Symposium on Access Control Models and Technologies
June 12 - 14, 2013
Amsterdam, The Netherlands
Acceptance Rates
SACMAT '13 Paper Acceptance Rate 19 of 62 submissions, 31%;
Overall Acceptance Rate 177 of 597 submissions, 30%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 185Total Downloads
- Downloads (Last 12 months)1
- Downloads (Last 6 weeks)0
Reflects downloads up to 22 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in