INTERFACES - Certified Interfaces for Integrity and Security in Extensible Web-based Applications
Start Date: 2009 Expected completion date: 2012
PIs: Luís Caires, Frank Pfenning
Dual Degree Ph.D. Student: Filipe David Oliveira Militão (Computer Science)
Teams: Universidade Nova de Lisboa (UNL), Faculdade de Ciências da Universidade de Lisboa (FCUL), Universidade de Carnegie Mellon
The project aims at the development of new techniques for enforcing security, integrity, and correctness requirements on distributed extensible web‐based applications by introducing novel, semantically rich notions of interface description languages, based on advanced type systems and logics. The increasing availability of Internet‐based services and of various sorts of devices with substantial computing and networking abilities is contributing to the growth of a global software infrastructure upon which the general society is becoming more and more dependent. This computing infrastructure is under permanent extension and active modification by parties working independently, even if it must support critical businesses and activities.
Among the most successful applications built on this infrastructure one finds particularly critical services, such as those that need to securely exchange information with previously unknown parties (for example, web portals), and applications willing to modify or extend their functionality in a trustworthy and reliable way, without interrupting operation (for example, a web browser). We also find applications that need to exchange not only data but also executable programs (either in the form of compiled code or in the form of other interpretable specifications, such as XML descriptions), and to reconfigure themselves in order to select and bind to suitable partners, a kind of behavior present in service oriented systems, such as those based on web‐service technology. Common instances of extensible network‐based applications include complex, reconfigurable applications such as enterprise information systems, required to evolve at the rapid pace that today's businesses need, and even general purpose devices such as mobile phones and PDAs, that keep increasing their computational capabilities everyday. Enforcing security, integrity and correctness requirements in such open and extensible applicational scenarios raises many challenges.
How can we make sure that the mechanisms made available for allowing the execution of foreign code will not open the door to virus infections? How can we combine runtime monitoring with static analysis of code when programs run on multiple, possibly untrusted environments? How would it be possible to validate that dynamic updates to running applications will not violate the prescribed security and integrity constraints? How can we guarantee that a web‐service collaboration does not violate the intended message interaction sequence, as defined by previously agreed business protocols, or does not exceed reasonable bounds on resource usage, as prescribed by a service level agreement? How can we incorporate in programming languages, analysis tools, and execution infrastructures, proof procedures and algorithms able to certify properties far beyond the usual type safety, such as secrecy, authenticity, concurrency control, access control, and conformance to protocols? In general terms, how can we define, in mathematical precise ways, the expectations and requirements of software fragments, so that software developers may determine as early as possible, ideally at compile or link time, that combinations will not break the intended key integrity constraints?
In this project we intend to approach these challenges by developing new notions of semantically rich interface languages, and associated programming language and logic based verification techniques.
• Define logic and type based interface languages for describing security and integrity properties of distributed extensible applications or services on the Internet.
• Develop programming models and languages supporting rich interface languages, amenable to formal analysis, based on logical reasoning, type checking and model-checking, in the context of high-level specifications of integrity and security requirements.
• Produce implementations of prototypes for specification, programming, and reasoning about case studies, including scenarios provided by an industrial strength web-based application development environment.