RICERCA ITALIANA     

Logical Foundations of Distributed Systems and Mobile Code

Università "Ca' Foscari" di Venezia

Abstract

Modern computer programs are increasingly being developed in support of distributed applications at different levels of abstractions, from IP-level communication protocols for mobile devices, such as IPv6, to application-level business transactions and e-commerce systems. The computing environments in which such programs operate are inherently open-ended, characterized by the absence of centralized structures, and built upon physical or virtual networks with complex structure and dynamic communication capabilities and services.

The role of formal methods for specification, analysis and verification is indisputable in this context as, given the size of the applications, and the complexity of the underlying computing environments, software development may not forego rigorous assessment before deployment. Yet, classical specification methods and verification techniques do not scale here. Firstly, the absence of centralized control, distinctive of open systems, invalidates the effectiveness of traditional verification methods which too often rely on the existence of precise, and reliable, assumptions on the structure and behavior of all system components to be analyzed and validated. Secondly, a number of core observables properties for computations in open systems, such as such as failures due to time-outs, delays due to shortage of communication bandwidth, quality of service parameters for communication links and other resource-centric parameters, remain largely unaddressed by current specification methods and analysis techiques.

The purpose of the project is to advance the state of the art on concurrency theoretic techniques for software analysis and verification, so as to make them more expressive and effective under the weaker and possibly partial assumptions on structure and behavior distinctive of the systems and applications of interest. More specifically, our research will focus on:
. the study of new expressive concurrency theoretic models for distributed computation in systems with name and code mobility;
. the development of formal techniques for the analysis and verification of process behavior in contexts with decentralized structure, limited trust, and partial knowledge about the context's components.

To keep the project focussed, and monitor its progress towards its objectives, the theories and techniques developed will be tested on a set of case studies representative of the systems of interest. <<<

Principal Investigator

Michele BUGLIESI Università "Cà Foscari" di VENEZIA

Research Objectives

Remote execution is an old and venerable topic in research on distributed systems, targeted at the development of techniques to support the sharing of computing power among distributed machines. The new advances in telecommunication tecnology have created revived interest and new challenges for this programming paradigm.

Modern computer programs are increasingly being developed to support distributed applications and protocols at different levels of abstractions, from IP-level communication protocols for mobile devices, such as IPv6, to application-level business transactions and e-commerce systems. The computing environments in which such programs operate are built upon physical or virtual networks with complex structure and dynamic communication capabilities and services. In addition, at all levels of abstractions these environments are inherently open-ended, and characterized by the absence of centralized structures of control, trust, and authorization.

The role of formal methods for specification, analysis and verification is indisputable in this context as, given the size of the applications, and the complexity of the underlying computing envronments, software development may not forego rigorous assessment before deployment. Yet, classical specification methods and verification techniques do not necessarily scale here: the absence of centralized control, distinctive of open systems, invalidates the effectiveness of traditional verification methods which too often rely on the existence of precise, and reliable, assumptions on the structure and behavior of all system components. Classical specification and verification techniques also fall short of providing adequate characterizations of core observable properties of computations in open systems, such as failures due to time-outs, delays due to shortage of communication bandwidth, metrics to establish quality of service parameters for communication links and other resource-centric parameters.

Objectives and approach
The purpose of the project is to advance the state of the art on concurrency theoretic techniques for software analysis and verification, so as to make them (i) more expressive, hence able to capture the relevant observable properties of distributed computations, and (ii) effective under the weaker and possibly partial assumptions on structure behavior distinctive of the systems and applications of the computing environments of interest. Generally stated, the objective of the project is twofold, and includes:

. The study of abstract models of mobile computation in distributed environments, based on process calculi. Such models will support formal reasoning on code execution and migration, context exploration and adaptive behavior based on new, resource-oriented observables and associated behavioral equivalences.
. The development of formal techniques, based on types and logical systems, for the specification and verification of concurrent program behavior. Such techniques should make it possible to express the admission/authorization policies for code migration to remote computational environments and, dually, to control the mechanisms of access, negotiation, monitoring, protection and use of the local resources available at such environments.

Our approach will be centred on theory, with the goal of isolating core unifying notions to yield effective techniques for analysis and verification tools, but at the same time complemented by work on case studies to assess the theoretical results and evaluate their advance.

The theoretical work we plan draws on operational models and proof-theoretic tools for analysis and verification. The theory of concurrency has long provided powerful foundational tools for reasoning on the (contextual) behavior of concurrent processes, and for analyzing and specifying their behavior by means of type and logical systems. Consolidated progress has been made over the years on applying these tools on first-order process calculi and, to some extent, also to calculi for name mobility like the pi-calculus.
In the context of the present proposal, we seek to extend the existing techniques to processes and systems whose components are mobile, distributed, open, (partially) typed, possibly untrusted.
We propose to use types and logical formulas as interfaces, or as contracts, expressing and governing the negotiation for resource acquisition between processes and their environments. The use of coinductive and logical characterizations of the corresponding behavioral equivalences will then provide finitary representations of contexts and serve as the basis for formal analysis of the observable effects of process execution in such contexts. Innovation will be required to find adequate characterizations of resource usage and management - bounds, protection, authorization, confinement. Similarly, novel techniques will be needed to formalize mechanisms for client code to discover and acquire its resources, by migrating over a distributed network with dynamic spatial structure and connectivity and dynamic access/authorization rights.
Static analysis, based on type and logical (inference) systems, is our proposed solution to reduce the overhead incurred by executions that need to self-tune on the basis of the context information. Such analysis will contribute to provide verifiable certificates for client code to prove that it complies with the access control policies of its hosting environment. Similarly, they will provide estimates of resource usage to help minimize the cost of the run-time accesses to context information.

The techniques and tools developed will be put to test on a set of case studies. While finding relevant cases of study is in itself an objective of the project, we already have plans to work on two, largely orthogonal scenarios. The first concerns the specification and analysis of protocols to regulate communication and routing in wireless ad-hoc networks. While ad-hoc networks are interesting in themselves for the mobility-intensive nature, the routing protocols are relevant for the project as they are cooperative in nature and require adequate forms of trust to be established among the peers that participate in the routing. As such, these protocols provide a significant example of the consequences of absence of centralized control and trust in distributed computations. The second scenario addresses the nowadays common practice by users to dowload code to run on their devices --laptops, PDAs, etc. The focus here will be on techniques to detect and anticipate various security threats, from attacks to the privacy and integrity of data to denial-of-service attacks based on over-use of system resources, mounted by malicious agents hosted in the downloaded code.

The purpose of the work on case studies is twofold. On one hand, it will help concretely stimulate and steer the theoretical work by providing problem-specific challenges and continued feedback to the activities in workpackages WP1-3. On the other side, it will provide a measurable indicator to evaluate the project's progress towards its objectives and to assess the quality of its results.

The structure and a detailed account of the project activities is given the workplan section of the present proposal. <<<

Timescale

24 months

National and international background

Types, logics and advanced techniques for equational reasoning are emerging as powerful tools for the analysis of distributed computations and open systems. Areas of particular relevance to the present proposal are related to the ability of types and logics to talk about resources and their usage, of typed equational theories to characterize observational properties of processes and their capture the spatial structure of systems. We briefly outline some relevant background below.

Type systems
Resource and mobility control, in diverse incarnations, has been the focus of extensive foundational research in type theory. Topics considered include the ability to read from and to write to a channel [PS96], the control of the location of channel names [YH99], the guarantee that distributed agents will access resources only when allowed to do so [HR02,CGZ01,BCC01,HMR03], the control of interference [LS03], the control of mobility, based on type-based permissions [DS00,MS02,CGG02,CDGS03], the guarantee of safety within local computational environments [CGG02], their secrecy [CGG00], the control on the flow and sharing of information, based on content and context [Mye99,CDV03].

With few exceptions, most of these systems rely on classical typing techniques whereby all the system components are type-checked under the same global typing assumptions. This is clearly unrealistic in distributed and dynamic environments as the ones of interest to the project. One solution to overcome this limitation is to rely on cryptographic primitives to protect trusted (i.e. typed) migrating agents against the untrusted sites they traverse, and to rely on a type system that separates trusted and untrusted code, while allowing safe interactions with untrusted sites [BCPS03]. An alternative solution is to rely on dynamic type checking, to contrast and validate the local assumptions made about remote components when such components interact [BC01,HR02,DFPV00]. In some cases [BC01,CDGS03] dynamic typing techniques have been formulated in terms of type inference systems extracting typing informations from untyped code to approximate the code's behavior. Such techniques are especially relevant, and effective, for systems which admit principal types, or typings, a property which is essential for compositional type analysis [W02].

Other static analysis techniques have been applied to extract information on the behavior of terms of typed or untyped calculi with mobility. Relevant references include flow analysis [DLB00,BDNN01], abstract interpretation [HJNN99], modal logics [CG00].

A complementary line of research on type systems focuses on the certification of bounds on resource consumption. Relevant references include the following ones: [Hof02,HJ03] introduce a notion of resource type representing an abstract unit of space, and uses a linear type system to guarantee linear space consumption; [CW00] enforces quantitative bounds on time usage using a typed assembly language; [IK02] puts forward a general formulation of resource usage analysis; more recently [CEI+05] proposes a new resource management paradigm that combines static and dynamic checks in a novel way. Briefly, the approach is based on the use of explicit language constructs to dynamically verify the availability of the required resources, and static analysis to verify that the dynamic checks enforce the resource intended bounds policies. In the context of distributed and concurrent calculi, relevant references include [GHS02], which presents a calculus in which resources may be moved across locations provided suitable space is available at the target location; [TZH02,BBDS03], which use typing systems to control resource usage and consumption; and [CGT02], which uses static techniques to analyze the behavior of finite control processes, i.e., those with bounded capabilities for ambient allocation and output creation.

Behavioral equivalences
Behavioral equivalences equate processes that "behave in the same way" in all contexts, that is, under all environments in which they could possibly be used. The behavior of processes is determined by how they interact with, or affect, such environments. In classical theories of concurrency (where processes are undistributed, untyped) the behavior is represented by the actions that the processes can perform, and formalized in the framework of Structural Operational Semantics. Thus processes are deemed equivalent if they can "perform the same actions".

Equivalence is particularly useful as a tool for justifying program transformations, ("we can validly replace P by Q because they have the same behavior in all contexts"), performed either by programmers during system development or by optimizing phases of compilers. Such transformations require equivalences relations to be congruences, i.e. preserved by all operators of the underlying calculi, a property that is also fundamental to perform compositional reasoning on complex systems.

Several notions of behavioral equivalence on processes have been defined (see for instance van Glabbeek's review [Gla93]). Among these, testing equivalence [DeHe84] and bisimulation equivalence [Pa81] have emerged as the most useful and stable. Beginning with work of Hennessy and Milner [HeMi85], they have been closely coupled with the use of various modal logics to characterize equivalent processes in terms of equi-satisfaction of modal process properties, and algebraic theories to transform finite-state equivalent processes by means of rewriting techniques. Another form of techniques developed for equivalence checking are operational techniques based on co-induction. This is especially important in the case of bisimulation, and includes strengthenings of the co-induction principle underlying bisimulation, called "up-to techniques" [Mil89,San98].

All of this is well-understood for the `classical' case of simple, CCS-like process calculi and, to some extent, for pure calculi of mobility like the pi-calculus (by pure we mean that there is mobility since names can be communicated, but there are no type and no
primitives for distribution). Even in the pi-calculus, however, tools for analysis have had a limited development compared to that for classical process calculi.
Theories of behavioral equivalences for calculi of code and agent mobility, with distributed locations and complex network topologies have received increasing but still limited attention in the recent literature. Initial work in this area [LS03,BCMS04] shows that mobility and distribution have deep impact on classical problems in the theory of concurrency, such as interference, with serious effects on the algebraic theory and algorithms for verification. Mobility also creates unexpected difficulties in modelling simple notions of bisimilarity, and in providing coinductive characterizations of contextual equivalences [GHS02,CZ02,MZ03]. Similar difficulties arise when types are employed to discipline behavior with forms of access control [PiSa00], and to control code mobility [HMR03, HRY03].
Behavioral equivalences for process calculi have also been studied in the approach known as "logical semantics" in which the elements of a calculus are interpreted as the set (filter) of the properties they satisfy. These properties are usually expressed as types, thus establishing a duality between a term of the calculus and its types (properties), which often represent approximate process behaviors. This idea has been investigated in several papers on the theory of process calculi. Filter models have been built for the pi-calculus [HH97, DDG99], Ambient Calculi [CD02,MZ04] and extensions of ambient calculi with objects [BdL03]; the equational theories of these models have been related to observational equivalences among processes. Relations between type systems underlying filter models and labelled transition systems exist as it is shown in [MZ04].

Specification logics
The work on logics for distributed systems has evolved along several directions in the recent literature. The ambient logic [CG00] is a modal logic, solidly based on the ambient calculus, that can talk about space as well as time. It has logical operators that can be used to make assertions about locations and their names, and express their properties. A related approach has been taken for KLAIM, with temporal logics employed to specify and verify dynamic properties of mobile agents running over a wide area network. Spatial/temporal logics are also useful for the analysis of open systems, where components can be dynamically connected to interact with network services. Of particular interest in this context is the novel approach to model dynamic open systems based on bigraphs [JM04], which are emerging as a generalisation of several process calculi.

Modal and temporal logics have been proved useful formalisms for specifying and verifying properties of concurrent and different tools have been developed to support such activities. Hennessy-Milner Logic, mu-calculus, CTL, CTL*, ACTL have proved to be useful tools for describing and establishing properties of concurrent systems described as process calculi. Following the work of Hennessy and Milner [HeMi85], various correspondences have been established in [BCG88], where two equivalences over Kripke structures (node-labeled transition systems) are related to two variants of CTL* and in [DV95] where CTL and HML are related to branching bisimulation.

The increasing use of wide area networks and pervasiveness of computing, together with the introduction of new programming paradigms and languages that model interactions among different (possibly mobile) actors have created revived interest in the study of new logics. For the new class of programs, like for concurrent formalisms, it is crucial to have tools for establishing deadlock freeness, liveness and correctness with respect to given specifications. However, for this new class of systems, it is also important to establish other properties such as resources allocation, access to resources and information disclosure. To this purpose, the use of temporal logics for specifying and verifying dynamic properties of mobile systems has been advocated and pursued. Properties are specified by means of temporal and spatial modalities and then verified, either proof-theoretically, or with the aid of model checkers. In the proof system approach, inference rules are provided in order to build proofs that establish the satisfaction of formulae by systems. In the model checking approach, a methodology is introduced to verify automatically whether a system belongs to the to the formal model of a formula.

Logics for process calculi with mobility have been studied in various papers. Below we briefly outline the references to the literature that are relevant to our present purposes.

[MPW93] introduces a modal logic for the pi-calculus. This logic aims at capturing different equivalences between processes and at establishing the differences between late and early bisimulation. It is based on Hennessy-Milner Logic (HML) but it has no operators for recursion. In [D96] a HML-like logic with recursion for pi-calculus is presented. This logic is equipped with a tableau-based proof system but has no operator for dealing with spatial properties and agent mobility.

[CG00] presents a modal logic for Mobile Ambients. It is a modal logic, solidly based on the Ambient calculus, that can talk about space as well as time. It has logical operators that can be used to make assertions about locations and their names, and can express also rather intensional properties [San01]. The work on spatial logics for distributed systems has since then evolved in several directions. [CC01] introduces a variant of the Ambient logic, tailored for asynchronous pi-calculus. This very interesting logic is equipped with operators for spatial and temporal properties, and for compositional specification of systems properties. In [CG01], new operators for expressing logical properties of name restrictions have been added. This logic supports the specification of spatial configurations and of a variety of properties of mobile computation, including security properties.

[DL04] develops a temporal logic for specifying properties of Klaim [DFP98]. The logic is inspired by Hennessy-Milner Logic and the mu-calculus, but has novel features that capture state properties and the impact of actions and movements over the different sites. The logic is equipped with a complete proof system that enables one to prove properties of mobile systems.

Temporal logics have also been studied in connection with the automaton-theoretic approach to concurrent system based on verification by model checking. History Dependent (HD) automata, which are able to allocate and deallocate names dynamically, have been introduced and proved effective for the verification of (finite fragments of) calculi with causality, locality and mobility [FGMP04].

[CMS05] proposes a spatial logic built on bigraphs. As it is equipped with a contextual operator, the logic can characterise both closed systems (processes) and open systems (contexts). It can describe also the composition of contexts and the separation of resources. Thanks to the generality of bigraphs, such a logic aims at embedding and contextualising the spatial logics proposed up to now. <<<