@Article{ bracevac.gay.ea:isabellehol, author = {Oliver Bracevac and Richard Gay and Sylvia Grewe and Heiko Mantel and Henning Sudbrock and Markus Tasch}, title = {An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties}, journal = {Archive of Formal Proofs}, year = 2018 } @TechReport{ grewe.mantel.ea:i-maks, author = {Sylvia Grewe and Heiko Mantel and Markus Tasch and Richard Gay and Henning Sudbrock}, title = {I-MAKS A Framework for Information-Flow Security in Isabelle/HOL}, institution = {TU Darmstadt}, year = 2018, number = {TUD-CS-2018-0056}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2018/TUD-CS-2018-0056-I-MAKS-Tr.pdf} } @Article{ ar:GayMantelSudbrock2015a, author = {Richard Gay and Heiko Mantel and Henning Sudbrock}, title = {{An Empirical Bandwidth Analysis of Interrupt-Related Covert Channels}}, journal = {International Journal of Secure Software Engineering (IJSSE)}, editor = {A. Aldini and F. Martinelli and N. Suri}, year = 2015, pages = {1--22}, volume = {6}, number = {2} } @InProceedings{ inp:GayMantelSudbrock2013a, author = {Richard Gay and Heiko Mantel and Henning Sudbrock}, title = {An Empirical Bandwidth Analysis of Interrupt-Related Covert Channels}, booktitle = {Proceedings of the 2nd International Workshop on Quantitative Aspects in Security Assurance (QASA)}, year = 2013, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2013/2013-GayMantelSudbrock-EmpiricalIRCC.pdf} } @InProceedings{ mantel.sudbrock:types:b, author = {Heiko Mantel and Henning Sudbrock}, title = {Types vs. PDGs in Information Flow Analysis}, booktitle = {Post-Proceedings of the 22nd International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2012)}, publisher = {Springer}, year = 2013, series = {LNCS 7844}, pages = {106--121}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2013/LOPSTR2012-MantelSudbrock.pdf} } @PhDThesis{ th:Sudbrock2013, author = {Henning Sudbrock}, title = {Compositional and Scheduler-Independent Information Flow Security}, school = {Technische Universit\"at Darmstadt}, year = 2013, address = {Darmstadt, Germany}, month = {April}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2014/2014-04-12-sudbrock-dissertation-final.pdf} } @InProceedings{ mantel.sudbrock:types, author = {Heiko Mantel and Henning Sudbrock}, title = {Types vs. PDGs in Information Flow Analysis}, booktitle = {Pre-Proceedings of the 22nd International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2012)}, address = {Leuven, Belgium}, year = 2012 } @TechReport{ tr:OchoaPapeRuhrothSprickStenzelSudbrock2012a, author = {Martin Ochoa and Sebastian Pape and Thomas Ruhroth and Barbara Sprick and Kurt Stenzel and Henning Sudbrock}, title = {{Report on the RS3 Topic Workshop ``Security Properties in Software Engineering''}}, institution = {Universit\"at Augsburg}, year = {2012}, number = {2012-02}, howpublished = {\url{http://opus.bibliothek.uni-augsburg.de/volltexte/2012/1865}} } @InProceedings{ mantel.sands.ea:assumptions, author = {Heiko Mantel and David Sands and Henning Sudbrock}, title = {Assumptions and Guarantees for Compositional Noninterference}, booktitle = {Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF)}, publisher = {IEEE Computer Society}, address = {Cernay-la-Ville, France}, year = 2011, pages = {218-232}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2011/2011-CSF-MantelSandsSudbrock-AssumptionsAndGuaranteesForCompositionalNoninterference.pdf} } @TechReport{ aderhold.ea:exemplary:2010, address = {Germany}, author = {Markus Aderhold and Jorge Cu{\'e}llar and Heiko Mantel and Henning Sudbrock}, institution = {TU Darmstadt}, number = {TUD-CS-2010-0060}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2010/2010_TUD-CS-2010-0060-SecureCoding.pdf}, title = {Exemplary Formalization of Secure Coding Guidelines}, year = 2010 } @InProceedings{ mantel.sudbrock:flexible, author = {Heiko Mantel and Henning Sudbrock}, title = {Flexible Scheduler-Independent Security}, booktitle = {Proceedings of the 15th European Symposium on Research in Computer Security (ESORICS)}, publisher = {Springer}, year = 2010, series = {LNCS 6345}, pages = {116--133}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2010/WebversionMantelSudbrock.pdf} } @InProceedings{ mantel.sudbrock:information-theoretic, author = {Heiko Mantel and Henning Sudbrock}, editor = {P. Degano and J. Guttman and F. Martinelli}, title = {Information-Theoretic Modeling and Analysis of Interrupt-Related Covert Channels}, booktitle = {Post-Proceedings of the 5th International Workshop on Formal Aspects in Security and Trust (FAST 2008)}, year = 2009, publisher = {Springer}, series = {LNCS 5491}, pages = {67--81}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2009/2008FAST-HMHS-Postproceedings-Webversion.pdf} } @InProceedings{ mantel.sudbrock:increasing, author = {Heiko Mantel and Henning Sudbrock}, title = {Increasing the Precision of the Combining Calculus (Extended Abstract)}, booktitle = {Proceedings of the 5th International Workshop on Programming Language Interference and Dependence (PLID)}, year = 2009 } @InProceedings{ mantel.sudbrock:information-theoretic:b, author = {Heiko Mantel and Henning Sudbrock}, title = {Information-Theoretic Modeling and Analysis of Interrupt-Related Covert Channels}, booktitle = {Pre-Proceedings of the 5th Workshop on Formal Aspects in Security and Trust (FAST 2008)}, year = 2008, pages = {67--81}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2008/mantelsudbrock-fast2008-preproceedings.pdf} } @TechReport{ molter.shao.ea:designing, author = {H. Gregor Molter and Hui Shao and Henning Sudbrock and Sorin A. Huss and Heiko Mantel}, title = {Designing a Coprocessor for Interrupt Handling on an FPGA}, institution = {TU Darmstadt}, year = 2008, number = {TUD-CS-2008-1103}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2008/0_TUD-CS-2008-1103.pdf} } @TechReport{ krauer.ea:probabilistic:2007, author = {Tina Krau\ss{}er and Heiko Mantel and Henning Sudbrock}, institution = {RWTH Aachen}, month = {May}, number = {2007-09}, title = {A Probabilistic Justification of the Combining Calculus under the Uniform Scheduler Assumption}, year = 2007 } @InProceedings{ mantel.ea:comparing:2007, abstract = {Interrupt-driven communication with hardware devices can be exploited for establishing covert channels. In this article, we propose an information-theoretic framework for analyzing the bandwidth of such interrupt-related channels while taking aspects of noise into account. As countermeasures, we present mechanisms that are already implemented in some operating systems, though for a different purpose. Based on our formal framework, the effectiveness of the mechanisms is evaluated. Despite the large body of work on covert channels, this is the first comprehensive account of interrupt-related covert channelanalysis and mitigation.}, author = {Heiko Mantel and Henning Sudbrock}, booktitle = {Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF)}, pages = {326--340}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2007/CSF07-MantelSudbrock.pdf}, publisher = {IEEE Computer Society}, title = {Comparing Countermeasures against Interrupt-Related Covert Channels in an Information-Theoretic Framework}, year = 2007 } @InProceedings{ mantel.sudbrock.ea:combining, author = {Heiko Mantel and Henning Sudbrock and Tina Krau\"ser}, editor = {German Puebla}, title = {Combining Different Proof Techniques for Verifying Information Flow Security}, booktitle = {Post-Proceedings of the 16th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2006)}, pages = {94--110}, publisher = {Springer}, year = 2007, series = {LNCS}, volume = 4407, abstract = {When giving a program access to secret information, one must ensure that the program does not leak the secrets to untrusted sinks. For reducing the complexity of such an information flow analysis, one can employ compositional proof techniques. In this article, we present a new approach to analyzing information flow security in a compositional manner. Instead of committing to a proof technique at the beginning of a verification, this choice is made during verification with the option of flexibly migrating to another proof technique. Our approachalso increases the precision of compositional reasoning in comparisonto the traditional approach. We illustrate the advantages in twoexemplary security analyses, on the semantic level and on thesyntactic level.}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2007/0_MantelSudbrockKrausser.pdf} } @InProceedings{ heiko-mantel-and-henning-sudbrock-and-tina-krauer:combining-different-proof-techniques-for-verifying-information-flow-security:2006, abstract = {When giving a program access to secret information, one must ensure that the program does not leak the secrets to untrusted sinks. For reducing the complexity of such an information flow analysis, one can employ compositional proof techniques. In this article, we present a new approach to analyzing information flow security in a compositional manner. Instead of committing to a proof technique at the beginning of a verification, this choice is made during verification with the option of flexibly migrating to another proof technique. Our approachalso increases the precision of compositional reasoning in comparison to the traditional approach. We illustrate the advantages in two exemplary security analyses, on the semantic level and on the syntactic level.}, address = {Venice, Italy}, author = {{Heiko Mantel and Henning Sudbrock and Tina Krau\ss{}er}}, booktitle = {{Pre-Proceedings of the 16th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2006)}}, editor = {Germ'an Puebla}, month = {July 12-14}, pages = {85--101}, pdf = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2006/lopstr-2006-preproceedings.pdf}, ps = {https://www.mais.informatik.tu-darmstadt.de/WebBib/papers/2006/lopstr-2006-preproceedings.PS.zip}, title = {{Combining Different Proof Techniques for Verifying Information Flow Security}}, year = 2006 }