Security policy analysis using deductive spreadsheets

ABSTRACT

As security policies get larger and more complex, analysis tools that help users understand and validate security policies are becoming more important.This paper explores the use of deductive spreadsheets for security policy analysis.Deductive spreadsheets combine the power ofdeductive rules (for specifying policies and analyses) with the usability of spreadsheets.This approach is introduced with a simple example of analyzing information flow allowed by RBAC policies and then applied in two case studies: analysis of computer system configurations and analysisof Security-Enhanced Linux access control policies.

REFERENCES

• 1: Moritz Y. Becker , Peter Sewell, Cassandra: Flexible Trust Management, Applied to Electronic Health Records, Proceedings of the 17th IEEE workshop on Computer Security Foundations, p.139, June 28-30, 2004 [doi>10.1109/CSFW.2004.7]
• 2: Gopal Gupta , Shameem F. Akhter, Knowledgesheet: A Graphical Spreadsheet Interface for Interactively Developing a Class of Constraint Programs, Proceedings of the Second International Workshop on Practical Aspects of Declarative Languages, p.308-323, January 01, 2000
• 3: J. D. Guttman, A. L. Herzog, and J. D. Ramsdell. Information flow in operating systems: Eager formal methods. In Workshop on Issues in the Theory of Security (WITS), 2003.
• 4: J. D. Guttman, A. L. Herzog, and J. D. Ramsdell. SLAT: Information flow in Security Enhanced Linux, 2003. Available from http://www.mitre.org/tech/selinux/.
• 5: Trent Jaeger , Xiaolan Zhang , Antony Edwards, Policy management using access control spaces, ACM Transactions on Information and System Security (TISSEC), v.6 n.3, p.327-364, August 2003 [doi>10.1145/937527.937528]
• 6: Trent Jaeger , Reiner Sailer , Xiaolan Zhang, Analyzing integrity protection in the SELinux example policy, Proceedings of the 12th conference on USENIX Security Symposium, p.5-5, August 04-08, 2003, Washington, DC
• 7: B. Jayaraman and K. Moon. Subset logic programs and their implementation. J. Log. Program., 42(2):71--110, 2000.
• 8: Simon Peyton Jones , Alan Blackwell , Margaret Burnett, A user-centred approach to functions in Excel, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.165-176, August 25-29, 2003, Uppsala, Sweden
• 9: Michael Kassoff , Lee-Ming Zen , Ankit Garg , Michael Genesereth, PrediCalc: a logical spreadsheet management system, Proceedings of the 31st international conference on Very large data bases, August 30-September 02, 2005, Trondheim, Norway
• 10: A. Kissinger and J. Hale. Lopol: A deductive database approach to policy analysis and rewriting. In 2006 Security Enhanced Linux Symposium, 2006.
• 11: P. Loscocco and S. Smalley. Meeting critical security objectives with security-enhanced Linux. In Proc. of 2001 Ottawa Linux Symposium, 2001. Available from http://www.nsa.gov/selinx/.
• 12: David Maier , David S. Warren, Computing with logic: logic programming with Prolog, Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1988
• 13: D. Merrit, J. Paine, and M. Kassof. Special Spreadsheet Issue of AI Expert Newsletter, May 2005. http://www.ainewsletter.com/newsletters/aix_0505.htm.
• 14: Prasad Naldurg , Stefan Schwoon , Sriram Rajamani , John Lambert, NETRA:: seeing through access control, Proceedings of the fourth ACM workshop on Formal methods in security, p.55-66, November 03-03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180337.1180343]
• 15: Xinming Ou , Sudhakar Govindavajhala , Andrew W. Appel, MulVAL: a logic-based network security analyzer, Proceedings of the 14th conference on USENIX Security Symposium, p.8-8, July 31-August 05, 2005, Baltimore, MD
• 16: Quantrix. http://www.quantrix.com/.
• 17: C. R. Ramakrishnan, I. V. Ramakrishnan, and D. S. Warren. Deductive spreadsheets using tabled logic programming. In 22nd International Conference on Logic Programming (ICLP), volume 4079 of Lecture Notes in Computer Science, pages 391--405. Springer-Verlag, 2006.
• 18: D. Saha and C. R. Ramakrishnan. Incremental evaluation of tabled prolog: Beyond pure logic programs. In PADL, volume 3819 of Lecture Notes in Computer Science, pages 215--229. Springer, 2006.
• 19: Ravi S. Sandhu , Edward J. Coyne , Hal L. Feinstein , Charles E. Youman, Role-Based Access Control Models, Computer, v.29 n.2, p.38-47, February 1996 [doi>10.1109/2.485845]
• 20: B. Sarna-Starosta and S. D. Stoller. Policy analysis for security-enhanced linux. In Proceedings of the 2004 Workshop on Issues in the Theory of Security (WITS), pages 112, April 2004. Available at http: //www.cs.sunysb.edu/~stoller/WITS2004.html.
• 21: J. T. Schwartz , R. B. Dewar , E. Schonberg , E. Dubinsky, Programming with sets; an introduction to SETL, Springer-Verlag New York, Inc., New York, NY, 1986
• 22: Tresys Technology. Policy tools for Security-Enhanced Linux. Available from http://www.tresys.com/selinux/.
• 23: Tresys Technology. Security-Enhanced Linux reference policy. Available from http://oss.tresys.com/projects/refpolicy.
• 24: J. Whaley, D. Avots, M. Carbin, and M. S. Lam. Using Datalog with binary decision diagrams for program analysis. In Third Asian Symposium on Programming Languages and Systems (APLAS), volume 3780 of Lecture Notes in Computer Science, pages 97--118. Springer-Verlag, 2005.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation
      D.2.6 Programming Environments
          Subjects: Graphical environments
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Information flow controls

General Terms:
Languages, Security, Verification

Keywords:
SELinux policy, security policy analysis, vulnerability analysis