Unit Papers

This work presents an object-oriented calculus based on higher-order mixin construction via mixin composition, where some software engineering requirements are modeled in a formal setting allowing to prove the absence of message-not-understood run-time errors. Mixin composition is shown to be a valuable language feature enabling a cleaner object-oriented design and development. In what we believe being quite a general framework, we give directions for designing a programming language equipped with higher-order mixins, although our study is not based on any already existing object-oriented language.

We design a calculus that combines class-based features with object-based ones, with the aim of fitting into a unifying setting the ``best of both worlds''. In a mixin-based approach, mixins are seen incomplete classes from which incomplete objects can be instantiated. In turn, incomplete objects can be completed in an object-based fashion. Our hybrid calculus is shown to be useful in some real world scenarios that we present as examples.

Standard class-based inheritance mechanisms, which are often used to implement distributed systems, do not seem to scale well to a distributed context with mobility. In this paper, a mixin-based approach is proposed for structuring mobile object-oriented code and it is shown to fit in the dynamic and open nature of a mobile code scenario. We introduce MoMi (Mobile Mixins), a coordination language for mobile processes that communicate and exchange object-oriented code in a distributed context. MoMi is equipped with a type system, based on polymorphism by subtyping, in order to guarantee safe code communications.

MoMi (Mobile Mixins) is a coordination language for mobile processes that communicate and exchange object-oriented code in a distributed context. MoMi's key idea is structuring mobile object-oriented code by using mixin-based inheritance. Mobile code is compiled and typed locally, and can successfully interact with code present on foreign sites only if its type is subtyping-compliant with what is expected by the receiving site. In this paper, we study a subtyping relation for MoMi that includes both subtyping-in-width and subtyping-in-depth, in order to achieve a significantly more flexible, yet still simple, communication pattern. Technical problems arising from this extension are solved by a static annotation procedure.

This paper presents O'Klaim (Object-Oriented Klaim), a linguistic extension of the higher-order calculus for mobile processes Klaim with object-oriented features. Processes interact by an asynchronous communication model: they can distribute and retrieve resources, sometimes structured as incomplete classes, i.e., mixins, to and from distributed tuple spaces. This mechanism is coordinated by providing a subtyping relation on classes and mixins, which become polymorphic items during communication. We propose a static typing system for: (i) checking locally each process in its own locality; (ii) decorating object-oriented code that is sent to remote sites with its type. This way, tuples can be dynamically retrieved only if they match by subtyping with the expected type. If this pattern matching succeeds, the so retrieved code can be composed with local code, dynamically and automatically, in a type-safe way. Thus a global safety condition is guaranteed without requiring any additional information on the local reconfiguration of local and foreign code, and, in particular, without any further type checking. Finally, we present main issues concerning the implementation of O'Klaim.

Class inheritance and dynamic binding are the key features of object-oriented programming and they permit designing and developing complex systems. However, standard class inheritance is essentially static and cannot be directly employed for modeling dynamic object behaviors. In this paper we propose a linguistic extension of Java, called Dec-Java, that is partially inspired by the decorator design pattern. This extension permits easily separating the basic features of objects (that are likely not to change during the application) from their behaviors (that, instead, can be composed dynamically at run-time). Thus, Dec-Java enables a dynamic extension and specialization of object responsibilities.

The tuple space communication model, such as the one used in Linda, provides great flexibility for modeling concurrent, distributed and mobile processes. In a distributed setting with mobile agents, particular attention is needed for protecting sites and information. We have designed and developed a Java middleware, Klava, for implementing distributed tuple spaces and operations to support agent interaction and mobility. In this paper, we extend the Klava middleware with cryptographic primitives that enable encryption and decryption of tuple fields. We describe the actual implementation of the new primitives and provide a few examples. The proposed extension is general enough to be applied to similar Java frameworks using multiple distributed tuples spaces possibly dealing with mobility.

The wide-spreading of Internet has stimulated the introduction of new programming paradigms and languages that model interactions among hosts by means of mobile agents, and that are centered around the notions of location awareness. In this paper we show how to use formal tools, specifically a modal logic, for formalizing properties for mobile agent systems. We concentrate on one of these new languages, Klaim, and we use it to specify a system that permits maintaining the software installed on several heterogeneous computers distributed over a network by taking advantage of the mobile agent paradigm.

We describe a system that permits maintaining the software installed on several heterogeneous computers distributed over a network by taking advantage of the mobile agent paradigm. The applications are installed and updated only on the central server. When a new release of an application is installed on the server, agents are scattered along the network to update the application on the clients. To build a prototype system we use X-Klaim, a programming language specifically designed to program distributed systems composed of several components interacting through multiple tuple spaces and mobile code.

Highly distributed networks have now become a common infrastructure for a new kind of wide-area distributed applications whose key design principle is network awareness, namely the ability of dealing with dynamic changes of the network environment. Network-aware computing has called for new programming languages that exploit the mobility paradigm as a basic interaction mechanism. In this paper we present the architecture of Klava, an experimental Java package for distributed applications and code mobility. We explain how Klava implements code mobility by relying on Java and show a few distributed applications that exploit mobile code and are programmed in Klava.

The structure of open nets, like the Internet, is highly dynamic, as the topology of component networks continuously evolves. In this context, node connectivity is a key aspect and a language for distributed network-aware mobile applications should provide explicit mechanisms to handle it. In this paper, we address the problem of expressing dynamic changes of node connectivity at linguistic level and, in particular, we focus on a slight extension of the language Klaim, that is targeted to this aim. The extension consists of the introduction of a new category of processes that, in addition to the standard process operations, can execute a few new coordination operations for establishing new connections, accepting connection requests and removing connections. Our extension puts forward a clean separation between the coordinator level and the user level and, hence, it is modular enough to be easily applicable also to other network-aware languages. We will also show that our approach can be used as a guide for actual distributed (i.e. without a single centralized server) implementations of mobile systems.

A general framework for network aware programming is presented that consists of a language for programming mobile applications, a logic for specifying properties of the applications and an automatic tool for verifying such properties. The framework is based on XKlaim, eXtended Klaim, an experimental programming language specifically designed to program distributed systems composed of several components interacting through multiple tuple spaces and mobile code. The proposed logic is a modal logic inspired by Hennessy-Milner logic and is interpreted over the same labelled structures used for the operational semantics of XKlaim. The automatic verification tool is based on a complete proof system that has been previously developed for the logic.

Fusion calculus is commonly regarded as a generalisation of pi-calculus. Actually, we prove that there is no uniform fully abstract embedding of pi-calculus into Fusion. This fact motivates the introduction of a new calculus, D-Fusion, with two binders, lambda and nu. We show that D-Fusion is strictly more expressive than both pi-calculus and Fusion. The expressiveness gap is further clarified by the existence of a fully abstract encoding of mixed guarded choice into the choice-free fragment of D-Fusion.

We study trace and may-testing equivalences in the asynchronous versions of CCS and pi-calculus. We start from the operational definition of the may-testing preorder and provide for it finitary and fully abstract trace-based characterizations, along with a complete in-equational proof system. We also touch upon two variants of this theory, by first considering a more demanding equivalence notion (must-testing) and then a richer version of asynchronous CCS. The results throw light on the difference between synchronous and asynchronous communication and on the weaker testing power of asynchronous observations.

Observational equivalences can be used to reason about the correctness of security protocols described in the spi-calculus. Unlike in CCS or in pi-calculus, these equivalences do not enjoy a simple formulation in spi-calculus. The present paper aims at enriching the set of tools for reasoning on processes by providing a few equational laws for a sensible notion of spi-bisimilarity. We discuss the difficulties underlying compositional reasoning in spi-calculus and show that, in some cases and with some care, the proposed laws can be used to build compositional proofs. A selection of these laws forms the basis of a proof system that we show to be sound and complete for the strong version of bisimilarity.

Recently there has been much interest towards using formal methods in the analysis of security protocols. Some recent approaches take advantage of concepts and techniques from the field of process calculi. Process calculi can be given a formal yet simple semantics, which permits rigorous definitions of such concepts as `attacker', `secrecy' and `authentication'. This feature has led to the development of solid reasoning methods and verification techniques, a few of which we outline in this paper.

The explicit management of Quality of Service (QoS) of network connectivity, such as, e.g., working cost, transaction support, and security, is a key requirement for the development of the novel wide area network applications. In this paper, we introduce a foundational model for specification of QoS attributes at application level. The model handles QoS attributes as semantic constraints within a graphical calculus for mobility. In our approach QoS attributes are related to the programming abstractions and are exploited to select, configure and dynamically modify the underlying system oriented QoS mechanisms.

Klaim is an experimental programming language that supports a programming paradigm where both processes and data can be moved across different computing environments. The language relies on the use of explicit localities, and on allocation environments that associate logical localities to physical sites. This paper presents a temporal logic for specifying properties of Klaim programs. The logic is inspired by Hennessy-Milner Logic (HML) and the mu-calculus, but has novel features that permit dealing with state properties to describe the effect of actions over the different sites. The logic is equipped with a consistent and complete proof system that enables one to prove properites of mobile systems.

This paper describes the design and the semantics of MetaKlaim, an higher order distributed process calculus equipped with staging mechanisms. MetaKlaim integrates MetaML (an extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (like assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and ``traditional'' computational activities on a wide area network (like remote communication and code mobility). MetaKlaim exploits a powerful type system (including polymorphic types á la system F) to deal with highly parameterized mobile components and to dynamically enforce security policies: types are metadata which are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide are network applications are maintained whenever computations interoperate with potentially untrusted components.

This paper describes the design and the semantics of MetaKlaim, an higher order distributed process calculus equipped with staging mechanisms. MetaKlaim integrates MetaML (an extension of SML for multi-stage programming) and Klaim (a Kernel Language for Agents Interaction and Mobility), to permit interleaving of meta-programming activities (like assembly and linking of code fragments), dynamic checking of security policies at administrative boundaries and ``traditional'' computational activities on a wide area network (like remote communication and code mobility). MetaKlaim exploits a powerful type system (including polymorphic types a la system F) to deal with highly parameterized mobile components and to dynamically enforce security policies: types are metadata which are extracted from code at run-time and are used to express trustiness guarantees. The dynamic type checking ensures that the trustiness guarantees of wide are network applications are maintained whenever computations interoperate with potentially untrusted components.

In the Mobile Ambients of Cardelli and Gordon an ambient is a unit for mobility, which may contain processes (data) and sub-ambients. Since the seminal work of Cardelli and Gordon, several ambient-based calculi have been proposed (Seal, Box-Pi, Safe Ambients, Secure Safe Ambients, Boxed Ambients), mainly for supporting security. At the operational level these (box- and) ambient-based calculi differ only in the capabilities of processes. We propose a way of extending ambient-based calculi, which embodies two principles: an ambient is a unit for monitoring and coordination, the name of an ambient determines its (monitoring and coordination) policy. More specifically, to each ambient we attach a guardian, which monitors the activity of sub-components (i.e. processes and sub-ambients) and the interaction with the external environment. In our proposal, guardians and processes play a dual role: guardians are centralized entities monitoring and inhibiting actions, while processes are decentralized entities performing actions. We exemplify the use of guardians for enforcing security properties.

Security is a key issue for distributed systems/applications with code mobility, like, e.g., e-commerce and on-line bank transactions. In a scenario with code mobility, traditional solutions based on cryptography cannot deal with all security issues and additional mechanisms are necessary. In this paper, we present a flexible and expressive type system for security for a calculus of distributed and mobile processes. The type system has been designed to supply real systems security features, like the assignment of different privileges to users over different data/resources. Type soundness is guaranteed by using a combination of static and dynamic checks, thus enforcing specific security policies on the use of resources. The usefulness of our approach is shown by modeling the simplified behaviour of a bank account management system.

muKlaim is a process language that permits programming distributed systems made up of several mobile components interacting through multiple distributed tuple spaces. We present the language and a type system for controlling the activities, e.g. access to resources and mobility, of the processes in a net. By dealing with privileges acquisition, the type system enables dynamic variations of security policies. We exploit a combination of static and dynamic type checking, and of in-lined reference monitoring, to guarantee absence of run-time errors due to lack of privileges and state two type soundness results: one involves whole nets, the other is relative to subnets of larger nets.

We present a programming notation aiming at protecting the secrecy of both host and agent data in global computing applications. The approach exploits annotations with sets of node addresses, called regions. A datum can be annotated with a region that specifies the network nodes that are allowed to interact with it. Network nodes come equipped with two region annotations specifying the nodes that can send data and spawn processes over them. The language semantics guarantees that computation proceeds according to these region constraints. To minimize the overhead of runtime checks, a static compilation phase is exploited. The proposed approach is largely independent of a specific programming language; however, to put it in concrete form, here we focus on its integration within the process language muKlaim. We prove that in compiled muKlaim nets, data can be manipulated only by authorized users. We also give a more local formulation of this property, where only a subnet is compiled. Finally, we use our theory to model the secure behaviour of a UNIX-like multiuser system.

Security is a key issue for distributed systems/applications with code mobility, like, e.g., e-commerce and on-line bank transactions. In a scenario with code mobility, traditional solutions based on cryptography cannot deal with all security issues and additional mechanisms are necessary. In this paper, we present a flexible and expressive type system for security for a calculus of distributed and mobile processes. By using a combination of static and dynamic checks, type safety and well-typedness preservation can be guaranteed, thus enforcing specific security policies on the use of resources. The usefulness of our approach will be shown by modeling the simplified behaviour of a bank account management system.

microKLAIM is a process language that permits programming distributed systems made up of several components interacting through multiple distributed tuple spaces. We present the language and a type system for controlling the activities, e.g. access to resources and mobility, of the processes in a net. By dealing with privileges acquisition and consumption, the type system enables dynamic variations of security policies. We exploit a combination of static and dynamic type checking, and of in-lined reference monitoring, to guarantee the absence of run-time errors due to lack of privileges and show two type safety results: one involves whole nets, the other is relative to subnets of larger nets.

Klaim (Kernel Language for Agents Interaction and Mobility) is an experimental language specifically designed to program distributed systems consisting of several mobile components that interact through multiple distributed tuple spaces. Klaim primitives allow programmers to distribute and retrieve data and processes to and from the nodes of a net. Moreover, localities are first-class citizens that can be dynamically created and communicated over the network. Components, both stationary and mobile, can explicitly refer and control the spatial structures of the network. This paper reports the experiences in the design and development of Klaim. Its main purpose is to outline the theoretical foundations of the main features of Klaim and its programming model. We also present a modal logic that permits reasoning about behavioural properties of systems and various type systems that help in controlling agents movements and actions. Extensions of the language in the direction of object oriented programming are also discussed together with the description of the implementation efforts which have lead to the current prototypes.

Building on recent work by Rutten on coinduction and formal power series, we define a denotational semantics for the csp calculus and prove it fully abstract for testing equivalence. The proposed methodology allows for abstract definition of operators in terms of behavioural differential equations and for coinductive reasoning on them, additionally dispensing with continuous order-theoretic structures.

Automatic methods developed so far for analysis of security protocols only model a limited set of cryptographic primitives (often, only encryption and concatenation) and abstract from low-level features of cryptographic algorithms. This paper is an attempt towards closing this gap. We propose a symbolic technique and a decision method for analysis of protocols based on modular exponentiation, such as Diffie-Hellman key exchange. We introduce a protocol description language along with its semantics. Then, we propose a notion of symbolic execution and, based on it, a verification method. We prove that the method is sound and complete with respect to the language semantics.

We present STA (Symbolic Trace Analyzer), a tool for the analysis of security protocols. STA relies on symbolic techniques that avoid explicit construction of the whole, possibly infinite, state-space of protocols. This results in accurate protocol modeling, increased efficiency and more direct formalization, when compared to finite-state techniques. We illustrate the use of STA by analyzing two well-known protocols, asymmetric Needham Schroeder and Kerberos. We discuss the results of this analysis, and contrast them with previous work based on finite-state model checking.