Convocatoria: 4º Convocatoria a Proyectos STIC AmSud
Fuente de financiamiento: STIC AmSud
Duración: 24 meses.
Fecha de aprobación: diciembre de 2008.
Fecha de comienzo: marzo de 2009.
Fecha de finalización: marzo de 2011.
Palabras clave: Secure Programs, Formal Methods, Type Theory, Logic.
Resumen
Computing has undergone a clear paradigm shift towards open ended, global interaction. Distributed services are uniformly being provided at a global level. This brings along new challenges to the computer science community in terms of engineering, security, interoperability and more.
One promising approach to these issues is that of Language based Security, a recent area which advocates the use of advanced programming language techniques to guarantee correctness and security properties of software at the source code level.
We propose addressing two important problems from a language based security perspective by resorting to a form of static program analysis called Type Systems. The first is to apply type theory to guarantee correct component interaction in a multi-party system.
These types may be seen as sequences of data types indicating the order in which interaction should take place and also the nature of the information that is to be exchanged. A number of questions arise as to the applicability of session types in real world situations. It has been suggested that session types could be used as choreography specification of web services.
One avenue we would like to pursue is the applicability of session types as a formal foundation for W3C's Web Services Choreography Description Language. On the other hand, new theoretical results are sought for.
One important task is that of establishing formal guarantees that the underlying theory of session types is mathematically robust particularly due to some bugs reported recently in some of the published literature.
This may be achieved by suitable formalization of session types in type theories. Another task is to extend session types with more expressive type features. The second issue we address is that of applying type systems to enforce correct string formation patterns in programming languages.
Many web-based client-server systems operate by means of the client generating queries encoded as strings to be executed at the server side.
This raises well-known security vulnerabilities such as cross site scripting and SQL injection attacks whereby a malicious client can spoof strings that encode queries or shell commands which were not intended by the programmer.
One promising technique that has emerged as a partial solution to this problem is to rely on type systems to approximate the values that strings take and then determine whether they are of the expected form or not.
Recent work on this form of type based string analysis only addresses toy languages such as simple extensions of the lambda calculus. It would be interesting to see how this applies to object oriented languages and to large scale languages.