| Acronym: Confident |
| Main Objective: The World Wide Web has grown from an infrastructure for document repository and retrieval to a platform for distributed applications. At the same time, modern web-based applications make use of a multitude of different technologies, including, e.g., those for the client side, for the server side, for the transport layer, and those for data management. Furthermore, short, casual scripts have given place to applications built from thousands of lines of code. At the same time, the quest for agile, reactive, web- based interaction, lead to the emergence of the REST (Representational State Transfer) architecture, which, for its simplicity, has been gradually replacing the more traditional SOAP and WSDL-based Web Services. As of today, ‘developing for the Web’ largely remains an undertaking supported by guidelines and best practices, lacking in general appropriate methodology and tool support, and where most if not all verification is performed at runtime. When available, tools for Web development are essentially those one finds for more conventional software development. On what concerns programming, scripting languages is the norm for client-side development. Such languages are essentially dynamically typed. The best one can find these days are static analysis tools, often in the form of traditional type systems, that essentially check local computations (e.g., the parameters to operators or the input-output behaviour of functions). RESTful applications require further support at development time, namely on what concerns the continued interaction among principals. Typical problems include the verification of whether a given resource is available at a given point in a complex interaction, or whether the client is authorised to access a given resource. The problem is exacerbated by the fact that server replies may point to further resources that will shape future interactions. At the heart of CONFIDENT lies the notion of Communication Contract, a global description of the interaction behaviour of complex distributed applications that brings together the roles each participant plays in a given computation. The nature of Communication Contracts, encompassing global communication descriptions of all principals involved, are equipped with a number of properties that foster reliable development of web applications. With CONFIDENT, Communication Contracts will guide the software development lifecycle for web-based distributed applications, in particular: a) the verification of source code against contracts, making sure that processes behave as the prescribed by the protocol they are supposed to follow, hence will not incur communication-related runtime errors; and b) the static validation of security requirements of applications, including authentication and resource access authorisation. The main objective of CONFIDENT is to develop and evaluate tools and technology for describing, inferring, and statically verifying component communication contracts for effective construction and evolution of complex distributed systems, notably JavaScript applications. To achieve this we will: 1) Integrate the theory of behavioural type systems, session types in particular, into a notion of communication contracts, effective in driving the software development life cycle, in particular that of RESTful JavaScript applications; 2) Develop a language of communication contracts for JavaScript, and use it to statically verify components, infer communication types from code, and to provide for the gradual evolution of existing code bases. 3) To support the development, verification, and refactoring of reliable web-based systems by developing a suite of integrated tools for supporting the software development lifecycle; 4) Evaluate the new software methodologies and associated tools and methodologies for engineering distributed applications using a few case studies. |
| Reference: PTDC/EEI-CTP/4503/2014 |
| Funding: FCT |
| Start Date: 01-05-2016 |
| End Date: 01-05-2019 |
| Team: Pedro Miguel dos Santos Alves Madeira Adão, Paulo Alexandre Carreira Mateus |
| Groups: Security and Quantum Information - Lx |
| Partners: Fundação da Faculdade de Ciências da Universidade de Lisboa (FFC/FC/UL) |
| Local Coordinator: Pedro Miguel dos Santos Alves Madeira Adão |
|
|
|
Associated Publications
|
