The Saarbrücken Graduate School in Computer Science

• An integrated program from B.Sc. or M.Sc. to Ph.D.
• Study and conduct research at a top computer science location
• Stipends and other forms of financial support
• All courses are taught in English
• !!! Next application deadline: 30 April 2009 !!!
• More information at
  http://frweb.cs.uni-sb.de/index.php?id=7&L=0

List of Researchers now in Romania

Ad Astra has a list* of researchers based in Romania and their ISI publications between 2002 and 2006 (computer science). The data is not so recent** and seems to be quite noisy***, still the general image is quite clear. It could be useful if you want to do research in Romania and you are looking for an adviser or a university****.

* Because of unavoidable errors this is not a reliable ranking.

** More recent data seems to be available in Excel format only. The format is more raw though.

*** The site allows you to correct the information for your papers if you find anything wrong.

**** Such data was used to rank Romanian universities based on their research achievement, as I already wrote.

zk-typechecker 0.2.0 Released

The zero-knowledge type-checker is a tool for automatically analyzing the security of protocols that use zero-knowledge proofs. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. The type-checker relies on the SPASS (or E) automated theorem prover to discharge proof obligations. It is released under the terms of the Apache License.

This release of the zero-knowledge type-checker adds support for security despite compromise and fixes many of the issues in the initial release (release notes). You can grab it from the page of the project.

My First Students

Last week two of the students I supervise submitted their Bachelor’s Thesis. Both theses are about automatically generating executable code from abstract specifications of security protocols, however, the focus is quite different. While Alex worked on a very powerful tool that generates interoperable protocol implementations (to be released soon), Thorsten formalized a much simpler code generator and proved it to the preserve the security of the original protocol. In the future we would like of course to have both, the extensibility, flexibility and interoperability of Alex’ tool, with the same strong security guarantees as Thorsten proves for his generated code.

• Expi2Java – An Extensible Code Generator for Security Protocols (Alex Busenius)
  Abstract: This thesis presents expi2java, an extensible code generator for security protocols. We use a variant of Spi calculus for the protocol specifications and complement it with an expressive type system that is designed to reject inconsistent protocols. This type system features subtyping and parametric polymorphism. It is able to handle the types of nested terms, specialized channels and even low-level term configurations. Expi2java is highly customizable, easily extensible and generates interoperable Java code. We show the flexibility of our approach by generating an implementation of the Transport Layer Security (TLS) protocol.
• Spi2F# – A Prototype Code Generator for Security Protocols (Thorsten Tarrach)
  Abstract: This thesis describes a new prototype tool that automatically generates a secure F# implementation of any protocol described in the Spi calculus. Type systems were previously proposed for analysing the security of both Spi calculus processes and F# implementations. The thesis investigates a formal translation from the Spi calculus to F# that is proved to preserve typability, and therefore the security properties of the original protocol are preserved.

Junior Research Groups at Saarland University

Saarland University is seeking to establish several junior research groups within the recently established Cluster of Excellence “Multimodal Computing and Interaction.” Here is the official announcement.

Summer School: GLOBAN 2008

This week I was in Warsaw where I attended the “Global Computing Approach to the Analysis of Systems” (GLOBAN) Summer School. The school is was (very well) organized by University of Warsaw, in association with the MOBIUS and SENSORIA European projects. The eight distinguished lecturers did a really good job introducing us to their research: Rocco De Nicola, Andrew D. Gordon, Reiko Heckel, Martin Hofmann, Joost-Pieter Katoen, Joe Kiniry, Flemming Nielson, and Andrei Sabelfeld.

All the materials (including slides and references) are available online, and so are some of the photos. My photos from Warsaw will also be available soon.

Summer School: VTSA 2008

Last week I attended the first “Verification Technology, Systems & Applications (VTSA 2008)” summer school at the Max Planck Institute for Informatics in Saarbrücken. The talks were very interesting and all the slides are available online. Some photos from the event are also available.

The course I liked the most was given by Grégoire Sutre and was about Static Analysis, Abstract Interpretation and Abstraction Refinement.

Course: Working with Automated Reasoning Tools

In the first week of September I attended a very interesting lecture entitled “Working with Automated Reasoning Tools”, given by Christoph Benzmueller (Saarland University) and Geoff Sutcliffe (University of Miami). The two most important highlights were the LEO-II automatic higher-order theorem prover and the TPTP theorem proving infrastructure (including the comprehensive TPTP problem and solution libraries, the TPTP syntax for first-order and higher-order logic, and the hordes of automatic theorem provers and many TPTP tools that can be called from any web browser using System-on-TPTP).

All the course materials are available online.

The Vicious Cycle

Two Hardware Hacks from Princeton

Cold Boot Attacks on Encryption Keys

The paper and more materials

 
 

Security Analysis of the Diebold AccuVote-TS Voting Machine

The paper and more materials

In more recent news: Diebold voting machine key copied from pic on Diebold site

POPL 2008 in San Francisco

A Step-indexed Semantics of Imperative Objects

Here is the final version of the paper I wrote with Jan as a follow up of my Master’s thesis. I’ll present it at the Workshop on Foundations of Object-Oriented Languages (FOOL’08) on the 13th January in San Francisco. This means I will also attend POPL, with which the workshop is affiliated, and I’m quite excited about it. Anyway, here is the paper and the 64-page extended version with full proofs.

Since the workshop does not count as prior publication the next step for us is to submit a slightly improved version to the Logical Methods in Computer Science journal.

The Status of the Romanian Research System (Translation, Draft)

Today we Romanians celebrate our national holiday. In a tradition that started last year when I translated muCommander to Romanian, I decided to do something that, even though very small, is still beneficial for my country. This time the translation goes from Romanian to English, and the source is an article by Razvan Florian about the current status of the Romanian research system. While the article puts my country is a rather negative light, I think it is an accurate description of reality, and should make an interesting read to foreigners interested in Romania.

Introduction

Sadly, the Romanian research system is currently in a lamentable state. Its poor performance situates Romania behind most countries in Europe, and even behind some of the countries in Africa. This situation is caused not only by the insufficient funds allocated for research, but also by the poor organization of the research system and the inefficient distribution of funds, as a consequence of using evaluation criteria for research that encourage the production of rubbish, rather than valuable knowledge or technologies. The current material aims at presenting the current status of the Romanian research system, while making reference to more detailed materials produced by the “Transparency and objectivity in the management of Romanian research” project, funded by the European Union through the PHARE program and carried over by the Ad Astra association.

Ad Astra: An Attempt to Help the Romanian Scientific Community

Ad Astra is a non-profit association that tries to promote high-quality research in Romania. I previously wrote about the ranking of the Romanian research universities maintained by Ad Astra, but there are many other nice things the association does in its attempt to help the Romanian scientific community.

Ad Astra publishes a journal twice per year containing reports on Romanian science, as well as papers on science and education policies. They also maintain a White Book of Romanian research in an attempt to showcase modern science, performed either in Romania or by Romanian scientists abroad.

Last but not least, Ad Astra aims at providing an open discussion forum on science and education policies, with the declared aim of presenting coherent reform proposals to the Romanian political establishment. They seem to act as a whistleblower for the chronic problems in the Romanian research and education system, about which everybody knows, but about which only very few try to do something. Here is a online petition for the resolution of some important problems of the Romanian research system.

Verifying Security Protocols and their Implementations

Last week I gave a two hour talk in our reading group about the verification of security protocols and their implementations. While the first half of my talk was a quite gentle introduction to protocol analysis, the second was actually much more interesting since I presented a nice paper from CSFW 2006:

Verified Interoperable Implementations of Security Protocols. Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse

The slides I used are available (pdf). They are “built” from the slides Andy Gordon used for his lecture at Marktoberdorf 2006 (pdf), the ones that Cédric Fournet used in a Colloquium talk at INRIA in 2007 (pdf), and the slides of one of the Language-based Security lectures Matteo Maffei gave last year at Saarland University (pdf).