|
|
|
COSoDIS FLACOS 2008 Second Workshop on Formal Languages and Analysis of Contract-Oriented Software Malta, November 27-28, 2008 University of Malta, Department of Computer Science Semantics and Verification Research Group  |
|
Invited Talks
Accepted Papers
Other Talks
Abstracts
Contracts in the Swedish Crisis Management System The talk will give a brief overview of my research project funded by the Swedish Emergency Management Agency. The Swedish Crisis Mangament System relies to a great extent on agreements both between governmental agencies and between agencies and private companies. These agreements deal both with resource allocation and distribution of responsibilities. The agreements are often made independently of each other, so a vital concern for the Swedish Crisis Management System is to be able to make sure that a set of such agreement form an adequate crisis response capability. The project formalises the agreements and try to find ways to decide whether an existing set of agreements form an adequate crisis respons capability. Service Contracts in a Secure Middleware for Embedded Peer-to-Peer Systems Antonio Brogi (joint work with. F. Benigni, S. Corfini, T. Fuentes) Peer-to-peer (P2P) systems are distributed computing systems where all network elements act both as service consumers (clients) and service providers. Most P2P communication mechanisms are not based on pre-existing infrastructures, but rather on dynamic ad-hoc networks among peers. Embedded Peer-to-Peer (EP2P) systems introduce new challenges in the development of software for distributed systems. The goal of the Secure Middleware for Embedded Peer-To-Peer Systems (SMEPP) European Project (www.smepp.org) is precisely to develop such a middleware, that will have to be secure, generic and highly customisable, allowing for its adaptation to different devices (from PDAs and smart phones to embedded sensor actuator systems) and to different domains (from critical systems to consumer entertainment or communication). One of the objectives of SMEPP is to feature a high-level, service-oriented model to program the interaction among peers, thus hiding low-level details that concern the supporting infrastructure. SMEPP services are associated with service contracts - which provide standard descriptions of SMEPP services - and with service groundings - which provide details on how to interoperate with services (i.e. communication protocols, message formats, port numbers, etc.). Service contracts are the key ingredients of the SMEPP mechanisms for service publication and discovery. In this paper, after briefly introducing the main features SMEPP model, we report on the structure of service contracts that has been defined in the SMEPP project. Runtime Verification of Deontic Contracts Christian Colombo (joint work with Gordon Pace, Stephen Fenech and Gerardo Schneider) With the advancement of service-oriented architecture (SOA), a lot of services are provided to customers, together with a contract between the customer and the service provider, regulating the transaction. To enable automatic verification of contracts, an adequate logic must be used to describe them formally. Contract Language (CL) is but one of the various logics suggested to represent contracts in a deontic style. Building upon recent work relating CL and automata, we present a framework for the runtime verification of contracts using LARVA, a real-time runtime verification system. A Tool for the Design and Verification of Composite Web Emilia Cambronero Piqueras This talk describes the main features of the Web Services Translation tool, WST for short, a tool for modeling and veri.cation of Web Services systems with time restrictions. The different parts of WST are then presented, and a case study is used to show the potential of this tool. This case study is called .Dynamic Internet Purchase Site. and it allows us to see the capabilities of modelling, code generation and verification of the tool. This case study is a Web Service system with time restrictions, which are one of the main objetives of the WST verification part. Treaty - A Modular Component Contract Language Jens Dietrich, Graham Jenson We introduce Treaty, a platform-independent component contract language. Treaty is expressive enough to define different types of constracts between components consuming and providing services and other resources, including contracts referring to interface interoperability, component semantics, and quality of service attributes. The contracts are based on a modular and extensible vocabulary, and precise enough to be used for runtime verification of component-based systems. We present a prototype based on OSGi/Eclipse that uses Treaty contracts. The contracts used in this example describe relationships between different resource types including Java types and XML documents. A modified version of JUnit that supports dependency injection is used to check semantic and quality of service contracts. Treaty contracts can be used to address the following workshop topics: reasoning about quality of service attributes (such as resource restrictions encountered in ubiquitous computing applications), making component assemblies more predictable (through verification), and the description of non-functional aspects. Conflict Analysis of Deontic Contracts Stephen Fenech (joint work with Gordon Pace and Gerardo Schneider Industry is currently pushing towards Service Oriented Architecture where code execution is not limited to the organisational borders but may extend outside of the organisation to which the sources are typically not accessible. In order to protect the interests of the organisation contracts are used which can be seen as a list of obligations, permissions and prohibitions. The composition of different services with different contracts, and the combination of service contracts with local contracts can give rise to conflicts, exposing the need for automatic techniques for contract analysis. In this paper we investigate how conflict analysis can be performed automatically for contracts specified in the contract language CL. Increasing Trust in Public Service Delivery - Contract-Based Software Infrastructure for Electronic Government Tomasz Janowski (joint work with Adegboyega Ojo) Citizens increasingly demand high-quality public services, available from a one-stop government portal, and delivered through a choice of electronic and traditional channels. In order to fulfill this demand, the implementation involves collaboration between agencies at different levels of government, driven by complex administrative and business processes. In addition, the delivery of public services increasingly involves private sector organizations serving as intermediaries or suppliers, able to flexibly join or leave dynamic service networks. Such networks have to be managed to address the expected stability of the services delivered through them. This paper presents a lightweight software infrastructure that enables collaborative delivery of public services through a managed set of services, components and frameworks. The infrastructure currently comprises five run-time and design-time elements: (1) Front Office Framework, (2) Back Office Framework, (3) Workflow Service, (4) Messaging Service, and (5) Infrastructure Management Service. With each element offering a pair of functional and management interfaces, the infrastructure allows the expression, instrumentation and verification of contracts. Contracts are expressed in an XML language defined by us, their instrumentation is implemented through the Web Services Distributed Management (WSDM) framework, and verification is carried out though a mediation service, part of Management Service. In addition to infrastructure-level contracts, we show how contracts can be formulated and verified at process and service levels where violation of infrastructure-level contracts may cause a chain of violations at process and service levels. Finally, we discuss how contract information can be use as part of organizational practices - IT Governance and specifically Service Management, to improve the delivery of public services in terms of availability and reliability. Cc-Pi: A Constraint-Based Language for Contracts with Service Level Agreements Ugo Montanari (joint work with Maria Grazia Buscemi) Service Level Agreements are a key issue in Service Oriented Computing. SLA contracts specify client requirements and service guarantees, with emphasis on Quality of Service (cost, performance, availability, etc.). In this work we propose a simple model of contracts for QoS and SLAs that also allows to study mechanisms for resource allocation and for joining different SLA requirements. Our language combines two basic programming paradigms: name-passing calculi and concurrent constraint programming (cc programming). Specifically, we extend cc programming by adding synchronous communication and by providing a treatment of names in terms of restriction and structural axioms closer to nominal calculi than to variables with existential quantification. In the resulting framework, SLA requirements are constraints that can be generated either by a single party or by the synchronisation of two agents. Moreover, restricting the scope of names allows for local stores of constraints, which may become global as a consequence of synchronisations. Our approach relies on a system of named constraints that equip classical constraints with a suitable algebraic structure providing a richer mechanism of constraint combination. The cc-pi calculus has been equipped with both a reduction and an abstract semantics in the style of open pi calculus. A symbolic transition system with contextual labels has also been defined. A reduction-preserving translation of cc programming and a translation of the fusion calculus by Gardner and Wischik which respects open bisimilarity have been provided. Besides small examples, cc-pi has been applied to a Telco case study. The model allows to specify, negotiate, and enforce policies in complex scenarios where policy negotiations and validations can be arbitrarily nested. Towards verifying contract regulated service composition Alessio Lomuscio (joint work with Hongyang Qu and Monika Solanki) We report on an approach to (semi-)automatically compile and verify contract-regulated service compositions. We specify web services and the contracts governing them as WSBPEL behaviours. We compile WSBPEL behaviours into the specialised system description language ISPL, to be used with the model checker MCMAS to verify behaviours automatically. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivat- ing example whose state space is approximately 10^6 and discuss experimental results. Security-By-Contract for the Future Internet? Fabio Massacci With the advent of the next generation java servlet on the smartcard, the Future Internet will be composed by web servers and clients silently yet busily running on high end smart cards in our phones and our wallets. In this brave new world we can no longer accept the current security model where programs can be downloaded on our machines just because they are vaguely "trusted". We want to know what they do in more precise details. We claim that the Future Internet needs the notion of security-by-contract: In a nutshell, a contract describes the security relevant interactions that the smart internet application could have with the smart devices hosting them. Compliance with contracts should veri.ed at development time, checked at depolyment time and contracts should be accepted by the platform before deployment and possibly their enforcement guaranteed, for instance by in-line monitoring. In this paper we describe the challenges that must be met in order to develop a security-by-contract framework for the Future Internet and how security research can be changed by it. Joseph Okika There are numerous existing notations and standards in the Web service community. These may be grouped broadly into three competing families, namely; Web Services, Semantic Web, and Electronic Business. Although the families are competing, we expect that the applications will cut across them and there is a need to map from one to another and to analyze compatibility and other properties. Therefore we survey how they deal with different aspects using Mealy machines to give meaning to the aspects. We then illustrate with examples, the aspects of contracts captured by one language from each of the three competing families in addition to WSDL, the core standard for Web services description. The result is a taxonomy based on the aspects of computations: functionality, protocol, and for instance performance covered by the languages. The taxonomy is used to identify similarities between semantic models and thus find potential mappings between the families. Furthermore, this gives a handle on analysis techniques that may apply to the aspects in a particular family. Based Verification of Hierarchical Systems of Components Sophie Quinton, Susanne Graf In earlier work, we have introduced a framework for contract-based reasoning parametrized, among others, by a notion of behaviors along with a semantics of composition of such behaviors. Our aim is to separate clearly between properties of contracts that are specific to a given framework and properties that apply to a whole class of contract-based verification frameworks. In particular, we think that soundness of (apparently) circular reasoning is a generic property that is essential when dealing with contracts. To support our claim, we provide two instantiations of our framework. We show that important results presented in earlier work are direct consequences of circular reasoning. Proofs are thus shorter and, we believe, clearer. We also believe that such a methodology improves understanding of concepts. As an example, if circular reasoning is not sound in a particular framework, there are two possibilities: either not use it, or find another definition of refinement in a concept such that in the modified framework circular reasoning is sound. Contract-Oriented Software Development for Internet Services - where are we now? Anders P. Ravn The presentation gives an overview of the initial goals of the CoSiDIS project and continues with an assessment of where we have made good progress and where we may lack progress. For the latter, more interesting cases, I discuss, whether the goals were wrong, unrealistic or whether they are still valid and thus attainable. Service Oriented Architectures: The New Software Paradigm Wolfgang Reisig Recent voices from industrial labs praise Service Oriented Architectures (SOA) as: "THE most relevant emerging paradigm", "a substantial change of view, as it happens at most once each decade", "the next fundamental software revolution after OO" or "much more than just another type of software". All SOA have evolved along applications. Though conceived as a widely applicable principle, SOA has so far not been equipped with a decent formal, abstract basis. In this talk we outline first ideas for a theoretical basis of SOA. Fundamental questions address the semantics of a service, equivalence of services, substitutability of services (also during runtime), etc. A fundamental construction in the area is the operating guideline of a service S, finitely characterizing the set of all partners (successful users) of S. A lot of questions on a service can be answered by means of its operating guideline. Specification and analysis of electronic contracts in CL Gerardo Schneider (joint work with Cristian Prisacariu and Gordon Pace) In this talk I will describe CL, a language for writing (electronic) contracts with semantics in an extension of the mu-calculus. The language allows to write (conditional) obligations, permissions and prohibitions, and to represent the so-called contrary-to-duty (CTD) and contrary-to-prohibition (CTP). CTDs and CTPs are useful to establish what happens in case an obligation, respectively a prohibition, is not respected. The approach is action-based, meaning that the above normative notions are defined on actions and not on state-of-affairs. I will then sketch some initial work on model checking contracts. Permission to Speak: An Access Control Logic Oleg Sokolsky (joint work with Nikhil Dinesh, Aravind Joshi and Insup Lee) The modality of saying is central to access control logics. In this paper, we investigate the interaction of saying with the deontic modalities of obligation and permission. The motivation is to provide a unified formalism for phenomena that have been studied separately in the literature -- (a) representation in access control, e.g., delegation and speaking for, (b) positive and negative permissions, and (c) conformance in the presence of iterated deontic modalities, e.g., "required to forbid". The central idea is to use statements that permit or require other statements. We propose two axiom schemas that transfer permissions and obligations from one set of laws to another. Policies are expressed in a non-monotonic formalism that accomodates reasoning about the transfer of permissions. CREOL as a Framework for Service-Oriented Architectures Martin Steffen, Olaf Owe CREOL is an executable, object-oriented language for modelling, prototyping and formal analysis of distributed active objects. Objects are concurrent, each with its own virtual processor and internal process control. Active behavior is interleaved with passive behavior by means of processor release points. Communication is based asynchronous method calls. By releasing the processor while waiting for a method reply, non-blocking method calls are possible. The language is strongly typed and class variables are typed by interfaces, which may contain constraints on the communication patterns. The notion of cointerface allows for type correct callbacks. The language is imperative with multiple inheritance, late binding, and dynamic class upgrades. It is developed with respect to ease of verification and has a compositional proof system. The language has a formal semantics with an operational semantics defined in rewriting logic, giving rise to an executable interpreter in Maude. Recent extensions of the language has added notions of component, futures, and acquisition of components and objects references with a specified interface, in an (unknown) environment. The talk will discuss the CREOL framework as a basis for service-oriented software, and suggest possible extensions of the interface concept to support contract specifications. A Contract-Oriented View on Threat Modelling Ketil Stølen We propose a modular approach to the modelling and analysis of threat scenarios with mutual dependencies. Our approach may be used to deduce threat scenarios for a composite service from threat scenarios of its constituent services. It may also be used to decompose the analysis of a complex services into separate parts that can be carried out independently. A custom made paradigm to describe threat scenarios with external dependencies is put forward. We also define a set of deduction rules facilitating various kinds of reasoning, including the analysis of mutual dependencies between threat scenarios. Integrating Contract-based Security Monitors in the Software Development Life Cycle Alexander M. Hoole, Isabelle Simplot-Ryl , Issa Traore Software systems, containing security vulnerabilities, continue to be created and released to consumers. We need to adopt improved software engineering practices to reduce the security vulnerabilities in modern systems. These practices should begin with stated security policies and end with systems which are quantitatively, not just qualitatively, more secure. Currently, contracts have been proposed for reliability and formal verification; yet, their use in security is limited. In this work, we propose a contract-based security assertion monitoring framework (CB_SAMF) that is intended to reduce the number of security vulnerabilities that are exploitable, spanning multiple software layers, to be used in an enhanced systems development life cycle (SDLC). An Aspect-Oriented Behavioral Interface Specification Language Takuo Watanabe, Kiyoshi Yamada We have designed and developed a behavioral interface specification language Moxa. that provides a modularization mechanism for contracts based on assertions. The mechanism, called assertion aspect, can capture the crosscutting properties among assertions. In this paper, we briefly explain the notion of assertion aspects and the design of Moxa. By comparing the specification to its JML counterpart, we show that the use of assertion aspects clarifies the large, complex specification and greatly simplifies each assertion in the specification. |