Secure systems development based on the common criteria: the PalME project

ABSTRACT

Security is a very important issue in information processing, especially in open network environments like the Internet. The Common Criteria (CC)is the standard requirements catalogue for the evaluation of security critical systems. Using the CC, a large number of security requirements on the system itself and on the system development can be defined. However, the CC does not give methodological support. In this paper, we show how integrate security aspects into the software engineering process. The activities and documents from the Common Criteria are tightly intertwined with the system development, which improves the quality of the developed system and reduces the additional cost and effort due to high security requirements. For modelling and verification of critical parts of the system, we use formal description techniques and model checking (supported by the graphical CASE tool AutoFocus, which increases both the understanding of the system specification and the system's reliability. We demonstrate our ideas by means of a case-study, the PalME project---an electronic purse application for Palm handhelds.

REFERENCES

• 1: Ross J. Anderson, Security Engineering: A Guide to Building Dependable Distributed Systems, John Wiley & Sons, Inc., New York, NY, 2001
• 2: M. Burrows, M. Abadi, and R. Needham. A logic of authentication. Proceedings of the Royal Society of London A, 426:233--271, 1989.
• 3: Common criteria for information technology security evaluation version 2.1. Technical report, 1999. URL: http://www.commoncriteria.org/docs/index.html.
• 4: Common criteria for information technology security evaluation supplement: Vulnerability analysis and penetration testing. Technical report, 2002. URL: http://www.commoncriteria.org/review_docs/index.html.
• 5: Desmond F. D'Souza , Alan Cameron Wills, Objects, components, and frameworks with UML: the catalysis approach, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998
• 6: Michael Gnatz , Frank Marschall , Gerhard Popp , Andreas Rausch , Wolfgang Schwerin, Towards a Living Software Development Process Based on Process Patterns, Proceedings of the 8th European Workshop on Software Process Technology, p.182-202, June 19-21, 2001
• 7: S. Molterer, A. Rausch, B. Schätz F. Hube , O. Slotosch, Tool Supported Specification and Simulation of Distributed Systems, Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems, p.155, April 20-21, 1998
• 8: Franz Huber , Sascha Molterer , Bernhard Schätz , Oscar Slotosch , Alexander Vilbig, Traffic Lights - An AutoFocus Case Study, Proceedings of the 1998 International Conference on Application of Concurrency to System Design, p.282, March 23-26, 1998
• 9: IABG. V-Modell 97, 1999. URL: http://www.v-modell.iabg.de/ (in German).
• 10: ITSEC. Information Technology Security Evaluation Criteria---Harmonised Criteria of France, Germany, the Netherlands, the United Kingdom, May 1990. Version 1.
• 11: Jan Jürjens , Guido Wimmel, Security Modelling for Electronic Commerce: The Common Electronic Purse Specifications, Proceedings of the IFIP Conference on Towards The E-Society: E-Commerce, E-Business, E-Government, p.489-506, October 03-05, 2001
• 12: 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
• 13: Donal O'Mahony , Michael Pierce , Hitesh Tewari , Michael Peirce, Electronic Payment Systems, Artech House, Inc., Norwood, MA, 1997
• 14: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 15: PalME-Team. PalME secure Palm-based Money Exchange -- Project Homepage, 2001. URL: http://www4.in.tum.de/ palme/ (in German).
• 16: Lawrence C. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, v.6 n.1-2, p.85-128, Sept. 1998
• 17: Jan Philipps , Oscar Slotosch, The Quest for Correct Systems: Model Checking of Diagrams and Datatypes, Proceedings of the Sixth Asia Pacific Software Engineering Conference, p.449, December 07-10, 1999
• 18: Oscar Slotosch, QUEST: Overview over the Project, Proceedings of the International Workshop on Current Trends in Applied Formal Method: Applied Formal Methods, p.346-350, October 07-09, 1998
• 19: Ian Sommerville, Software Engineering, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1989
• 20: William Swartout , Robert Balzer, On the inevitable intertwining of specification and implementation, Communications of the ACM, v.25 n.7, p.438-440, July 1982 [doi>10.1145/358557.358572]
• 21: M. Vetterling. Security Engineering nach den Common Criteria --- eine Fallstudie. Master's thesis, Technische Universität München, Aug. 2001.
• 22: G. Wimmel, H. Lötzbeyer, A. Pretschner, and O. Slotosch. Specification Based Test Sequence Generation with Propositional Logic. Journal on Software Testing Verification and Reliability, 10, 2000.
• 23: Guido Wimmel , Alexander Wisspeintner, Extended description techniques for security engineering, Proceedings of the 16th international conference on Information security: Trusted information: the new decade challenge, June 11-13, 2001, Paris, France

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
      D.2.2 Design Tools and Techniques
      D.2.4 Software/Program Verification

General Terms:
Design, Documentation, Experimentation, Security, Verification

Keywords:
AutoFocus, CASE, case study, common criteria, development process, formal methods, graphical description techniques, requirements engineering, security engineering, software design, software engineering