[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 ]
Component-based design is a method for modular design of systems. The structure of component-based systems follows specific rules and single components make assumptions on the environment that they run in. In this paper, we provide a noninterference property for component-based systems that allows for a precise specification of what-declassification of information and takes assumptions on the environment into consideration in order to allow a modular, precise and re-usable information-flow analysis. For precise analysis, components can be analyzed by separately analysing services provided by a component, and from our compositionality theorem non-interference of components follows.

[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 ]
We give an account on the authors' experience and results from the software verification competition held at the Formal Methods 2012 conference. Competitions like this are meant to provide a benchmark for verification systems. It consisted of three algorithms which the authors have implemented in Java, specified with the Java Modeling Language, and verified using the KeY system. Building on our solutions, we argue that verification systems which target implementations in real-world programming languages are required to have powerful capabilities for abstraction. Regarding the KeY tool, we explain features which, driven by the competition, have been freshly implemented to accommodate for these demands.

[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 ]
The goal of this thesis is to develop a rigorous analysis technique for proving functional and relational correctness of shared-memory multi-threaded object-oriented software systems—such as programs written in the Java language—based on formal program semantics and deductive verification. This work contains the first approach towards a semantically precise information flow anlaysis for concurrent programs.

[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 ]
Verification of concurrent programs still poses one of the major challenges in computer science. Several techniques to tackle this problem have been proposed. However, they often do not scale. We present an adaptation of the rely/ guarantee methodology in dynamic logic. Rely/ guarantee uses functional specification to symbolically describe the behavior of concurrently running threads: while each thread guarantees adherence to a specified property at any point in time, all other threads can rely on this property being established. This allows to regard threads largely in isolation—only w.r.t. an environment constrained by these specifications. While rely/guarantee based approaches often suffer from a considerable specification overhead, we complement functional thread specifications with frame conditions. We will explain our approach using a simple, but concurrent programing language. Besides the usual constructs for sequential programs, it caters for dynamic thread creation. We define semantics of concurrent programs w.r.t. an underspecified deterministic scheduling function. To formally reason about programs of this language, we introduce a novel multi-modal logic, Concurrent Dynamic Trace Logic (CDTL). It combines the strengthes of dynamic logic with those of linear temporal logic and allows to express temporal properties about symbolic program traces. We first develop a sound and complete sequent calculus for the logic subset that uses the sequential part of the language, based on symbolic execution. In a second step, we extend this to a calculus for the complete logic by adding symbolic execution rules for concurrent interleavings and dynamic thread creation based on the rely/guarantee methodology. Again, this calculus is proven sound and complete.

[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 ]
Several tools and approaches for proving noninterference properties for Java and other languages exist. Some of them have a high degree of automation or are even fully automatic, but overapproximate the actual information flow, and hence, may produce false positives. Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence, analysis is time-consuming. In this paper, we propose a hybrid approach that aims at obtaining the best of both approaches: We want to use fully automatic analysis as much as possible and only at places in a program where, due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive analysis, where the latter involves only the verification of specific functional properties in certain parts of the program, rather than checking more intricate noninterference properties for the whole program. To illustrate the hybrid approach, in a case study we use the hybrid approach—along with the fully automatic tool Joana for checking noninterference properties for Java programs and the theorem prover KeYfor the verification of Java programs—and the CVJ framework proposed by Küsters, Truderung, and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an e-voting system. The CVJ framework allows one to establish cryptographic indistinguishability properties for Java programs by checking (standard) noninterference properties for such programs.

[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 ]
Electronic voting (e-voting) systems that are used in public elections need to fulfil a broad range of strong requirements concerning both safety and security. Among these requirements are reliability, robustness, privacy of votes, coercion resistance and universal verifiability. Bugs in or manipulations of an e-voting system may have considerable influence on the life of the humans living in a country where such a system is used. Hence, e-voting systems are an obvious target for software verification. In this paper, we report on an implementation of such a system in Java and the formal verification of functional properties thereof in the KeY verification system. Even though the actual components are clearly modularized, the challenge lies in the fact that we need to prove a highly nonlocal property: After all voters have cast their votes, the server calculates the correct votes for each candidate w.r.t. the original ballots. This kind of trace property is difficult to prove with static techniques like verification and typically yields a large specification overhead.

[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 ]
Today, nearly all personal computer systems are multiprocessor systems, allowing multiple programs to be executed in parallel while accessing a shared memory. At the same time, computers are increasingly handling more and more data. Ensuring that no confidential data is leaked to untrusted sinks remains a major quest in software engineering. Formal verification, based on theorem proving, is a powerful technique to prove both functional correctness and security properties such as absence of information flow. Present verification systems are sound and complete, but often lack efficiency and are only applicable to sequential programs. Concurrent programs are notorious for all possible environment actions have to be taken into account. In this paper, we point out steps towards a formal verification methodology for information flow in concurrent programs. We consider passive attackers who are able to observe public parts of the memory at any time during execution and to compare program traces between different executions. Our approach consists of two main elements: (i) formalizing properties on whether two executions are indistinguishable to such an attacker in a decidable logic, and (ii) defining a technique to reason about executions of concurrent programs by regarding a single thread in isolation. The latter is based on the rely/guarantee approach.

[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 ]
This paper contributes to the investigation of object-sensitive information-flow properties for sequential Java, i.e., properties that take into account information leakage through objects, as opposed to primitive values. We present two improvements to a popular object-sensitive non-interference property. Both reduce the burden on analysis and monitoring tools. The second contribution is a formalization of this property in a program logic – JavaDL in our case – which allows using an existing tool without requiring program modification. The third contribution is a novel fine-grained specification methodology. In our approach, arbitrary JavaDL terms (read side-effect-free Java expressions) may be assigned a security level – in contrast to security labels being attached to fields and variables only.

[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 ]
This text is a general, self contained, and tool independent introduction into the Java Modeling Language, JML. It is a preview of a chapter planned to appear in a book about the KeY approach and tool to the verification of Java software. JML is the dominating starting point of KeY style Java verification. However, this paper does not in any way depend on any tool nor verification methodology. Other chapters in this book talk about the usage of JML in KeY style verification. Here, we only refer to KeY in very few places, without relying on it. This introduction is written for all readers with an interest in formal specification of software in general, and anyone who wants to learn about the JML approach to specification in particular. The authors appreciate any comments or questions that help to improve the text.

[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 ]
The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flow security, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.

[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 ]
Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic (DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for proving functional and information-flow properties in concurrent programs, among other applications.

[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 ]
It is a common belief that the rise of standardized software certification schemes like the Common Criteria (CC) would give a boost to formal verification, and that software certification may be a killer application for program verification. However, while formal models are indeed used throughout high-assurance certification, verification of the actual implementation is not required by the CC and largely neglected in certification practice – despite the great advances in program verification over the last decade. In this paper we discuss the gap between program verification and CC software certification, and we point out possible uses of code-level program verification in the CC certification process.

[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 ]
It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional. In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert's ε terms.

[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 ]
Dynamic logic is an established instrument for program verification and for reasoning about the semantics of programs and programming languages. In this paper, we define an extension of dynamic logic, called Dynamic Trace Logic (DTL), which combines the expressiveness of program logics such as dynamic logic with that of temporal logic. And we present a sound and relatively complete sequent calculus for proving validity of DTL formulae. Due to its expressiveness, DTL can serve as a basis for functional verification of concurrent programs and for proving information-flow properties among other applications.

[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 ]
In this paper, we report on an ongoing case study in which we use the KeY tool, a theorem prover for checking functional correctness and noninterference properties of Java programs, to establish computational indistinguishability for a simple Java program that involves clients sending encrypted messages over an untrusted network to a server. The analysis uses a general framework, recently proposed by Küsters et al., which enables program analysis tools, such as KeY, that can check (standard) noninterference properties for Java programs to establish computational indistinguishability properties.

[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 ]
Complex data structures still pose a major challenge in specification and verification of object-oriented programs. Leino and Moskal have proposed a suite of benchmarks for verification tools, nicknamed “VACID-0”. In contrast to similar papers, the tasks of VACID-0 do not only include verification in terms of an observable behavior but also of internal workings of algorithms and data structures. The arguably most difficult target are so-called red-black black trees. In this contribution, we present an implementation and specification in Java/JML (i.e., KeY's extension to JML with dynamic frames). It makes use of several new features: first and foremost the dynamic frame theory, model fields, the sequence ADT, as well as some newly supported features from standard JML.

[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 ]
It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification languages, such as the Java Modeling Language (JML), model fields are a common means for achieving abstraction and information hiding. However, there is yet no well-defined formal semantics for the general case in which the abstraction relation defining a model field is non-functional and may contain references to other model fields. In this contribution, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is inspired by a generalization of Hilbert's ε terms.

[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 ]
Software product lines (SPL) are a well-known methodology to develop industry-size adaptable software systems. SPL are often used in domains where high-quality software is desirable, but the overwhelming product diversity remains a challenge for assuring correctness. We present our work in progress on reducing the deductive verification effort across different products of an SPL. On the specification side, our approach enriches the delta language for describing SPLs with formal product specifications. On the verification side, we combine program slicing and similarity-guided proof reuse to ease the verification process.

[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 ]
Software product lines (SPL) are a well-known methodology to develop industry-size adaptable software systems. SPL are often used in domains where high-quality software is desirable, but the overwhelming product diversity remains a challenge for assuring correctness. We present our work in progress on reducing the deductive verification effort across different products of an SPL. On the specification side, our approach enriches the delta language for describing SPLs with formal product specifications. On the verification side, we combine program slicing and similarity-guided proof reuse to ease the verification process.

[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 ]
A common critique of formal methods in software development practise is, that they are not readily understandable and thus not widely used. The Java Modeling Language (JML) was created in an attempt to bridge that gap. By building upon the syntax of Java it is meant to be easily accessible to the common user – who might not be skilled in formal modeling. Due to this advantage, JML has quickly become one of most popular specification languages to use with both static and runtime analysis of programs. JML specifications are written in a Java-like expression language as comments straight into source files. It provides both in-code assertions as well as method contracts and class invariants which are indicated by appropriate preceding keywords. However, the official reference mostly lacks a clear definition of semantics. In turn, several tools implementing JML syntax use their own interpretations. Past approaches to formal semantics have rather been documentations of those tools than providing a unified reference.

[Bru09] Daniel Bruns. Formal semantics for the Java Modeling Language. Diplomarbeit, Universität Karlsruhe, June 2009. [ bib | license | urn | http ]
This thesis is concerned with the Java Modeling Language (JML), a wide-spread specification language for Java, which is used in both static and runtime analysis of programs. Yet, the official reference mostly lacks semantics, while several tools which implement JML do not agree on their interpretation of JML specifications. Past approaches have all centered around a certain verification tool and are highly depending on specific higher order logics. In this work, we develop a formalization with little requirements. Upon a simple machine model we describe JML artifacts in basic notations such as first order logic. In that, we provide a nearly comprehensive overview of features which cover nearly all specification elements for sequential Java programs.

[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 ]

This file was generated by bibtex2html 1.98.