Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Chalmers Security and Static Analysis Workshop
[go: Go Back, main page]

Chalmers Security and Static Analysis Workshop

Chalmers

Dept. of Computer Science
Chalmers University of Technology
Gothenburg, Sweden, August 19, 2005

Hosted by
The ProSec group

Schedule

Click on a talk title for the abstract. The slides are to be uploaded.

Friday, August 19, 2005 Slides
8:30 Coffee (D⁢ lunchroom, 7th floor)
9:00 Hanne Riis Nielson, DTU Abstract transition graphs for pi-calculus processes
9:25
Q&A;
9:30 Christian Probst, DTU A Portable Virtual Machine Target For Proof-Carrying Code slides
9:55
Q&A;
10:00 David Sands, Chalmers On Flow Sensitive Security Types
10:25
Q&A;
10:30 Coffee
11:00 Heiko Mantel, RWTH Aachen Eliminating Implicit Information Leaks by Transformational Typing and Unification
11:25
Q&A;
11:30 Mads Dam, KTH Decidability and proof systems for language-based non-interference relations preprint
on request
11:55
Q&A;
12:00 Lunch
1:30 Alejandro Russo, Stevens Declassification by Self-composition and Assertions slides
1:45
Q&A;
1:50 Tobias Gedell, Chalmers Loop Analysis in KeY slides
2:10
Q&A;
2:15 Aslan Askarov, Chalmers Security-typed languages for implementation of cryptographic protocols: A case study slides
2:40
Q&A;
2:45 Coffee
3:15 Rene Rydhof Hansen, DTU Non-interference for Carmel slides
3:40
Q&A;
3:45 Terkel Tolstrup, DTU Non-interference for VHDL slides
4:10
Q&A;
4:15 Coffee

Venue

Sektionsgemensamt sammanträdesrum, room 3364, EDIT Bldg, Hörsalsvägen 11, Chalmers.
How to get to the Department of Computer Science and Engineering, with maps.

Useful contacts:

Andrei Sabelfeld, EDIT 5476

Talk abstracts

Abstract transition graphs for pi-calculus processes

Speaker: Hanne Riis Nielson, DTU
Abstract:
Static program analyses often capture properties of the configurations of a system rather than properties of the transitions causing the system to move from one configuration to another. In this talk we sketch the ideas behind an analysis that constructs a finite and hence abstract transition system that faithfully models the execution of a process of the pi-calculus.  We illustrate the results of the analysis using several examples taken from the literature.

A Portable Virtual Machine Target For Proof-Carrying Code

Speaker: Christian Probst, DTU
Abstract:
Virtual Machines and Proof-Carrying Code are two techniques that have been used independently to provide safety for (mobile) code. Both these techniques have strengths and individual limitations. Existing virtual machines, such as the Java VM, have several drawbacks: First, the effort required for safety verification is considerable. Second, and more subtly, the need to provide such verification by the code consumer inhibits the amount of optimization that can be performed by the code producer. This in turn makes just-in-time compilation surprisingly expensive. Proof-Carrying Code, on the other hand, has its own set of limitations, among which are the size of proofs and the fact that the certified code is no longer machine-independent. By combining the two techniques, we are able to overcome these limitations.
Our hybrid safe-code solution uses a virtual machine that has been designed specifically to support proof-carrying code, while simultaneously providing efficient just-in-time compilation and target-machine independence. In particular, our approach reduces the complexity of the required proofs, resulting in fewer proof obligations that need to be discharged at the target machine.

On Flow Sensitive Security Types

Speaker: David Sands*, Chalmers
Abstract:
This work investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice.
By choosing the flow lattice to be the powerset of program variables, we obtain a system which, in a very strong sense, subsumes all other systems in the family (in particular, for each program, it allows one particular ``polymorphic'' derivation from which all others may be inferred). This distinguished system is shown to be equivalent to, though more simply described than, Amtoft and Banerjee's Hoare-style independence logic (SAS'04).
In general, some lattices are more expressive than others but, despite this, we show that no type system in the family can give better results for a given choice of lattice than the type system for that lattice itself.
Finally, for any program typeable in one of these systems, we show how to construct an equivalent program which is typeable in a simple flow-insensitive system. We argue that this general approach could be useful in a proof-carrying-code setting.
* Joint work with Sebastian Hunt, City U., London

Eliminating Implicit Information Leaks by Transformational Typing and Unification

Speaker: Heiko Mantel, RWTH Aachen
Abstract:
Before starting the security analysis of an existing system, the most likely outcome is often already clear, namely that the system is not entirely secure. Modifying a program such that it passes the analysis is a difficult problem and usually left entirely to the programmer. In this talk, I will show that and how unification can be used to compute such program transformations. This opens a new perspective on the problem of correcting insecure programs. I will demonstrate that integrating this approach into an existing transforming type system can also improve the precision of the analysis and the quality of the resulting programs.
This is joint work with Boris Koepf (ETH Zurich).

Decidability and proof systems for language-based non-interference relations

Speaker: Mads Dam, KTH
Abstract:
We examine decidability and axiomatizability of various non-interference relations in the literature, along with some new ones. Specifically we show that, for a simple parallel while language with a decidable expression theory, the relation of strong low bisimulation is decidable, and we give a sound and relatively complete proof system for the corresponding equivalence (hence also, non-interference) problem. In contrast, related equivalence and non-interference relations used by e.g. Volpano-Smith, Boudol-Castellani, and others, are undecidable. We then extend strong low bisimulation to the case where the level assignment to identifiers is allowed to change dynamically. This is closely related to intransitive non-interference studied recently by Mantel and Sands. We examine the relation between the definitions and conclude by adapting our decidability and axiomatizability results accordingly.

Declassification by Self-composition and Assertions

Speaker: Alejandro Russo, Stevens
Abstract:
Security properties based on information flow, such as noninterference, provide strong guarantees that confidentiality is maintained. However, programs often need to leak some amount of confidential information in order to serve their intended purpose, and thus violate noninterference.
To deal with these intentional leaks, Sabelfeld and Myers have introduced a model for delimited information release, which defines program security in the presence of leaks. They have also proposed a type system to detect if a program satisfies delimited release. Unfortunately, the type system is too restrictive; it rejects some programs that are trivially secure.
In this work-in-progress talk, we present a less restrictive system based on self-composition and assertions.

Loop Analysis in KeY

Speaker: Tobias Gedell, Chalmers
Abstract:
In the KeY system, loops can currently be handled in two ways. Either they are successively unwinded and symbolically executed, and their effects collected in so called updates, or induction is used. Both these methods have some drawbacks. Symbolically executing a loop may be very time consuming and might not always be possible, an example of this is when the loop range is unknown. Induction is very powerful but often requires a human to give the loop invariant.
We show that a class of loops can be handled without needing to unwind them or use induction. Our method is very similar to loop parallelization, which analyses the data dependence between the loop iterations. If there is no data dependence or there is only a special kind a dependence, the loop iterations can be executed in parallel. In KeY we simulate this parallel execution of a loop to construct the updates of the loop in an efficient way.

Security-typed languages for implementation of cryptographic protocols: A case study

Speaker: Aslan Askarov, Chalmers
Abstract:
Security protocols are critical for protecting modern communication infrastructures and are therefore subject to thorough analysis. However practical implementations of these protocols lack the same level of attention and thus may be more exposed to attacks.
This paper discusses security assurance provided by security-typed languages when implementing cryptographic protocols. Our results are based on a case study using Jif, a Java-based security-typed language, for implementing a non-trivial cryptographic protocol that allows playing online poker without a trusted third party.
The case study deploys the largest program written in a security-typed language to date and identifies insights ranging from security guarantees to useful patterns of secure programming.
Based on a joint paper with Andrei Sabelfeld, to appear in ESORICS'05.

Non-interference for Carmel

Speaker: Rene Rydhof Hansen, DTU
Abstract:
In this talk we define a notion of non-interference for a "rationalised" version of Java Card bytecode, called Carmel. Furthermore we discuss how an Information Flow Analysis can be specified and how it can be used to statically guarantee that a Carmel program has the non-interference property.

Non-interference for VHDL

Speaker: Terkel Tolstrup, DTU
Abstract:
The talk will describe a fragment of the hardware description language VHDL that is suitable for implementing the Advanced Encryption Standard algorithm. We then define an Information Flow analysis as required by the international standard Common Criteria. The goal of the analysis is to identify the entire information flow through the VHDL program. The result of the analysis is presented as a non-transitive directed graph that connects those nodes (representing either variables or signals) where an information flow might occur. We compare our approach to that of Kemmerer and conclude that our approach yields more precise results.
Andrei Sabelfeld, Last modified: August 2005