Formal Methods for Security Engineering (FM-SecEng)
| Principal Investigator: | Prof. Dr.-Ing. Heiko Mantel |
| Funded by: | DFG (German Research Foundation), within the Computer Science Action Program (Aktionsplan Informatik) |
| Project Duration: | 01.08.2005–31.05.2013 |
Project Summary
During the development of security-critical software systems, security aspects like confidentiality, integrity, and availability need to be addressed in addition to functional and other non-functional requirements. The goal of the FM-SecEng-project was to develop novel methods, techniques, and tools that support security engineering, i.e., the development of security-critical systems. The overall objective of the project was to contribute to more trustworthy software systems by enabling the derivation of reliable, end-to-end security guarantees based on formal methods.
The scope of FM-SecEng ranged from the formal definition of security requirements by security properties through the step-wise development of software systems by composition and refinement to the verification of critical security requirements for concrete programs and for more abstract system specifications. The work-program was structured into three areas:
- Security Properties,
- Stepwise System Development, and
- Security Analysis.
Within the project area A) Security Properties, the focus was on the specification of security requirements based on information-flow properties. The scientific goals were to improve the understanding of this important class of security properties, based on both concrete examples and theoretical studies; to augment the application spectrum of information-flow properties by identifying novel properties as well as by providing adequate formal definitions of them; and to support engineers in employing information-flow properties during the development of security-critical systems, from the choice of a suitable property to the use of this property.
Within the project area B) Stepwise System Development, the focus was, firstly, on clarifying the interplay between security and stepwise system development and, secondly, on supporting the rigorous treatment of security aspects in stepwise system development. More concretely, the main foundational questions were how security is affected in detail by composition and refinement (it had been known already that, in general, composition and refinement both do not preserve security); which security properties can be established by employing particular security mechanisms; and how security interacts with other system requirements.
Within the project area C) Security Analysis, the focus was on the verification of security properties, from the study of existing program analysis and verification techniques to the development of novel security analyses and their prototypical implementation. The scientific goals were to achieve a deeper understanding of the pros and cons of existing program analyses, in particular of the various security type systems; to investigate and to elaborate other possibilities for verifying information-flow security than security type systems; and to develop techniques that security engineers can employ for removing certain insecurities from systems.
Relevant Publications
- Richard Gay, Heiko Mantel and Henning Sudbrock. An Empirical Bandwidth Analysis of Interrupt-Related Covert Channels. In International Journal of Secure Software Engineering (IJSSE), 6(2), pages 1-22, 2015.
[ BibTeX entry ] - Richard Gay, Jinwei Hu and Heiko Mantel. CliSeAu: Securing Distributed Java Programs by Cooperative Dynamic Enforcement. In Proceedings of the 10th International Conference on Information Systems Security (ICISS). LNCS 8880, pages 378-398. Springer, 2014.
[ BibTeX entry | PDF ] - Richard Gay, Heiko Mantel and Henning Sudbrock. An Empirical Bandwidth Analysis of Interrupt-Related Covert Channels. In Proceedings of the 2nd International Workshop on Quantitative Aspects in Security Assurance (QASA), 2013.
[ BibTeX entry | PDF ] - Heiko Mantel and Henning Sudbrock. Types vs. PDGs in Information Flow Analysis. In Post-Proceedings of the 22nd International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2012). LNCS 7844, pages 106-121. Springer, 2013.
[ BibTeX entry | PDF | Addendum ] - Barbara Sprick and Daniel Staesche. Verifying Information Flow Security in Visibly Pushdown Automata. TU Darmstadt, Technical Report TUD-CS-2013-0275, 2013.
[ BibTeX entry | PDF ] - Henning Sudbrock. Compositional and Scheduler-Independent Information Flow Security. Ph.D. Thesis, Technische Universität Darmstadt, 2013.
[ BibTeX entry | PDF ] - Richard Gay, Heiko Mantel and Barbara Sprick. Service Automata. In Post-Proceedings of the 8th International Workshop on Formal Aspects of Security and Trust (FAST 2011). LNCS 7140, pages 148-163. Springer, 2012.
[ BibTeX entry | PDF | Proofs ] - Martin Ochoa, Sebastian Pape, Thomas Ruhroth, Barbara Sprick, Kurt Stenzel and Henning Sudbrock. Report on the RS3 Topic Workshop ``Security Properties in Software Engineering''. Universität Augsburg, Technical Report 2012-02, 2012.
[ BibTeX entry ] - Markus Aderhold, Serge Autexier and Heiko Mantel (Ed.). Proceedings of the 6th International Verification Workshop (VERIFY 2010). EPiC Series in Computer Science, Vol. 3, 2012. Workshop in connection with the Federated Logic Conference (FLoC 2010).
[ BibTeX entry ] - Deepak D'Souza, Ravindra Holla, Raghavendra KR and Barbara Sprick. Model Checking Trace Based Information Flow Properties. In Journal of Computer Security (JCS), 19(1), pages 101-138, 2011.
[ BibTeX entry ] - Heiko Mantel. Information Flow and Noninterference. In Encyclopedia of Cryptography and Security (2nd Ed.), pages 605-607, 2011.
[ BibTeX entry ] - Heiko Mantel, David Sands and Henning Sudbrock. Assumptions and Guarantees for Compositional Noninterference. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF), pages 218-232. IEEE Computer Society, 2011.
[ BibTeX entry | PDF | Proofs and Addendum ] - Heiko Mantel and Henning Sudbrock. Flexible Scheduler-Independent Security. In Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS). LNCS 6345, pages 116-133. Springer, 2010.
[ BibTeX entry | PDF | Proofs of Theorems ] - Alexander Lux and Heiko Mantel. Who Can Declassify? In Post-Proceedings of the 5th Workshop on Formal Aspects in Security and Trust (FAST 2008). LNCS, 5491, pages 35-49. Springer, 2009.
[ BibTeX entry | PDF ] - Alexander Lux and Heiko Mantel. Declassification with Explicit Reference Points. In Proceedings of the 14th European Symposium on Research in Computer Security (ESORICS). LNCS, 5789, pages 69-85. Springer, 2009.
[ BibTeX entry | PDF ] - Heiko Mantel and Henning Sudbrock. Information-Theoretic Modeling and Analysis of Interrupt-Related Covert Channels. In Post-Proceedings of the 5th International Workshop on Formal Aspects in Security and Trust (FAST 2008). LNCS 5491, pages 67-81. Springer, 2009.
[ BibTeX entry | PDF | Appendix ] - Heiko Mantel and Henning Sudbrock. Increasing the Precision of the Combining Calculus (Extended Abstract). In Proceedings of the 5th International Workshop on Programming Language Interference and Dependence (PLID), 2009.
[ BibTeX entry ] - Deepak D'Souza, Raveendra Holla, Janardhan Kulkarni, Raghavendra Kagalavadi Ramesh and Barbara Sprick. On the Decidability of Model-Checking Information Flow Properties. In Proceedings of the 4th International Conference on Information Systems Security (ICISS). LNCS 5352, pages 26-40. Springer, 2008.
[ BibTeX entry ] - H. Gregor Molter, Hui Shao, Henning Sudbrock, Sorin A. Huss and Heiko Mantel. Designing a Coprocessor for Interrupt Handling on an FPGA. TU Darmstadt, Technical Report TUD-CS-2008-1103, 2008.
[ BibTeX entry | PDF ] - Serge Autexier, Heiko Mantel, Stephan Merz and Tobias Nipkow (Ed.). Special Issue on Formal Modeling and Verification of Critical Systems. Journal of Automated Reasoning 41(3-4), Springer, 2008.
[ BibTeX entry | URL ] - Dieter Hutter, Heiko Mantel, Ina Schaefer and Axel Schairer. Security of Multi-agent Systems: A Case Study on Comparison Shopping. In Journal of Applied Logic (JAL), 5(2), pages 303-332, 2007.
[ BibTeX entry ] - Boris Köpf and Heiko Mantel. Transformational Typing and Unification for Automatically Correcting Insecure Programs. In International Journal of Information Security (IJIS), 6(2-3), pages 107-131, 2007.
[ BibTeX entry ] - Tina Kraußer, Heiko Mantel and Henning Sudbrock. A Probabilistic Justification of the Combining Calculus under the Uniform Scheduler Assumption. RWTH Aachen, Technical Report 2007-09, 2007.
[ BibTeX entry ] - Heiko Mantel and Alexander Reinhard. Controlling the What and Where of Declassification in Language-Based Security. In Proceedings of the 16th European Symposium on Programming (ESOP). LNCS, 4421, pages 141-156. Springer, 2007.
[ Abstract | BibTeX entry | PDF ] - Heiko Mantel and Henning Sudbrock. Comparing Countermeasures against Interrupt-Related Covert Channels in an Information-Theoretic Framework. In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF), pages 326-340. IEEE Computer Society, 2007.
[ Abstract | BibTeX entry | PDF ] - Heiko Mantel, Henning Sudbrock and Tina Kraußer. Combining Different Proof Techniques for Verifying Information Flow Security. In Post-Proceedings of the 16th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2006). LNCS, 4407, pages 94-110. Springer, 2007.
[ Abstract | BibTeX entry | PDF ] - Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers and Andrei Sabelfeld (Ed.). Executive Summary and Abstracts Collection of Seminar 0709: Mobility, Ubiquity, and Security. Dagstuhl, 2007.
[ BibTeX entry ] - Virgil D. Gligor and Heiko Mantel (Ed.). Proceedings of the ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE). 2007.
[ BibTeX entry ] - Boris Köpf and Heiko Mantel. Eliminating Implicit Information Leaks by Transformational Typing and Unification. In Post-Proceedings of the 3rd International Workshop on Formal Aspects in Security and Trust (FAST 2005). LNCS, 3866, pages 47-62. Springer, 2006.
[ BibTeX entry | URL ] - Serge Autexier and Heiko Mantel (Ed.). Proceedings of the Verification Workshop (VERIFY 2006). FLoC, 2006. Workshop in connection with Federated Logic Conference, FLoC'06.
[ BibTeX entry | URL ] - Heiko Mantel. The Framework of Selective Interleaving Functions and the Modular Assembly Kit. In Proceedings of the 3rd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE), pages 53-62. ACM, 2005.
[ BibTeX entry | PDF | zipped Postscript ]
Master/Diploma/Bachelor Theses
- Jens Korinth. Preserving Information Flow Properties of CSP Specifications under Refinement. Master Thesis, TU Darmstadt, 2013.
[ BibTeX entry ] - Patrick Metzler. Tool Support for Step-Wise Analysis and Mitigation of Timing Channels in Java. Bachelor Thesis, TU Darmstadt, 2013.
[ BibTeX entry ] - Dominic Scheurer. Enforcing Datalog Policies with Service Automata on Distributed Version Control Systems. Bachelor Thesis, TU Darmstadt, 2013.
[ BibTeX entry ] - Markus Tasch. Exemplary Specification of Integrity Requirements by Information-Flow Properties. Bachelor Thesis, TU Darmstadt, 2013.
[ BibTeX entry ] - Alexander Gebhardt. Monitoring C Programs by Finite State Machines. Master Thesis, TU Darmstadt, 2012.
[ BibTeX entry ] - Sogol Mazaheri. Race Conditions in Distributed Enforcement at the Example of Online Social Networks. Bachelor Thesis, TU Darmstadt, 2012.
[ BibTeX entry ] - Jan Mundo. Analyse von C-Programmen bezüglich Secure Coding mittels LTL-Modelchecking. Bachelor Thesis, TU Darmstadt, 2012.
[ BibTeX entry ] - Daniel Specht. A Formal Model and Tool for Data Flow Security in Computer Networks. Bachelor Thesis, TU Darmstadt, 2012.
[ BibTeX entry ] - Daniel Staesche. Security Preserving Refinement of CSP Specifications. Master Thesis, TU Darmstadt, 2012.
[ BibTeX entry ] - Florian Wendel. An Evaluation of Delegation Strategies for Coordinated Enforcement. Bachelor Thesis, TU Darmstadt, 2012.
[ BibTeX entry ] - Tobias Plötz. Vertraulichkeit von Werten im Modular Assembly Kit for Security (MAKS). Bachelor Thesis, TU Darmstadt, 2011.
[ BibTeX entry ] - Sylvia Grüner. Formale Spezifikation von Sicherheitsanforderungen mit MAKS in Isabelle/HOL. Bachelor Thesis, TU Darmstadt, 2010.
[ BibTeX entry ] - Jens Korinth. Relating Process Semantics by Equivalence-Preserving Transformations. Bachelor Thesis, TU Darmstadt, 2010.
[ BibTeX entry ] - Timo Schneider. Model Checking von Informationsflusseigenschaften. Master Thesis, TU Darmstadt, 2010.
[ BibTeX entry ] - Oliver Bračevac. Verhaltensintegrität von Programmen unter nebenläufigen Dateisystemzugriffen. Bachelor Thesis, TU Darmstadt, 2010.
[ BibTeX entry ] - Sven Amann. Spezifikation und Codegenerierung von Sicherheitsautomaten. Bachelor Thesis, TU Darmstadt, 2009.
[ BibTeX entry ] - Steffen Lortz. Typbasierte Informationsflussanalyse für JVM-Programme auf Mobilgeräten. Bachelor Thesis, TU Darmstadt, 2009.
[ BibTeX entry ] - Matthias Perner. Information Flow Analysis for CIL. Bachelor Thesis, TU Darmstadt, 2008.
[ BibTeX entry | PDF ] - Timo Schneider. Fallstudie: Sicherheitsautomat für einen orchestrierten Dienst in einer serviceorientierten Architektur. Bachelor Thesis, TU Darmstadt, 2008.
[ BibTeX entry ] - Alexander Reinhard. Analyse nebenläufiger Programme unter intransitiven Sicherheitspolitiken. Diploma Thesis, RWTH Aachen, 2006.
[ BibTeX entry | PDF ]
Print
Imprint
Sitemap
Contact