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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.