1,722,415 research outputs found
On the Modeling of Bell-LaPadula Security Policies using RBAC
No full textThe Bell-LaPadula security model is a hybrid model that combines mandatory access controls and discretionary access controls. The Bell-LaPadula security model has been widely accepted in military environments for its capability to specify military style confidentiality policies. The role based access control (RBAC) model has attracted extensive research effort and has been acknowledged as a flexible and policy natural model. This paper investigates a way of modeling Bell-LaPadula security policies using the RBAC model. The capability of modeling Bell-LaPadula security policies using RBAC model means that applications that are implemented using the RBAC model can then be deployed in military environments and will meet their requirements for information confidentiality
Using formal methods to develop WS-BPEL applications
No full textIn recent years, WS-BPEL has become a de facto standard language for orchestration of Web Services. However, there are still some well-known difficulties that make programming
in WS-BPEL a tricky task. In this paper, we firstly point out major loose points of the WS-BPEL specification by means of many examples, some of which are also exploited
to test and compare the behaviour of three of the most known freely available WS-BPEL engines. We show that, as a matter of fact, these engines implement different
semantics, which undermines portability of WS-BPEL programs over different platforms. Then we introduce Blite, a prototypical orchestration language equipped with a formal
operational semantics, which is closely inspired by, but simpler than, WS-BPEL. Indeed, Blite is designed around some of WS-BPEL distinctive features like partner links, process termination, message correlation, long-running business transactions and compensation handlers. Finally, we present BliteC, a software tool supporting a rapid and easy development of WS-BPEL applications via translation of service orchestrations written in Blite into executable WS-BPEL programs. We illustrate our approach by means of a running example borrowed from the official specification of WS-BPEL
A Formal Account of WS-BPEL
No full textWe introduce B lite, a lightweight language for web services orchestration designed around some of WS-BPEL peculiar features like partner links, process termination, message correlation, long-running business transactions and compensation handlers. B lite formal presentation helps clarifying some ambiguous aspects of the WS-BPEL specification, which have led to engines implementing different semantics and, thus, have undermined portability of WS-BPEL programs over different platforms. We illustrate the main features of B lite by means of many examples, some of which are also exploited to test and compare the behaviour of three of the most known free WS-BPEL engines
Specification and analysis of SOC systems using COWS: a finance case study
No full textService-oriented computing, an emerging paradigm for distributed computing based on the use of services, is calling for the development of tools and techniques to build safe and trustworthy systems, and to analyse their behaviour. Therefore many researchers have proposed to use process calculi, a cornerstone of current foundational research on specification and analysis of concurrent and distributed systems.
We illustrate this approach by focussing on COWS, a process calculus expressly designed for specifying and combining services, while modelling their dynamic behaviour. We present the calculus and one of the analysis techniques it enables, that is based on the temporal logic SocL and the associated model checker CMC. We demonstrate applicability of our tools by means of a large case study, from the financial domain, which is first specified in COWS, and then analysed by using SocL to express many significant properties and CMC to verify them
Regulating Data Exchange in Service Oriented Applications
No full textWe define a type system for COWS, a formalism for specifying and combining services, while modelling their dynamic behaviour. Our types permit to express policies constraining data exchanges in terms of sets of service partner names attachable to each single datum. Service programmers explicitly write only the annotations necessary to specify the wanted policies for communicable data, while a type inference system (statically) derives the minimal additional annotations that ensure consistency of services initial configuration. Then, the language dynamic semantics only performs very simple checks to authorize or block communication. We prove that the type system and the operational semantics are sound. As a consequence, we have the following data protection property: services always comply with the policies regulating the exchange of data among interacting services. We illustrate our approach through a simplified but realistic scenario for a service-based electronic marketplace
Service discovery and negotiation with COWS
No full textTo provide formal foundations to current (web) services technologies, we put forward using COWS, a process calculus for specifying, combining and analysing services, as a uniform formalism for modelling all the relevant phases of the life cycle of service-oriented applications, such as publication, discovery, negotiation, deployment and execution. In this paper, we show that constraints and operations on them can be smoothly incorporated in COWS, and propose a disciplined way to model multisets of constraints and to manipulate them through appropriate interaction protocols. Therefore, we demonstrate that also QoS requirement specifications and SLA achievements, and the phases of dynamic service discovery and negotiation can be comfortably modelled in COWS. We illustrate our approach through a scenario for a service-based web hosting provider
Introduzione. Un percorso di ricerca per i sarcofagi di Atella e di Rapolla
No full textI sarcofagi rinvenuti ad Atella e a Rapolla documentano la ricchezza e l’immaginario raffinato dei proprietari terrieri che, in età imperiale romana, dominavano la campagna del Vulture. Il racconto di un paesaggio millenario, naturale e umano, si dipana tra iconografia, studio dei materiali e storia collezionistica, seguendo i percorsi antichi e moderni dei due ‘capolavori in rilievo’
Automated Proof of Bell–LaPadula Security Properties
No full textAlmost 50 years ago, D. E. Bell and L. LaPadula published the first formal model of a secure system, known today as the Bell–LaPadula (BLP) model. BLP is described as a state machine by means of first-order logic and set theory. The authors also formalize two state invariants known as security condition and *-property. Bell and LaPadula prove that all the state transitions preserve these invariants. In this paper we present a fully automated proof of the security condition and the *-property for all the model operations. The model and the proofs are coded in the { log} tool. As far as we know this is the first time such proofs are automated. Besides, we show that the { log} model is also an executable prototype. Therefore we are providing an automatically verified executable prototype of BLP
A Calculus for Orchestration of Web Services
No full textWe introduce COWS (Calculus for Orchestration of Web Services), a new foundational language for SOC whose design has been influenced by WS-BPEL, the de facto standard language for orchestration of web services. COWS combines in an original way a number of ingredients borrowed from well-known process calculi, e.g. asynchronous communication, polyadic synchronization, pattern matching, protection, delimited receiving and killing activities, while resulting different from any of them. Several examples illustrates COWS peculiarities and show its expressiveness both for modelling imperative and orchestration constructs, e.g. web services, flow graphs, fault and compensation handlers, and for encoding other process and orchestration languages
- …
