SoS vacancies

There are vacancies for in the SoS (Security of Systems) group at the Radboud University Nijmegen.

Three PhD Positions in the area of Software Quality

It's a well-known fact that programmers currently spend far longer fixing defects in existing code than they do writing new code. Hence the growing interest in software tools that can analyze code as it is being written and that can automate the testing and quality-assurance procedures. On the other hand tremendous amounts of software have already been produced, and rewriting even a small part of it is not a realistic option. So, besides tools for writing new (correct) software there is a need for tools for analyzing existing software. In this project we will investigate both directions.

As to verification and validation of existing software, (model) abstraction is a key notion. To be able to analyse a concrete program one first has to build/extract an abstract model. This model only contains the information of the program relevant to the property being analyzed. Traditionally, model extraction is dedicated to a specific property and performed manually. In this project we will focus on what we would like to call (semi) automatic abstract model extraction: the model itself abstracts from the concrete property to be analyzed and the analysis tool that will be used. Then the abstract model can be instantiated to a specific property on which the analysis itself can be performed. An example is the analysis of heap-space usage of programs using amortization, which is the research goal of one of the available PhD positions, see below. The LaQuSo PhD position (position 2; see below) will focus on existing tools applied to industrial software. LaQuSo stands for Laboratory for Quality Software which aims at verification and validation of real software applications. It is a collaboration between Radboud University Nijmegen and Technical University Eindhoven.

As to development of new software, formal program correctness is a key issue. The idea is to use the program verification system PVS as an interactive development environment. In PVS one can write formal specifications, and simultaneously prove their correctness. Moreover, PVS offers the possibility of translating an (executable subset of) PVS into common Lisp. Currently, these generated Lisp programs can be evaluated using the eval-rule of the ground evaluator. The PhD position on this subject focusses on the extension of PVS in such a way that specifications of realistic, real-size applications can be written. They idea is to specify/model these applications in PVS, to prove their correctness, and to translate these specifications into either a functional language (Clean) or an imperative language (C).

Candidates should have an excellent Master's degree in Computer Science, knowledge of formal methods, an interest in software analysis, model checking and verification, theorem proving and a strong background in some of these areas.

The positions involve a normal employment contract for a period of up to 4 years, and is expected to lead to a Ph.D. degree. The salary starts at about 1950 euro gross per month in the first year.

Applications should be submitted before the 19th of May 2006.

  1. Heap-space Usage.

    Amortized analysis is a technique which is used to obtain accurate bounds of resource consumption and gain. For the amortization analysis of a resource one considers not the worst case of a single operation but the worst case of a sequence of operations. A combination of amortization and type theory allows to check linear heap consumption bounds for functional programs with explicit memory deallocation.

    This project will be performed together with postdoc Olha Shkaravska. The project proposes to extend this combined method to a lazy functional language as well as to transfer the results of the functional programming community to the imperative object-oriented programming world by applying the amortized method to derive accurate bounds for heap usage of Java programs. In this way the potential impact of amortized analysis is increased significantly.

    For more information, contact Marko van Eekelen. You can apply by sending a letter of motivation and a detailed cv, and contact details of at least two references to marko@cs.ru.nl.

  2. Code-Model Conformance.

    The research topic is software analysis, in particular advanced techniques regarding the conformance of particular industrial software with formal models for a certain property. Target languages may typically be Java or C variants.

    Examples are conformity to finite state models, finite state model extraction, security information flow analysis, order dependencies and object extraction. Analysis is not restricted to formal automatic analysis. More typical an analysis will be the result of an interactive process in which the code is annotated manually and the analysis is performed semi-automatically.

    For more information, contact Marko van Eekelen. You can apply by sending a letter of motivation and a detailed cv, and contact details of at least two references to marko@cs.ru.nl.

  3. Generating Correct Software.

    The research consists of developing new translation techniques for different target languages and of investigating methods for modeling complex application issues, such as I/O, process communication and user interaction. When writing new applications it is recommendable to re-use existing software as much as possible. When using PVS it therefore becomes necessary to have an adequate way

    of characterizing existing software libraries. For the characterization itself, a translation of existing code into PVS is unavoidable. An interesting research topic is to explore techniques for extracting PVS-specifications out of programs (semi-)automatically.

    For more information, please contact Sjaak Smetsers (email: s.smetsers@science.ru.nl). You can apply by sending a letter of motivation, and a detailed cv to s.smetsers@science.ru.nl.

PhD Position on Analysis of Anonymity

There is a growing concern about the amount of personal digital information that is being gathered about people's actions. Websites habitually track people's browsing behavior, health care insurers gather medical data, and current trends in applications of RFID chips will enable tracking people's physical location. Hence, privacy and anonymity are increasingly at stake.

Anonymizing protocols counter this concern by offering anonymous communication over the Internet. To ensure the correctness of such protocols, which are often tricky and non-trivial and allow non-obvious attacks, a rigorous framework is needed in which anonymity properties can be expressed and analyzed. Whereas a wide variety of methods and tools exist for analysis of authentication and confidentiality protocols, research on anonymity properties has lagged behind.

The Analysis of Anonimity project at the Radboud University of Nijmegen aims at developing methods and tools to analyze anonymity protocols. The project proposal can be found here.

Candidates should recently have obtained a MSc in Computer Science or Mathematics, have a strong background in formal methods and interest in computer security. The position involves a normal employment contract for a period of up to 4 years, and is expected to lead to a PhD degree. The salary starts at about 1950 euro gross per month (plus benefits) in the first year.

For more information, contact Peter van Rossum <petervr@cs.ru.nl>. You can apply by sending a letter of motivation, a detailed cv, and contact details of at least two references. Applications should be submitted before May 19th 2006.