RICERCA ITALIANA     

SOFT - Security-Oriented Formal Techniques

Università "Ca' Foscari" di Venezia

Abstract

Security of software systems is a critical issue in a world where Information Technology is becoming more and more pervasive. The number of services for everyday life that are provided via electronic networks is rapidly increasing, as witnessed by the longer and longer list of words with the prefix "e", such as e-banking, e-commerce, e-government, where the "e" substantiates their electronic nature. These kinds of services usually require the exchange of sensible data and the sharing of computational resources, thus needing strong security requirements because of the relevance of the exchanged information and the very distributed and untrusted environment, the Internet, in which they operate. It is important, for example, to ensure the authenticity and the secrecy of the exchanged messages, to establish the identity of the involved entities, and to have guarantees that the different system components correctly interact, without violating the required global properties.
Unfortunately, many authoritative security-related organizations as, e.g., the CERT at Carnegie Mellon University, report a growing number of computer system vulnerabilities which are often the result of exploits against defects in the design or code of software. The approach most commonly employed to address such defects is to attempt to a posteriori "repair the flaw" by making it more difficult for those defects to be exploited. This solution, however, does not certainly >>>

Principal Investigator

Riccardo Focardi Università "Ca' Foscari" di VENEZIA

Research Objectives

Information security is becoming more and more relevant given the increasing usage of computers and networks for critical applications as, e.g, e-commerce, home-banking, purchase of digital goods and, in general, on-line services. It becomes thus very relevant to understand in depth the security requirements of distributed applications and to investigate methods for the automated verification of such requirements. The primary aim of the SOFT project is the study of foundations of information security and the development of formal methods for the specification and verification of security properties of programs, systems and computer networks. SOFT includes 3 Universities with 11 permanent researchers, 10 among PhD students and post-docs, 2 researchers from a foreign University and 2 contracts of 6-8 months specifically requested on this project research, for a total of 25 researchers. Research units are characterized by strong skills in formal methods for security, static analysis, abstract interpretation, verification of program properties and semantics of concurrency. The presence of two researchers from Saarland University of Saarbrücken and a PhD student co-tutored with the Ecole Polytechnique of Palaiseau shows the connection with important European research groups in the field.
We intend to cover many different aspects of security working both on high (i.e., application) level properties as, e.g., information flow and "Service-Oriented" security, and on >>>

First Results

For each work-package we give a list of the main expected results. These results are intentionally very specific, so to be verifiable, and will constitute the primary criteria for the evaluation of the success of the project. The contribution of these results with respect to the state of the art has been extensively illustrated in sections 12 and 13.


Expected results for WP1

Phase 1
- new formal models of trust for ad-hoc networks and integration of these models into suitable process calculi.
Phase 2
- a new security-oriented temporal logic for communicating processes.
Phase 3
- definition of an abstract interpretation of challenge-response authentication protocols;
- definition of new Control Flow Analyses for security protocols;
- extension of the verification tool proposed in [BBDNN05] to the new Control Flow Analyses;
- use of symbolic techniques and refinement for the verification of security properties;
- extension of AVISPA to the logic described in phase 2;
- investigation of possible extensions of AVISPA to other techniques developed in this WP.


Expected results for WP2

Phase 1
- definition of security-oriented imperative languages with cryptographic communication primitives;
- new abstract communication primitives that make programming independent of cryptographic implementation.
Phase 2
- new >>>

Timescale

24 months

National and international background

SOFT project will focus on diverse research topics related to the application of formal methods to security, that we shortly describe below. To clarify the connection with project targets we have grouped topics depending on the specific work-package they belong to.

- Communication and Network Security

Cryptographic protocols are one of the fundamental mechanisms for achieving security on computer networks. Wide-area networks are, in fact, not controllable and there is a need to protect sent/received data through cryptographic techniques. Even if these protocols are often just a few lines of codes, many attacks subverting the protocol logic and invalidating the expected security properties have been found. These attacks are not necessarily based on cryptographic flaws and can be reproduced even when cryptography is considered as a fully reliable black box. In the literature we find a huge amount of contributions on the analysis and verification of security protocols, but only a few of them follow a language-based approach, i.e., are based on static-analysis. We mention here some relevant papers on secrecy [A99,AB05] and authentication [BBDNN05, BFM07, GJ03, GJ04]. We intend to go on on this line of research by focussing on abstract interpretation and control flow analysis of cryptographic protocols and abstract communication primitives to make programming independent of cryptographic implementation. Moreover, we also aim to extend the symbolic >>>