Many applications that handle private or confidential data release part of this data in a controlled manner through filter functions.However, it can be difficult to reason formally about exactly what or how much information is declassified.Often, anonymity is measured by reasoning about the equivalence classes of all inputs to the filter that map to the same output.An observer or attacker that sees the output of the filter then only knows that the secret input belongs to one of these classes, but not the exact input.We propose a technique suitable for complex filter functions together with a proof method, that additionally can provide meaningful guarantees.We illustrate the technique with a DistanceTracker app in a leaky and a non-leaky version.

The development of a secure service application is a difficult task and designed protocols are very error-prone. To develop a secure SOA application, application-independent protocols (e.g. TLS or Web service security protocols) are used. These protocols guarantee standard security properties like integrity or confidentiality but the critical properties are applicationspecific (e.g. “a ticket can not be used twice”). For that, security has to be integrated in the whole development process and application-specific security properties have to be guaranteed. This paper illustrates the modeling of a security-critical service application with UML. The modeling is part of an integrated software engineering approach that encompasses model-driven development. Using the approach, an application based on service-oriented architectures (SOA) is modeled with UML. From this model executable code as well as a formal specification to prove the security of the application is generated automatically. Our approach, called SecureMDD, supports the development of security-critical applications and integrates formal methods to guarantee the security of the system. The modeling guidelines are demonstrated with an online banking example.

Formal verification can give more confidence in the security of cryptographic protocols. Application specific security properties like "The service provider does not loose money" can give even more confidence than standard properties like secrecy or authentication. However, it is surprisingly easy to get a meaningful property slightly wrong. The result is that an insecure protocol can be 'proven' secure. We illustrate the problem with a very small application, a copy card, that has only five different messages. The example is taken from a paper where the protocol is secure, but the proved property slightly wrong. We propose to solve the problem by incorporating more of the real-world application into the formal model.

In this paper we introduce our model-driven software engineering method, called SecureMDD, which facilitates the development of security-critical applications that are based on cryptographic protocols. The approach seamlessly integrates the generation of code and formal methods. Starting with a platform-independent UML model of a system under development, we generate executable Java (Card) code as well as a formal model from the UML model. Subsequent to this, the formal model is used to verify the security of the modeled system. Our goal is to prove that the generated code is correct w.r.t. the generated formal model in terms of formal refinement. The approach is tailored to the domain of security-critical systems, e.g. smart card applications.

There is a mismatch between the data format used in implementations of security protocols and the data types used in formal verification of security protocols. We present a verified encoding scheme for data used in security protocols, which links the abstract data types of the formal world to a byte format usable in implementations. The encoding is inspired by the ASN1 encoding scheme. The encoding is implemented in Java and the implementation is proven to be correct against a formal specification. The implementation can be used as a reusable reference library in security protocol implementations. The benefit is a separation of concerns: The protocol can be verified on an abstract level. The mapping to bytes is automatically correct by linking the library. Additionally the encoding is a challenging Java verification case study in its own.

This paper presents an approach to the verification of large Java programs. The focus lies on programs that implement a distributed communicating system e.g. in a M- or E-commerce scenario. When trying to verify such programs, thousands of Java classes with tens of thousands of lines of code would have to be taken into consideration. That is impossible. The paper introduces a technique that dramatically reduces the amount of source code that must be considered. Additionally, a suitable method for programming security critical systems is introduced. The reduction is achieved by extracting a verification kernel from the program, which is sufficient for proving the correctness of the relevant part. An algorithm for the automatic computation of the verification kernel has been developed and is presented in the paper. The correctness of the verification kernel approach is proved on the level of the Java language semantics.