Formal Methods for Security Engineering
In addition to functional requirements, one needs to consider aspects like confidentiality, integrity, and availability during the development of security-critical systems. Such security aspects are not properly addressed during system development so far. This is one of the main reasons why we are facing so many security problems in current IT systems.
Our aim in the project FM-SecEng (funded by the German Research Foundation - DFG) is to develop a formally justified basis for respecting security aspects throughout the software development process and for a global, i.e. system-wide, consideration of security requirements. We develop methods, techniques, and tools that can be applied in a security engineering process in order to improve the security of the resulting IT systems.
A software engineer faces several problems when applying a security engineering process. For instance, the following questions arise when security requirements are considered throughout the development process:
- Which security requirements are critical for the system under development and how can these requirements be formally specified in an adequate way?
- Which architecture should be chosen and which security mechanisms should be employed in order to simplify the treatment of security during further system development or for simplifying a formal verification of the system?
- Which is the most efficient way of verifying a given system against its requirements?
For instance, the following questions arise in a system-wide consideration of security requirements
- How does a given system component or a given security mechanism contribute to the security (or insecurity) of the overall system?
- What is the significance of the results from the analysis of an abstract system model for the actual system?
Our plans include, for instance,
- to investigate the extent to which the known information flow properties (noninterference and its variants) are adequate for capturing typical security requirements and, possibly, to further widen the application spectrum by modifying the known properties,
- to develop criteria that provide guidance in the formal specification of security requirements,
- to derive mathematically justified methods and techniques for the stepwise development of secure systems (refinement and composition),
- to develop guidelines that support the software engineer in choosing a suitable system architecture and security mechanisms, and
- to develop tools for the automated security analysis of concrete programs and to evaluate them in practice.
Information flow properties and stepwise development of secure systems
- Heiko Mantel. On the Composition of Secure Systems. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, pp. 88-101, May 12-15, 2002
- Annalisa Bossi, Riccardo Focardi, Carla Piazza, Sabina Rossi. Refinement Operators and Information Flow Security. In Proceedings of the International Conference on Software Engineering and Formal Methods, SEFM, pp. 44-53, 2003.
- Heiko Mantel. Preserving Information Flow Properties under Refinement. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, pp. 78-91, May 14-16, 2001.
- Andrei Sabelfeld, Andrew C. Myers. Language-based Information-Flow Security. IEEE Journal on Selected Areas in Communication, 21(1):5--19, 2003.
- Andrei Sabelfeld and David Sands. Probabilistic Noninterference for Multi-threaded Programs. In Proceedings of the 13th IEEE Computer Security Foundations Workshop, pages 200--215, Cambridge, UK, 2000.
- Heiko Mantel, David Sands. Controlled Declassification based on Intransitive Noninterference. In Proceedings of the 2nd ASIAN Symposium on Programming Languages and Systems, APLAS 2004, Taipei, Taiwan, LNCS 3302, pp. 129-145, November 4-6, 2004.
Print
Imprint
Sitemap
Contact