Reasoning about confidentiality at requirements engineering time

ABSTRACT

Growing attention is being paid to application security at requirements engineering time. Confidentiality is a particular subclass of security concerns that requires sensitive information to never be disclosed to unauthorized agents. Disclosure refers to undesired knowledge states of such agents. In previous work we have extended our requirements specification framework with epistemic constructs for capturing what agents may or may not know about the application. Roughly, an agent knows some property if the latter is found in the agent's memory.This paper makes the semantics of such constructs further precise through a formal model of how sensitive information may appear or disappear in an agent's memory. Based on this extended framework, a catalog of specification patterns is proposed to codify families of confidentiality requirements. A proof-of-concept tool is presented for early checking of requirements models against such confidentiality patterns. In case of violation, the counterexample scenarios generated by the tool show how an unauthorized agent may acquire confidential knowledge. Counter-measures should then be devised to produce further confidentiality requirements.

REFERENCES

• 1: A. Biere, A.Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, "Bounded model checking", Advances in Computers, 58, 2003.
• 2: Dominique Bolignano, Towards a Mechanization of Cryptographic Protocal Verification, Proceedings of the 9th International Conference on Computer Aided Verification, p.131-142, June 22-25, 1997
• 3: http://www.cert.org/stats/cert_stats.html.
• 4: I. Cervesato, "Data access specification and the most powerful symbolic attacker in msr", In ISSS 2002: Software Security - Theories and Systems, LNCS 2609, Springer-Verlag, November 2003, 384--416.
• 5: Marsha Chechik , Dimitrie O. Paun, Events in Property Patterns, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.154-167, September 21-24, 1999
• 6: R. De Landtsheer, "Solving CSPs including universal quantifications", Proc. of the 2nd Int. Mozart/Oz Conference, 2004.
• 7: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 8: J. Engelfriet, "Monotonicity and persistence in preferential logics", J. Artif. Intell. Res. 8, 1998, 1--21.
• 9: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 10: J. Halpern , Y. Moses, Towards a theory of knowledge and ignorance: preliminary report, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 11: Halpern J., van der Meyden R., and Vardi. Complete axiomatizations for reasoning about knowledge and time. 1997.
• 12: J. Jacob, "On the derivation of secure components", In Proc. of 1989 IEEE Symposium on Security and Privacy, Oakland, CA, May 1989.
• 13: Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
• 14: Natasha Alechina , Brian Logan , Mark Whitsey, A Complete and Decidable Logic for Resource-Bounded Agents, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, p.606-613, July 19-23, 2004, New York, New York [doi>10.1109/AAMAS.2004.8]
• 15: E. M. Clarke , S. Jha , W. Marrero, Verifying security protocols with Brutus, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.443-487, Oct. 2000 [doi>10.1145/363516.363528]
• 16: U. Junker, "QUICKXPLAIN: Conflict Detection for Arbitrary Constraint Propagation Algorithms", Proc. IJCAI'01 Workshop on Modeling and Solving Problems with Constraints, 2001.
• 17: R. Kemmerer, C. Meadows, and J. Millen, "Three systems for cryptographic protocol analysis", Journal of Cryptology 7(2), 1994, 79--130.
• 18: Richard A. Kemmerer, Cybersecurity, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 19: Axel van Lamsweerde , Emmanuel Letier, Handling Obstacles in Goal-Oriented Requirements Engineering, IEEE Transactions on Software Engineering, v.26 n.10, p.978-1005, October 2000 [doi>10.1109/32.879820]
• 20: Axel Van Lamsweerde, Goal-Oriented Requirements Engineering: A Guided Tour, Proceedings of the Fifth IEEE International Symposium on Requirements Engineering (RE '01), p.249, August 27-31, 2001
• 21: A. van Lamsweerde, "From System Goals to Software Architecture", In Formal Methods for Software Architectures, M. Bernardo & P. Inverardi (eds), LNCS 2804, Springer-Verlag, 2003, 25--43.
• 22: Axel van Lamsweerde, Elaborating Security Requirements by Construction of Intentional Anti-Models, Proceedings of the 26th International Conference on Software Engineering, p.148-157, May 23-28, 2004
• 23: Emmanuel Letier , Axel van Lamsweerde, Deriving operational software specifications from system goals, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587070]
• 24: Lin Liu , Eric Yu , John Mylopoulos, Security and Privacy Requirements Analysis within a Social Setting, Proceedings of the 11th IEEE International Conference on Requirements Engineering, p.151, September 08-12, 2003
• 25: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 26: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 27: A. Pnueli, "Verification by Finitary Abstraction", Proc. SPIN'98: 4th Intl. SPIN Workshop, Paris, Nov. 1998.
• 28: Ch. Schulte. Programming Constraint Services. Lecture Notes in Artificial Intelligence Vol. 2302,. Springer-Verlag, Berlin, 2002.
• 29: Peter Van Roy , Seif Haridi, Concepts, Techniques, and Models of Computer Programming, MIT Press, Cambridge, MA, 2004
• 30: J. Viega and G. McGraw. Building Secure Software: How to Avoid Security Problems the Right Way. Addison-Wesley, 2001.
• 31: Jeannette M. Wing, A Symbiotic Relationship Between Formal Methods and Security, Proceedings of the Conference on Computer Security, Dependability, and Assurance: From Needs to Solutions, p.26, July 09-11, 1998

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Languages; Tools

General Terms:
Design, Languages, Security, Verification

Keywords:
bounded model checking, reasoning about confidentiality, security requirements, specification patterns