Unit Research

Theme 1. Design and experiments with Network Aware Languages
A major research effort in the last four years of the group of Firenze has been the design and the implementation of a language for the development and proof of properties of distributed and mobile systems. The language has been named KLAIM, a Kernel Language for Agents Interaction and Mobility. The linguistic extension of KLAIM with constructs for supporting network aware programming, the tuning of its semantics and the development of case studies will be the main objective of the Firenze group.

Phase I
A first objective is to enrich KLAIM with linguistic abstractions for dealing with hierarchical nets, quality of service, and secure communications. In the current formulation, KLAIM permits describing essentially flat computer networks a` la Ethernet; the language will be generalized to permit design nets hierarchies that more faithfully represent architectures a` la Internet. The language will also be extended with suitable mechanisms for resource acquisition, fault tolerance, timeliness and for combining in a flexible way different, even contrasting, quality of service requirements. Finally, to protect sensible data that are exchanged in communications, KLAIM will also be extended with cryptographic primitives, based both on shared keys and on public/private keys. Keys will be used as a further parameter of the KLAIM primitives acting over tuple spaces. The new primitives will permit encrypting tuples added to tuple spaces that would be withdrawn only with appropriate keys. Moreover, we see collaborations with the groups of Pisa on research activities related to Theme 2, namely coordination and resource monitoring, as instrumental for additional linguistic enrichments supporting coordination and security policies.
Our experience using KLAIM has shown that its coordination constructs were too static to be able to meet evolving demands. More dynamic mechanisms will be added for guaranteeing programmable coordination policies that will permit dynamically negotiating the cooperation activities of mobile components, and controlling the access rights of mobile components over network services and resources. The new primitives will allow privileged processes/users to directly program and manage security policies. Such constructs will permit to wrap mobile components within customized execution contexts, acting as "guardians", that can intercept, and possibly redefine, all potentially dangerous components operations. We shall also study observational semantics for KLAIM applications based on equivalences or preorders. More abstract semantics are necessary to support modular programming and program verification. We shall define behavioural equivalences, temporal logics and equational systems that are a necessary support for the statement and the verification of systems properties.

Phase II
In this second phase, KLAIM will be enriched with linguistic abstractions for dealing with "open" systems, i.e. systems whose structure can change dynamically and unpredictably. KLAIM will be equipped with proper mechanisms for services lookup, for interaction among mobile components and resources, and for binding services to components.
Some work about this topic will be carried on jointly with the Pisa group.
By taking advantage of collaborations with the groups of Genova and of Pisa on research activities related to Theme 3, namely dynamic configuration and assembly of components, KLAIM will be further enriched with mechanisms supporting separate compilation and linking of code fragments, and execution of dynamically generated code.
Indeed, network aware applications has shown that mobile code tends to be generic, because often one wants to download software components, and small, because one wants to reduce communication costs. Moreover, mobile code is often written in an intermediate language (without the frills of a high-level language nor the machine-specific nature of a low-level language). We plan to extend the KLAIM programming model with staging mechanisms which support linking and specialization of mobile code based on information available only locally and permit assembling components and generating specialized code prior execution.
Finally, by relying on the KLAIM prototype implementations developed within Theme 5, we intend to experiment with the proposed programming abstractions on non-trivial network applications. We shall consider a set of case studies dealing with examples borrowed from the fields of electronic commerce and load balancing over distributed CPU's for assessing the different choices about linguistic constructs.

Theme 4. Types and calculi for secure distributed programming
Another research line investigated in the last few years by the group of Firenze has been the development of theories and tools that support reasoning on and verification of security aspects of concurrent, possibly distributed, systems. Along this research line, we plan to extend the KLAIM type system and the spi-calculus, a cryptographic extension of the pi-calculus. Other research efforts will be devoted to the study of event-based calculi and of calculi with object mobility.

Phase I
By making use of a capability-based type system, KLAIM provides direct support for expressing and enforcing security policies that control access to resources and data. In its current formulation, the KLAIM type system may turn out to be too restrictive because it requires fixing statically and independently for all processes their access rights with respect to systems resources. We intend to relax these constraints by enriching the actual type system with mechanisms supporting exchange and dynamic acquisition of access rights. This will permit to change at run-time the capabilities assigned to processes. This feature turns out to be essential when dealing with applications for e-commerce, and requires a more extensive dynamic type checking.
Regarding the spi-calculus, we aim at understanding the full impact of testing theory for this calculus by providing complete axiomatizations of the observational preorder. The axiomatization will be the basis for developing tractable proof techniques and for studying the foundations of security in mobile systems. We also plan to consider a distributed version of the language that includes operators for managing security policies in evolving networks. The new language should be sufficiently expressive to, e.g., be used for defining resource access policies for agents visiting a node of the network. We intend to study how this high level language could be implemented, via crypto-protocols, into the low-level cryptographic calculus. In view of studying the correctness of this implementation, we also plan to devise proof/verification techniques, and proof systems, for reasoning about contextual equivalences and security properties in the new language. The considered techniques should deal with both shared and public key cryptosystems.
For event-based calculi, we want to study a semantics for concurrency in terms of "algebra of contexts" and, as a first result, to prove a theorem relating operational and denotational semantics for a nontrivial fragment of a realistic language, like Java. This study will be afforded with usual tools of algebraic category theory, as well as with enriched category theory. It should be easy to look at algebraic models for Java in strict relation with event structures, therefore, a result connecting these two ways of looking at concurrency is expected. Calculi for object mobility will be also formulated. Here we take the word mobility to mean on one side "active" mobility, that is objects that have migration primitives (like agents), on the other a "passive" mobility, that is objects that may run in different environments (like scripting).

Phase II
In this second phase, the KLAIM type system will also be enriched with behavioural/history dependent types. We will design new, more intensional type operators, which do correspond to modal logics operators, suggested by an interpretation of types as logic formulae. This will permit to introduce in the type system more dynamical aspects that currently are only expressible in modal logic. The new type system will allow us to encode, by using types, temporal/causal dependences between access rights. As an example of such properties, a type can express the fact that a mobile component that executes over a host can perform remote outputs only until it does not perform local inputs. Moreover, in order to guarantee the well-typedness of a distributed system, in its current formulation the KLAIM type system needs to statically check the whole system. This is impossible to do in open systems, such as the Internet. To tackle this problem, we will extend the KLAIM type system with the possibility of making just a partial static type checking of those (trusted) locations whose behaviour has been completely specified. Of course, this will demand to enrich the KLAIM type system with proper mechanisms supporting a form of dynamic type checking that will be performed when mobile components coming from unchecked (untrusted) locations arrive at and should be executed by a trusted host location.
Some of the work about this topic will be carried on jointly with the groups of Pisa and of Torino.
As far as the spi-calculus is concerned, the proof/verification techniques developed in phase 1 will be used to prove correctness of the translations defined in phase 1. To assist this task, we also plan to implement the proposed techniques and put forward an automatic verification tool.

Theme 5. Virtual Machines and Prototype Implementation
We have already implemented KLAIM over a number of different platforms. For greater portability, we took advantage of the Java approach by compiling in intermediate code, which is independent from the underlying platform, and then interpreting the intermediate code.

Phase I
A first objective of our work is the prototype implementation of the new KLAIM linguistic abstractions developed within Theme 1. We also plan to port KLAIM on PDAs with Windows CE, using C++, and to create communication protocols to enable KLAIM components written in Java to communicate with C++ components running on Windows CE. A porting of KLAIM under C# is also planned.