In this paper we study how to fulfill proof of violation (POV) for availability of IaaS systems in the cloud. A POV scheme enables a user or a service provider to produce a precise proof of either the occurrence of the violation of properties or the innocence of the service provider. POV schemes are solutions for obtaining mutual nonrepudiation between users and the service provider in the cloud. To the best of our knowledge, it is the first scheme that can perform availability auditing according to cryptographic proofs. Experimental results are presented that demonstrate the feasibility of the proposed scheme. Service providers can use the proposed scheme to provide a mutual nonrepudiation guarantee for availability in their service-level agreements.

In this paper we study how to develop an efficient real-time auditing and proof of violation (POV) scheme for cloud storage systems. A POV scheme enables a user or a service provider to produce cryptographic proofs which can be used to prove either the occurrence of the violation of properties or the innocence of the service provider. POV schemes are solutions for obtaining mutual nonrepudiation between users and the service provider in the cloud. After each file operation, a real-time auditing should be performed so that the violation of the service provider can be found instantly. Existing solutions need to cache the hash values of files in client devices and thus the overhead for storing and synchronizing hash values in client devices which share files is huge. We propose a novel scheme in which client devices do not need to cache any hash values of files. A small portion called slice of a binary hash tree is transferred to the client device for real-time auditing and it can support POV whenever the audit does not pass. Experimental results are presented that demonstrate the feasibility of the proposed scheme and show that our scheme outperforms previous work by one to two order of magnitude. Service providers of cloud storage can use the proposed scheme to provide a mutual nonrepudiation guarantee in their service-level agreements.

A cloud database is a system that typically runs on a cloud computing platform which is not maintained by the user but a service provider. The service provider can leak confidential data, modify the data, or return inconsistent data to users due to bugs, crashes, operator errors, or even malicious security attacks. Some cloud database systems provide Web interface or application programming interface for clients to access logs of database transactions. However, these logs are not cryptographic proofs. Clients cannot use these logs to prove whether a cloud service provider has violated some required properties such as data integrity, write serializability, and read freshness. A proof of violation (POV) scheme enables a client or a service provider to produce a precise proof of either the occurrence of the violation of properties or the innocence of the service provider. In this paper, we develop POV schemes for cloud database systems. First, we show that previously proposed cryptographic accountability protocols (CAPs), cannot be applied to cloud database systems directly. A CAP defines a multi-step handshaking protocol for clients and the service provider to exchange signed messages during service request and response so as to generate cryptographic proofs for later auditing. In addition, previously proposed auditing schemes are inappropriate to obtain the auditing requirements of SQL database according to collected cryptographic proofs. We design a new auditing scheme for cloud database systems. Implementation and experimental results are presented that demonstrate the feasibility of the proposed schemes. Service providers can use the proposed schemes to provide a mutual nonrepudiation guarantee for database transactions in their service-level agreements.

Summary In this paper, we propose solution for obtaining mutual nonrepudiation between the user and service provider in cloud storage. One of the solutions for mutual nonrepudiation is based on logging attestations, which are signed messages. For supporting write‐serializability and read freshness of files, an intuitive solution is to have attestations be chain hashed. However, it is inefficient when files in an account can be accessed by multiple client devices interchangeably because client devices must keep all the attestations or there must exist a way to broadcast the last attestation to all the client devices. We propose a scheme that can guarantee mutual nonrepudiation between the user and service provider without requiring the client devices to exchange any messages, and each client device only has to store the last attestation it received. Concurrent accesses of files should be forbidden if all attestations need to be chained together with one chain. We propose to use multiple chains to provide concurrent file accesses in a single account. In addition, we also propose how to apply the hash tree to remove accumulated attestations. The results from related experiments demonstrate the feasibility of the proposed scheme. A service provider of cloud storage can use the proposed scheme to provide a mutual nonrepudiation guarantee in their service‐level agreement. Copyright © 2014 John Wiley & Sons, Ltd.

In this paper we define and explore proof of violation (POV) for cloud storage systems. A POV scheme enables a user or a service provider to produce a precise proof of either the occurrence of the violation of properties or the innocence of the service provider. POV schemes are solutions for obtaining mutual nonrepudiation between users and the service provider in the cloud. Existing solutions for obtaining mutual nonrepudiation only support epoch-based POV. The drawback of an epoch-based POV scheme is that violation of properties can only be detected at the end of an epoch. We propose a real-time POV scheme in which the auditing can be performed at the time of each file operation. To the best of our knowledge, it is the first scheme that can perform real-time POV for cloud storage. In addition, each client device only needs to store a partial hash tree of files in an account. Experimental results are presented that demonstrate the feasibility of the proposed scheme. Service providers of cloud storage can use the proposed scheme to provide a mutual nonrepudiation guarantee in their service-level agreements.

SUMMARY In this paper, we present a new framework for performing dynamic testing of semaphore‐based and shared‐memory concurrent programs. The proposed scheme only has to analyse the synchronization sequences (SYN‐sequences) that are collected during the dynamic testing of the concurrent program – static analysis of the syntax and semantics of the target concurrent program is unnecessary. A model checker is not needed to explore the feasible interleavings of the execution of the concurrent program. If the number of feasible SYN‐sequences of the tested concurrent program is finite, our scheme can perform dynamic testing of all the feasible SYN‐sequences. If the tested concurrent program has an infinite number of SYN‐sequences, state‐cover testing of the target program can be performed (if the execution states of the target concurrent program are finite). The implementation and experimental results obtained with real codes and some benchmark programs demonstrate the feasibility of the proposed scheme. Copyright © 2014 John Wiley & Sons, Ltd.

For efficient execution of long-running autonomous transactions, the isolation property is commonly relaxed. Previous works on relaxing the isolation property of transactions proposed deriving the conflict relation between each pair of autonomous transactions. In this paper we show that the pair wise conflict relation is not sufficient in the general cases and propose a solution for implementing concurrency control dynamically according to the global context of all of the autonomous transactions in the system. We employed defeasible logic as a definition tool to describe the concurrency control requirement and used a query-answering defeasible logic system to implement a concurrency control system.

In this paper we propose a novel workflow definition language—called the CLWfDL (Cloud Collaboration Workflow Definition Language)—for defining workflow in the working model of cloud collaboration. The language enables the distributed definition and concurrent revision of a workflow by multiple user

In this paper we propose a scheme for reachability testing to obtain statement coverage in the dynamic testing of concurrent programs. The proposed scheme derives inputs from SYN-sequences obtained in reachability testing and uses these inputs to perform reachability testing multiple times in order to achieve statement-coverage testing for a concurrent program.

The Chinese wall security model (CWSM) was designed to provide access controls that mitigate conflict of interest in commercial organizations, and is especially important for large-scale interenterprise workflow applications. This paper describes how to implement the CWSM in a WfMS. We first demonstrate situations in which the role-based access control model is not sufficient for this, and we then propose a security policy language to solve this problem, also providing support for the intrinsic dynamic access control mechanism defined in the CWSM (i.e., the dynamic binding of subjects and elements in the company data set). This language can also specify several requirements of the dynamic security policy that arise when applying the CWSM in WfMSs. Finally we discuss how to implement a run-time system to implement CWSM policies specified by this language in a WfMS.

This paper addresses the issue of how to support cloud computing in thin-client/server computing model. We describe the design and implementation of the multiple-application-server thin-client/server computing (MAS TC/S) model that allows users with thin-client devices to roam around a wide area network whilst experiencing transparent working environments. MAS TC/S can be applied to a wide variety of applications in wide area network, such as pervasive software rental, service-oriented infrastructure for an Internet service provider, and office automation for transnational corporations. The MAS TC/S architecture model comprises five major components: the display protocol, the multiple-application-server topology, the application-server discovery protocol, the distributed file system, and the network input/output protocol. We discuss problems and present solutions in the design of each constituent component. A prototype of the MAS TC/S that spans the campuses of two universities in Taiwan has been built - we also report our experiences in constructing this prototype.

We propose a framework for the automatic dynamic testing of workflow management systems (WfMSs). We first classify faults that can occur during the execution of a WfMS and then describe a systematic testing scheme that provides the following advantages. First, the system developer does not need to play the roles of participants, and hence the entire testing process can be automated. Second, resources that cannot be addressed or represented by the workflow engine can be simulated, which makes the proposed framework also a simulation environment for applications. Third, our platform solves the problems caused by the presence of nondeterministic behavior during dynamic testing of a WfMS. Finally, we describe how to apply temporal logic to verify the dynamic behavior of the tested WfMS. The implementation and experimental results demonstrate the feasibility of the proposed framework.

Concurrent programs that contain busy-waiting loops or iterative statements might not stop when they are tested dynamically due to some processes getting stuck in infinite loops or the execution of several loops forming a livelock. The traditional way of handling this problem in dynamic testing - interrupting the execution of the concurrent program when a predefined maximum execution time is exceeded. In this paper, we propose a dynamic decision scheme that spontaneously stops the execution of tested processes when they get stuck in an infinite loop or form a livelock. Since the halting problem is proven to be undecidable, we propose heuristic algorithms to cope with this. We apply the proposed scheme to a dynamic testing methodology called dynamic effective testing, which can perform state- and transition-cover testing for concurrent programs with busy-waiting loops. The implementation and experimental results demonstrate the feasibility of the proposed scheme.

In this paper, we propose an operational model to support the security of Web services. In addition to satisfying the basic security requirements, including authentication, confidentiality, data integrity, and nonrepudiation, the proposed model supports security mechanisms such as element-wise encryption and temporal-based element-wise digital signatures. Furthermore, the proposed model supports a flexible key specification scheme called explicit key definition, which can be used to define three different types of keys: static keys, dynamically selected keys, and keys applied to digital signatures. The service requester can determine the identity of the keys used without negotiating with the service provider. The implementation and experimental results demonstrate the feasibility of the proposed system.

XSLT is a very popular and flexible language for transforming XML documents which provides a powerful implementation of a tree-oriented transformation language for transmuting instances of XML using a single vocabulary into a desired output. In this paper, we propose a processing model that enables the XSLT processor to encrypt and decrypt XML documents. The details of the implementation are presented. Our model supports a more general encryption scope than previous models. The implementation and experimental results demonstrate the practicality of the proposed model. Copyright © 2006 John Wiley & Sons, Ltd.

In this paper, we propose a new failure-recovery model for workflow management systems (WfMSs). This model is supported with a new language, called the workflow failure-handling (WfFH) language, which allows the workflow designer to write programs so that he can use data-flow analysis technology to guide the failure recovery in workflow execution. With the WfFH language, the computation of the end compensation point and the compensation set for failure recovery can proceed during the workflow process run-time according to the execution results and status of workflow activities. Also, the failure-recovery definitions programmed with the WfFH language can be independent, thereby dramatically reducing the maintenance overhead of workflow processes. A prototype is built in a Java-based object-oriented workflow management system, called JOO-WfMS. We also report our experiences in constructing this prototype.

XSLT is a very popular and flexible language for transforming XML documents which provides a powerful implementation of a tree-oriented transformation language for transmuting instances of XML using a single vocabulary into a desired output. In this paper, we propose a processing model that enables the XSLT processor to encrypt and decrypt XML documents. Our model supports a more general encryption scope than previous models. The implementation and experimental results demonstrate the practicality of the proposed model.

The execution of a client/server application involving database access requires a sequence of database transaction events (or, T-events), called a transaction sequence (or, T-sequence). A client/server database application may have nondeterministic behavior in that multiple executions thereof with the same input may produce different T-sequences. We present a framework for testing all possible T-sequences of a client/server database application. We first show how to define a T-sequence in order to provide sufficient information to detect race conditions between T-events. Second, we design algorithms to change the outcomes of race conditions in order to derive race variants, which are prefixes of other T-sequences. Third, we develop a prefix-based replay technique for race variants derived from T-sequences. We prove that our framework can derive all the possible T-sequences in cases where every execution of the application terminates. A formal proof and an analysis of the proposed framework are given. We describe a prototype implementation of the framework and present experimental results obtained from it.

An increasing number of programming languages, such as Fortran 90 and APL, are providing a rich set of intrinsic array functions and array expressions. These constructs which constitute an important part of data parallel languages provide excellent opportunities for compiler optimizations. In this paper, we present a new approach to combine consecutive data access patterns of array constructs into a composite access function to the source arrays. Our scheme is based on the composition of access functions, which is similar to a composition of mathematic functions. Our new scheme can handle not only data movements of arrays of different numbers of dimensions and segmented array operations but also masked array expressions and multiple sources array operations. As a result, our proposed scheme is the first synthesis scheme which can synthesize Fortran 90 RESHAPE, EOSHIFT, MERGE, and WHERE constructs together. Experimental results show speedups from 1.21 to 2.95 for code fragments from real applications on a Sequent multiprocessor machine by incorporating the proposed optimizations.

Concurrent programs are more difficult to test than sequential programs because of non-deterministic behavior. An execution of a concurrent program non-deterministically exercises a sequence of synchronization events called a synchronization sequence (or SYN-sequence). Non-deterministic testing of a concurrent program P is to execute P with a given input many times in order to exercise distinct SYN-sequences. In this paper, we present a new testing approach called reachability testing. If every execution of P with input X terminates, reachability testing of P with input X derives and executes all possible SYN-sequences of P with input X. We show how to perform reachability testing of concurrent programs using read and write operations. Also, we present results of empirical studies comparing reachability and non-deterministic testing. Our results indicate that reachability testing has advantages over non-deterministic testing.

Concurrent programs are more difficult to test than sequential programs because of nondeterministic behavior. An execution of a concurrent program nondeterministically exercises a sequence of synchronization events, called a synchronization sequence (or SYN-sequence). Nondeterministic testing of a concurrent program P is to execute P with a given input many times in order to exercise distinct SYN-sequences and produce different results. We present a new testing approach, called reachability testing. If P with input X contains a finite number of SYN-sequences, reachability testing of P with input X can execute all possible SYN-sequences of P with input X. We show how to perform reachability testing of concurrent programs using read and write operations. Also, we present results of empirical studies comparing reachability and nondeterministic testing. Our results indicate that reachability testing has advantages over nondeterministic testing.>