SOJOURN · Security Of Java for rigorous and reliable networks
FP6 — Marie Curie Actions (Human Resources and Mobility)
- Duration
- 2005-12-07 → 2006-12-06
- EU contribution
- €76,611
- Participants
- 1
- Scheme
- EIF
Lines connect the coordinator with its partners.
Results in brief
Final Activity Report Summary - SOJOURN (Security of java for rigorous and reliable networks)
Our society increasingly relies on information technology to provide essential information and services, including in security- or privacy sensitive domains such as banking or health care. Here security protocols play a central role to secure communication over digital networks, for example the SSL protocol for securing Internet connections. The correctness and security of software components implementing such protocols is crucial to the security of any services using these networks. The highest degree of confidence in the security of such software components can be obtained by formal methods, which provide mathematical proofs to certify that software has the required properties. The SOJOURN project investigated this possibility; more in particular through the use of the formal specification language JML and the associated verification tool ESC/Java2. As a concrete case study the project studied an existing open source implementation of SSH, a security protocol used for remote logins. A concrete result of the project was that the particular implementation studied was found to be seriously flawed. Of more general interest was the systematic way in which this flaw was found. The methodology used was to formally specify a security protocol as a finite state machine, translate this specification to JML and use ESC/Java2 to prove (or disprove) that the implementation obeys this specification. The methodology highlights the value of finite state machines as simple but effective specification formalism. Other results of the project are in the field of (Java) program specification and verification. Here the main achievements are the extension of the ESC/Java2 tool to deal with alias control properties (using so-called universes) and the investigation of a notion of immutable object that can be statically enforced and which is guaranteed to be safe even in the presence of hostile code.
Data: CORDIS, © European Union
Project objective
Security protocols, such as SSL (Secure Socket Layer) implemented in web browsers, play a vital role in our society that increasingly relies on electronic networks, such as the Internet and mobile phone networks. Whereas there are now reasonably mature mathematical methods to study the security of these protocols, rigorous techniques to ensure the correctness and security of the software implementing them are still in their infancy. The development of such techniques is of particular importance, as many security problems are ultimately due to software bugs. In order to reinforce Seneca's maxim `If virtue precedes us every step will be safe', the SOJOURN project aims at the development of rigorous, tool-supported techniques to assess and improve the security of Java implementations of the security protocols, with SSL as a concrete case study.This is obviously an instance of a much more general problem, namely how to ensure the security of software. This is not just an issue of growing importance for the IT sector, but for society as a whole. It concerns all people as they increasingly rely on computerised networks in everyday life, e.g. for banking and health care, where security and privacy are very important. The fundamental scientific questions in this field of research -- how to identify relevant security properties, how to characterise and specify them, and how to ensure that they are met -- are still very much open questions. Surely, we cannot hope to solve these questions, but by concentrating our efforts in a specific area of security protocols, where the security issues are relatively clear, and by building on existing technologies and tools, we can expect to make an impact.
Original text from CORDIS.
Participants
- STICHTING KATHOLIEKE UNIVERSITEIT · NIJMEGENCoordinatorNetherlands
Links
Data: CORDIS, © European Union