Smart contracts, which are self-executing agreements, have a huge range of possible uses from finance to supply chain management. To avoid costly errors and vulnerabilities, it is crucial to guarantee the accuracy and reliability of these contracts. This paper explores the convergence of Blockchain technology, particularly Ethereum’s smart contracts, and Business Process Modeling (BPM), capitalizing on the synergies between these domains. We propose that viewing smart contracts as akin to business processes can significantly enhance the verification of Blockchain-based applications, addressing critical challenges in smart contract correctness and security. In this work we employ a formal verification approach based on Coloured Petri Nets and Linear Temporal Logic to detect potential vulnerabilities in Solidity smart contracts while considering their behavioral context as a business process model.

Opacity is a security property that guarantees the confidentiality of secret information from a partial observer of the system. To address this problem, we propose a modular approach that uses Supervisory and Control Theory to design a global supervisor for Modular Discrete Event Systems (MDES). This approach assumes the attacker can observe the shared alphabet between modules, and takes into account the modular structure of the system; which significantly decreases computational complexity compared to monolithic methods. To achieve this, we introduce a reduced-complexity algorithm, based on the Hyper Symbolic Observation Graph. The HSOG is an abstraction graph that considers only events that have a direct impact on the opacity. This reduces the number of states to be considered, making the algorithm more efficient.

Discrete Event systems are dynamic systems with two main characteristics: their set of states is discrete and their dynamic is event driven (as opposed to time driven). In this paper, we study a security property for DES called opacity. A system$\mathcal{T}$, partially observed by a third party -called an attacker- is said to be opaque if the attacker can never conclude from its provided interface that$\mathcal{T}$is in a secret state. Given a critical system that may leak confidential information, an attacker and a subset of controllable actions, we propose an approach to synthesize a controller that enforces the system's opacity. This controller is designed as a function that applies, at run time, on the current executions to disable any controllable action that eventually leads to the violation of the system's opacity. Our approach is based on a novel graph called a Hyper Symbolic Observation Graph. The language obtained under control is proven to be maximal whatever is the relationship between the attacker and the controller observations.

While Blockchains can open intriguing opportunities of research in many application contexts, they come with the risk of bringing new unconventional problems. In fact, because of the monetary value they hold, Blockchains have been subject to many attacks. Smart contracts, which are at the core of second-generation Blockchains, have been proven to be the origin of such attacks due to the exploitable vulnerabilities their code may hold. It is therefore an essential requirement to prove the correctness of the smart contracts to be deployed on a Blockchain to ensure its protection. The existing approaches have been focusing on targeting generic vulnerabilities like reentrancy, without offering the possibility to check temporal-based contract-specific properties. In this paper, we aim to address smart contracts verification while supporting such properties. We propose and implement a transformation of Solidity smart contracts into Coloured Petri nets and investigate the capability of existing model checking tools to check specific temporal properties of the formally modeled contract.

A system is opaque w.r.t. a secret and an observation map if for every run that leads to the secret, there exists at least one equivalent run which does not. The dichotomy of this definition, however, fails to measure just how much information the system keeps hidden. In fact, a system can be deemed opaque due to a single non-secret run, among an overwhelming number of secret equivalents. In this paper, we wish to redeem this drawback by the means of quantifying opacity into an opacity degree measuring the security of a system. After we formalize this numeral value for both the system and its corresponding Symbolic Observation Graph (SOG), we enhance our findings using a case study and some experimentation.

Opacity is a formal security property that formulates the abilities of a passive observer to infer secret information. Usual opacity studies focus on affirming that a system is either opaque or non-opaque w.r.t. the secret and an observation map. This view, however, fails to reflect that a system may be opaque because of a single non-secret execution among an overwhelming number of secret ones. For this reason, we propose, in this work, to quantify the opacity of a Web service (WS) into a numeral value that measures its security. Our approach consists in defining an opacity degree for the system and its Symbolic Observation Graph (SOG) abstraction. Furthermore, and to ensure its efficiency, we conduct an experimental study.

Processes, whatever the field (e.g. software, military or healthcare), are everywhere. They represent the building block of any information system nowadays. Business processes are used to represent the enterprise’s business and services it delivers. They are also used as a mean to enforce customer’s satisfaction and to create an added value to the company. Software processes are critical as well since they represent the guaranty to respect development process’s deadlines and to ensure a certain quality of the delivered software, which in some cases will end up being the company’s information system itself. It is then more than critical to seriously consider the design of such processes and to make sure that they are free of any kind of inconsistencies. One possible way to unsure that the developed processes are safe is to apply formal verification. Hence, we propose this workshop to investigate the novelties and advances concerning the application of formal methods in Business/Software (BS) processes design and execution.

This report gives a brief overview of the main concerns addressed by the authors at the fifth international track on Formal Verification of Service Based Systems, held at WETICE 2017 conference. A presentation of the main topics is given and then a summary of the paper accepted by this conference track is reported.

Web service (WS) providers need to restrain access to private information when cooperating with business partners. This need is translated in practice by an abstraction phase where inner data is withheld from public view. However, just like hiding encryption keys is not enough to prove the secrecy of information in a communication protocol, this procedure cannot prove the goal of secrecy is attained. Security related literature has turned in the past couple of decades to a new, formal, security property, i.e., opacity, to both hide and prove the privacy of secrets. Following our previous work on the use of the Symbolic Observation Graph (SOG), on one hand, to abstract and compose Web services, and to verify the opacity of systems on the other, we show in this paper how the verification of three different types of opacity in SOG-abstracted WSs is translated to the opacity of their composites. We hence establish that the SOG is a suitable abstraction that allows to check these opacity variants locally to each component of a composite WS, and preserves opacity by composition (i.e., each WS component is opaque iff the composite WS is).

Composition of Cloud services is necessary when a single component is unable to satisfy all the user's requirements. It is a complex task for Cloud managers which involves several operations such as discovery, compatibility checking, selection, and deployment. Similarly to a non Cloud environment, the service composition raises the need for design-time approaches to check the correct interaction between the different components of a composite service. However, for Cloud-based service composition, new specific constraints, such as resources management, elasticity and multitenancy have to be considered. In this work, we use Symbolic Observation Graphs (SOG) in order to abstract Cloud services and to check the correction of their composition with respect to event-and state-based LTL formulae. The violation of such formulae can come either from the stakeholders' interaction or from the shared Cloud resources perspectives. In the former case, the involved services are considered as incompatible while, in the latter case, the problem can be solved by deploying additional resources. The approach we propose in this paper allows then to check whether the resource provider service is able, at run time, to satisfy the users' requests in terms of Cloud resources.

Composition of Cloud services is necessary when a single component is unable to satisfy all the user's requirements. It is a complex task for Cloud managers which involves several operations such as discovery, compatibility checking, selection, and deployment. Similarly to a non Cloud environment, the service composition raises the need for design-time approaches to check the correct interaction between the different components of a composite service. However, for Cloud-based service composition, new specific constraints, such as resources management, elasticity and multi-tenancy have to be considered. In this work, we use Symbolic Observation Graphs (SOG) in order to abstract Cloud services and to check the correction of their composition with respect to event-and state-based LTL formulae (Hybrid LTL). The violation of such formulae can come either from the stakeholders' interaction or from the shared Cloud resources perspectives. In the former case, the involved services are considered as incompatible while, in the latter case, the problem can be solved by deploying additional resources. Using our approach, one can check then, if the resource provider service can supply sufficient Cloud resources w. r. t. the users' requests.

This report gives a brief overview of the main concerns addressed by the authors at the fourth international track on Formal Verification of Service Based Systems, held at WETICE 2016 conference. A presentation of the main topics is given and then a summary of the paper accepted by this conference track is reported.

Automatic composition of Web services requires that the providers publish an abstract version of their Web services to a registry. They offer this abstraction instead of the complete web service to ensure the privacy of their internal know-how and trade secrets. Many studies have offered methods to do this, but none of them is able to formally prove their ability to keep the secret information hidden. In this article we turn to the verification of opacity, a formal security property that allows not only to preserve the secret but also to formally prove that it remains hidden. In particular, we investigate if the composition of two opaque Web services is also opaque. Our work consists in verifying the opacity of the composition of two Web services through the verification of the opacity of their individual abstractions represented by Symbolic Observation Graphs.

In this paper, we propose a bottom-up approach to check the correct interaction between workflows distributed over a number of organizations. The whole system's model being unavailable, an up-down analysis approach is not appropriate. We consider two correctness criteria of inter-organizational work-flows communicating asynchronously and sharing resources: a generic one expressed with the soundness property, and a specific one expressed with any temporal property expressed with the LTL logic. Each part of the whole organization exposes its abstract model, represented by a Symbolic Observation Graph (SOG), to allow the collaboration with possible partners. The SOG is then revisited and adapted in order to reduce the verification of the entire composite model to the verification of the composition of the SOG-based abstractions. We illustrate our approach with a case study and give preliminary results of our implemented prototype.

This report gives a brief overview of the main concerns addressed by the authors at the third international track on Formal Verification of Service Based Systems, held at WETICE 2015 conference. A presentation of the main topics is given and then a summary of the paper accepted by this conference track is reported.

This report gives a brief overview of the main concerns addressed by the authors at the second international track on Formal Verification of Service Based Systems, held at WETICE 2014 conference. A presentation of the main topics is given and then a summary of the paper accepted by this conference track is reported.

Opacity is an important security property dealing with the hiding and keeping secret, a subset of a system's behaviour from external observers. A system is characterised as "opaque" if it can effectively hide specific actions from an intruder or attacker. As the need for opacity, and similar fundamental secrecy properties may arise in a wide range of applications and sectors, like health care, banking, trading and voting systems, ... etc., providing efficient tools for its verification becomes important, especially for large-scale real-world systems. In this paper, we formulate opacity, based on labeled transition systems models, and provide an efficient verification algorithm within the framework of a hybrid on-the-fly approach. Our verification strategy is based on the construction of a symbolic observation graph, allowing for the abstraction of the system's behaviour, while preserving the necessary structure needed for the checking of the opacity property dealt with in this paper. The preliminary implementation of our algorithm and the provided experimental results are promising, and demonstrate its effectiveness in face of the exponential state explosion problem, compared with existing techniques.

Cloud environments are being increasingly used for the deployment and execution of service-based business processes (SBPs). Among other properties, cloud provides elasticity in order to guarantee provisioning of necessary resources that ensure a smooth functioning of cloud services despite changes in solicitations. Provisioning of elastic infrastructures and platforms is not sufficient to provide elasticity of the deployed SBP. Therefore, SBPs should be provided with elasticity mechanisms to ensure their adaptation to the workload changes. In this paper, we propose a formal model, using timed Petri nets, for SBPs elasticity considering temporal constraints and an approach for time-based evaluation of SBPs elasticity strategies.

For automatically composing Web services in a correct manner, information about their behaviors (an abstract model) has to be published in a repository. This abstract model must be sufficient to decide whether two, or more, services are compatible (the composition is possible) is possible without including any additional information that can be used to disclose the privacy of these services. The compatibility property is defined by different variants of the well known soundness property on open workflow nets. These properties guarantee the absence of livelocks, deadlocks and other anomalies that can be formulated without domain knowledge. In this paper we address the automatic abstraction of Web services and the checking of their compatibility using their abstract models only. To abstract Web services, we use the symbolic observation graph (SOG) approach that preserves necessary information for service composition and hides private information. We show how the SOG can be adapted and used so that the verification of different variants of compatibility can be performed on the composition of the abstract models (SOGs) of Web services instead of the original composite service.

Time Petri nets (TPN model) allow the specification of real-time systems involving explicit timing constraints. The main challenge of the analysis of such systems is to construct, with few resources (time and space), a coarse abstraction preserving timed properties. In this paper, we propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behaviour of bounded TPNs with strong time semantics. The main feature of this abstract representation compared to existing approaches is the encoding of the time information. This is done in a pure way within each node of the TAG allowing to compute the minimum and maximum elapsed time in every path of the graph. The TAG preserves runs and reachable states of the corresponding TPN and allows for verification of both event- and state-based properties.

This work deals with services composition. We propose an approache based on Symbolic Observation Graphs (SOG) allowing to decide whether two (ore more) web services can cooperate safely. The compatibility between two web services is defined by the well known soundness property on open workflow nets and checked on the composition of SOGs instead of the original web services composition. This allows to respect the privacy of the services since SOGs are base on collaborative activities only and hide the internal structure and behavior of the corresponding service.

In a context of short-term cooperation, enterprises with complementary skills are dynamically interconnected according to their needs. To deal with requirements in a such cooperation, we present in this paper CoopFlow that aims at providing a useful artifact for preservation of the privacy of workflows partners, pre-established workflows and pre-established workflow management systems. CoopFlow consists of three steps: workflow abstraction and advertisement, workflow matching and interconnection, and workflow cooperation. To preserve the privacy of partners, the first step of the approach includes an abstraction procedure allowing a partial visibility of the partners' workflows. The second step consists of interconnecting existing workflows of partners with complementary skills attributing to a matching procedure that allows checking both behaviors and business semantics of partners' workflows. Finally, the last step of CoopFlow consists of controlling the inter-enterprise workflows cooperation allowing cooperation partners to integrate the existing workflows and to check whenever they can cooperate and change their partners, which frequently leads to support spontaneous, dynamic and short-term cooperation. With this intention, we developed a platform that manages inter-operability by integrating pre-established workflow management systems. The proof of concept is provided by integrating three heterogeneous and open workflow management systems to the CoopFlow platform.