Security through Analysis and Verification

Security is a fast growing area of Computer Science, with increasing relevance to real life applications such as internet transactions, electronic commerce and smart cards. Already for some time, techniques from program verification and program logics have been used to validate the correctness of secure communication protocols. Recent work suggests that techniques from program analysis and type systems may allow fully automatic validation of systems against certain types of attack. These techniques work directly on the program rather than some specification that may then have been incorrectly implemented.

This seminar aims at identifying and studying those ingredients of security that may be addressed by analyzing programming languages and programming constructs using techniques from program verification, type systems or program analysis. We would also like to compare these approaches to those focusing on specification techniques, dynamic analysis for information flow or specific techniques from cryptography.

On the security side the seminar will involve a classification of the appropriate semantic notions for the key security concepts: confidentiality, integrity, authentication, watermarking, prevention of denial of service, auditing etc. Special interest centers on approaches to capturing the semantic differences between different classes of security concepts (e.g. confidentiality versus authentication) and on the design of robust communication protocols; this involves clearly defining how one detects breaches of security and what assumptions can be made on the attacker (e.g. can an attacker only observe the outcome of computations or can he also inspect the internal operation of the system).

On the analysis side the seminar will involve a survey of the results that have been achieved. Verification has been used for showing the correctness of protocols. Type systems with security annotations have been used to ensure integrity and safety; type and effect systems may be used for extracting the inherent protocols used for communication in programs (including legacy code and code purchased from sub-contractors) so as to allow validating the overall protocol of a software system. Control flow analyses have been used for devising tests that can be used to validate key software components against infinitely many attackers by using a deep understanding of the analysis to construct an attacker that is as hard to protect against as any other attacker (in the manner of hard problems for complexity classes). Points to consider are the extent to which the cryptographic scheme is essential for the static approach to analyzing systems and whether or not static approaches are able to deal with the probabilistic notions arising from the semantic considerations.

We would like to gather researchers who work on problems quite close, sometimes with similar mathematical tools, and who have seldom the opportunity to compare their proposals: Cross-fertilization should be one of the main outcomes of this Seminar. Also we hope to identify a number of challenges (to the formal description of security, and to the static techniques aiming at establishing them) that can serve as a guide for further research.

Furthermore, we want to get a clear perspective on the relevance of the issues studied and the solutions proposed. To this extent we would like to gather also researchers working on more practical aspects of security. The pious hope is that we will be able to take a first step to bridge the gap between "theoretically" motivated research on security and "practically" motivated research.