Dr.rer.nat. Daniel Grahl (né Bruns)
|
Until February 2016, I was a post-doctoral researcher with the Application-oriented Formal Verification group led by Bernhard Beckert at KIT. My PhD thesis is entitled "Deductive Verification of Concurrent Programs and its Application to Secure Information Flow for Java" (see below). Please note that this page is no longer maintained since I moved to industry. Research ProjectsCurrently, I'm working on the FIfAKS project, that is funded by BMBF as part of the Sofwarecampus program. The goal of the project is to establish an analysis technique for secure information flow in component software at design level with high precision. We cooperate with DHL IT Services. |
 |
Previously, I was working on the DeduSec project as part of the DFG SPP 1496 Reliably Secure Software Systems (RS3). The goal is to establish a semantically precise information flow analysis in Java programs at source level through the means to theorem proving. Please see the project homepage (or read my publications) for more information on the topic.
Contact Information
Please consider sending e-mails encrypted. My PGP public key can be downloaded here: 52A42DF1. The fingerprint is F98852543F84C40A3D49F4C6264DB27852A42DF1.
Teaching
I have been teaching Software Engingeering Practice (Praxis der Software-Entwicklung, PSE) for some time. In PSE, early in their curriculum, Bachelor students (usually in their 3rd semester) are working in groups of 5 or 6 on developing a moderately complex object-oriented software system (c. 10kLoC). They are required to complete all stages of the waterfall model: requirements, design, implementation, validation, and deployment.
In 2012, I have been awarded for 'excellent teaching in the department of informatics.'
All my students did very well and most of them have released their work to the public:
Software verification using SMT
In the winter term 2011/2012, the objective was to design a simple imperative programing language and to develop an IDE for it. The IDE was supposed to include features for both execution/debugging and formal verification using weakest precondition calculation and passing the proof obligation to an SMT solver (Z3 in our case). The resulting WorthWhile and WeProve tools are really impressive!
Information flow analysis using theorem proving
In the winter term 2012/2013, we extended the above topic with information flow analysis (leaving some other features optional). The idea was to use selfcomposition to transform a program into a form where proving its postcondition is equivalent to proving the (relational) property of noninterference. The Fährmann tool is the result ('Fährmann' meaning 'ferry man' in German).
Calculating election results for the German Bundestag
The electoral system for the Bundestag (the German federal parliament) is one of the most complex election systems, due to different levels of participation (district, state, federal), the mix of directly FPTP elected candidates and proportional representation of party list candidates, and a threshold combining several criteria. Proportionality is established through leveling seats since a reform in 2013. (See, e.g., the explanation on Wikipedia.)
The objective of PSE in winter term 2013/2014 was to create a sound and transparent calculator for Bundestag elections. Bundeswahlrechner and OpenBundestagswahl are Java implementations (in German), which also allow comparing different election outcomes.
Professional activitiesI organized a workshop at the Lorentz Center in Leiden (NL) on the Java Modeling Language (JML) in March 2015. JML is the de-facto standard language for the formal specification of Java source code. The workshop is the central gathering point for the community that contributes to the development of JML. It is the third in a series with the previous editions 2010 at Schloss Dagstuhl and 2015 at the Shōnan Center in Japan (which I also attended). The next workshop is planned for early 2016 in Karlsruhe. |
|
Publications
| [GG15] | Daniel Grahl and Simon Greiner. Non-interference with what-declassification in component-based systems. Technical Report 2015,10, Department of Informatics, Karlsruhe Institute of Technology, November 2015. [ bib | license | urn | http | Abstract ] |
| [BMU15] | Daniel Bruns, Wojciech Mostowski, and Mattias Ulbrich. Implementation-level verification of algorithms with KeY. Software Tools for Technology Transfer, 17(6):729–744, November 2015. [ bib | DOI | http | Abstract ] |
| [Gra15] | Daniel Grahl. Deductive Verification of Concurrent Programs and its Application to Secure Information Flow for Java. PhD thesis, Karlsruhe Institute of Technology, 29 October 2015. [ bib | DOI | license | urn | http | Abstract ] |
| [Bru15b] | Daniel Bruns. A theorem proving approach to secure information flow in concurrent programs (extended abstract). In Deepak Garg and Boris Köpf, editors, Workshop on Foundations of Computer Security (FCS 2015), July 2015. [ bib | .pdf ] |
| [BDG+15] | Daniel Bruns, Huy Quoc Do, Simon Greiner, Mihai Herda, Martin Mohr, Enrico Scapin, Tomasz Truderung, Bernhard Beckert, Ralf Küsters, Heiko Mantel, and Richard Gay. Poster: Security in e-voting. In Sophie Engle, editor, 36th IEEE Symposium on Security and Privacy, Poster Session, 18 May 2015. [ bib ] |
| [Bru15a] | Daniel Bruns. Deductive verification of concurrent programs. Technical Report 2015,3, Department of Informatics, Karlsruhe Institute of Technology, February 2015. [ bib | license | urn | http | Abstract ] |
| [KTB+15] | Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Michael Kirsten, and Martin Mohr. A hybrid approach for proving noninterference of Java programs. In Cédric Fournet, Michael Hicks, and Luca Viganò, editors, 28th IEEE Computer Security Foundations Symposium (CSF), pages 305–319, 2015. [ bib | DOI | http | Abstract ] |
| [Bru14a] | Daniel Bruns. Formal verification of an electronic voting system. Technical Report 2014,11, Department of Informatics, Karlsruhe Institute of Technology, August 2014. [ bib | license | urn | http | Abstract ] |
| [Bru14b] | Daniel Bruns. Towards specification and verification of information flow in concurrent Java-like programs. Technical Report 2014,5, Department of Informatics, Karlsruhe Institute of Technology, March 2014. [ bib | license | urn | http | Abstract ] |
| [BBK+14] | Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. Information flow in object-oriented software. In Gopal Gupta and Ricardo Peña, editors, Logic-Based Program Synthesis and Transformation, LOPSTR 2013, number 8901 in Lecture Notes in Computer Science, pages 19–37. Springer, 2014. [ bib | DOI | Abstract ] |
| [HABH14] | Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel. Formal specification with JML. Technical Report 2014,10, Department of Informatics, Karlsruhe Institute of Technology, 2014. [ bib | license | urn | http | Abstract ] |
| [ABB+14] | Wolfgang Ahrendt, Bernhard Beckert, Daniel Bruns, Richard Bubel, Christoph Gladisch, Sarah Grebing, Reiner Hähnle, Martin Hentschel, Mihai Herda, Vladimir Klebanov, Wojciech Mostowski, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. The KeY platform for verification and analysis of Java programs. In Dimitra Giannakopoulou and Daniel Kroening, editors, Verified Software: Theories, Tools, and Experiments (VSTTE 2014), number 8471 in Lecture Notes in Computer Science, pages 1–17. Springer-Verlag, 2014. [ bib | DOI | http | Abstract ] |
| [BBK+13a] | Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. Information flow in object-oriented software – extended version –. Technical Report 2013,14, Department of Informatics, Karlsruhe Institute of Technology, 2013. [ bib | license | urn | http ] |
| [BBK+13b] | Bernhard Beckert, Daniel Bruns, Vladimir Klebanov, Christoph Scheben, Peter H. Schmitt, and Mattias Ulbrich. Secure information flow for Java – a dynamic logic approach. Technical Report 2013,10, Department of Informatics, Karlsruhe Institute of Technology, 2013. [ bib | license | http ] |
| [BB13] | Bernhard Beckert and Daniel Bruns. Dynamic logic with trace semantics. In Maria Paola Bonacina, editor, 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Computer Science, pages 315–329. Springer-Verlag, 2013. [ bib | DOI | http | Abstract ] |
| [KTB+13] | Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Jürgen Graf, and Christoph Scheben. A hybrid approach for proving noninterference and applications to the cryptographic verification of Java programs. In Christian Hammer and Sjouke Mauw, editors, Grande Region Security and Reliability Day 2013, Luxembourg, 2013. Extended Abstract. [ bib | .pdf ] |
| [BBG12] | Bernhard Beckert, Daniel Bruns, and Sarah Grebing. Mind the gap: Formal verification and the Common Criteria. In Markus Aderhold, Serge Autexier, and Heiko Mantel, editors, 6th International Verification Workshop, VERIFY-2010, volume 3 of EPiC Series, pages 4–12. EasyChair, 2012. [ bib | http | Abstract ] |
| [BB12b] | Bernhard Beckert and Daniel Bruns. Formal semantics of model fields in annotation-based specifications. In Birte Glimm and Antonio Krüger, editors, KI 2012: Advances in Artificial Intelligence, volume 7526 of Lecture Notes in Computer Science, pages 13–24. Springer-Verlag, 2012. [ bib | http | Abstract ] |
| [BB12a] | Bernhard Beckert and Daniel Bruns. Dynamic trace logic: Definition and proofs. Technical Report 2012,10, Department of Informatics, Karlsruhe Institute of Technology, 2012. A revised version replacing an unsound rule is available at https://formal.kastel.kit.edu/grahl/papers/trace-tr.pdf. [ bib | license | urn | http | Abstract ] |
| [Bru12] | Daniel Bruns. Eine formale Semantik für die Java Modeling Language. Informatik-Spektrum, 35(1):45–49, 2012. [ bib | DOI | http ] |
| [BBK+12] | Bernhard Beckert, Daniel Bruns, Ralf Küsters, Christoph Scheben, Peter H. Schmitt, and Tomasz Truderung. The KeY approach for the cryptographic verification of Java programs: A case study. Technical Report 2012,8, Department of Informatics, Karlsruhe Institute of Technology, 2012. [ bib | license | urn | http | Abstract ] |
| [Bru11] | Daniel Bruns. Specification of red-black trees: Showcasing dynamic frames, model fields and sequences. In Wolfgang Ahrendt and Richard Bubel, editors, 10th KeY Symposium, Nijmegen, the Netherlands, 26–27 August 2011. Extended Abstract. [ bib | urn | http | Abstract ] |
| [BB11] | Bernhard Beckert and Daniel Bruns. Formal semantics of model fields inspired by a generalization of Hilbert's ε terms. In Wolfgang Ahrendt and Richard Bubel, editors, 10th KeY Symposium, Nijmegen, the Netherlands, 26–27 August 2011. Extended Abstract. [ bib | urn | http | Abstract ] |
| [BKS11] | Daniel Bruns, Vladimir Klebanov, and Ina Schaefer. Verification of software product lines with delta-oriented slicing. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software (FoVeOOS 2010), volume 6528 of Lecture Notes in Computer Science, pages 61–75. Springer-Verlag, 2011. [ bib | DOI | http | Abstract ] |
| [BKS10] | Daniel Bruns, Vladimir Klebanov, and Ina Schaefer. Verification of software product lines: Reducing the effort with delta-oriented slicing and proof reuse. In Bernhard Beckert and Claude Marché, editors, Papers Presented at the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), number 2010,13 in Karlsruhe Reports in Informatics, pages 345–358, Paris, France, 28–30 June 2010. Technical Report, Department of Informatics, Karlsruhe Institute of Technology, 2010-13. [ bib | urn | http | Abstract ] |
| [Bru10] | Daniel Bruns. Formal semantics for the Java Modeling Language. In Informatiktage 2010, volume S-9 of Lecture Notes in Informatics, pages 15–18, Bonn, Germany, 19–20 March 2010. Gesellschaft für Informatik. Best Paper Award. [ bib | .pdf | Abstract ] |
| [Bru09] | Daniel Bruns. Formal semantics for the Java Modeling Language. Diplomarbeit, Universität Karlsruhe, June 2009. [ bib | license | urn | http | Abstract ] |
| [Bru08] | Daniel Bruns. Elektronische Wahlen: Theoretisch möglich, praktisch undemokratisch. FIfF-Kommunikation, 25(3):33–35, September 2008. [ bib ] |
| [Bru07] | Daniel Bruns. A fixpoint-based rule for loop verification. Studienarbeit, Universität Karlsruhe, June 2007. [ bib ] |
Erdős number
My Erdős number is at most 4:- Paul Erdős, Saharon Shelah: Separability properties of almost-disjoint families of sets. Israel J. Math. 12 (1972)
- Dov M. Gabbay, Amir Pnueli, Saharon Shelah, Jonathan Stavi: On the Temporal Basis of Fairness. POPL 1980
- Bernhard Beckert, Dov M. Gabbay: Fibring Semantic Tableaux. TABLEAUX 1998
- Bernhard Beckert, Daniel Bruns: Dynamic Logic with Trace Semantics. CADE 2013
