Consider the problem of auditing an investment fund. This usually involves inspecting each transaction in its trading history, and accumulating its capital gains and losses, so that its net asset value can be computed precisely to avoid financial frauds. We present ZeroAUDIT, a confidential and privacy preserving auditing platform, which accomplishes this goal without having to know any of a transaction’s details. Sitting at the heart of the system is a zero knowledge proof protocol, in the discrete logarithm setting, which allows one to reason about the elements of a Merkle tree. Using it, we can prove that a trading transaction is occurring at a fair market price without disclosing which securities are being traded. We have implemented the system on the Hyperledger Fabric platform and we report the use of batch verification techniques in improving its efficiency.

We present LINK-REPORT, a distributed learning outcome analysis module that is integrated with the WISEngineering platform for supporting informal learning in engineering. LINK-REPORT provides a coherent workflow of outcome analysis: starting from development of learning outcome goals, to learner behavior collection, to automated grading of open ended short answer questions, and to report generation and aggregation. It generates learning data for research opportunities in modeling of learner traits.

Abstract Modern web applications often suffer from command injection attacks. Even when equipped with sanitization code, many systems can be penetrated due to software bugs. It is desirable to automatically discover such vulnerabilities, given the bytecode of a web application. One approach would be symbolically executing the target system and constructing constraints for matching path conditions and attack patterns. Solving these constraints yields an attack signature, based on which, the attack process can be replayed. Constraint solving is the key to symbolic execution. For web applications, string constraints receive most of the attention because web applications are essentially text processing programs. We present simple linear string equation (SISE) , a decidable fragment of the general string constraint system. SISE models a collection of regular replacement operations (such as the greedy, reluctant, declarative, and finite replacement), which are frequently used by text processing programs. Various automata techniques are proposed for simulating procedural semantics such as left-most matching. By composing atomic transducers of a SISE, we show that a recursive algorithm can be used to compute the solution pool, which contains the value range of each variable in concrete solutions. Then a concrete variable solution can be synthesized from a solution pool. To accelerate solver performance, a symbolic representation of finite state transducer is developed. This allows the constraint solver to support a 16-bit Unicode alphabet in practice. The algorithm is implemented in a Java constraint solver called SUSHI. We compare the applicability and performance of SUSHI with Kaluza, a bounded string solver.

Analyzing interactions among peers that interact via messages is a crucial problem due to increasingly distributed nature of current software systems, especially the ones built using the service oriented computing paradigm. In service oriented computing, interactions among peers participating to a composite service involve message exchanges across organizational boundaries in a distributed computing environment. In order to build such systems in a reliable manner, it is necessary to develop techniques for analysis and verification of interactions among services. Collaboration diagrams provide a convenient visual model for modeling service interactions. In this paper, we present a tool that (1) checks the realizability of interactions specified by the given collaboration diagram, (2) verifies the LTL properties of the interactions specified by the given collaboration diagram by automatically converting it to a state machine model, and (3) synthesizes peer state machines that realize the set of interactions specified by the given collaboration diagram.

Providing consistent, instant, and detailed feedback to students has been a great challenge in teaching Web based computing. We present the prototype of an automated grading system called ProtoAPOGEE for enriching students' learning experience and elevating faculty productivity. Unlike other automated graders used in introductory programming classes, ProtoAPOGEE emphasizes the examination of quality attributes of student project submissions, in addition to the basic functionality requirements. The tool is able to generate step by step play-back guidance for failed test cases, hence providing informative feedback to help students make reflective and iterative improvements in learning.

Recently SQL injection attack (SIA) has become a major threat to Web applications. Via carefully crafted user input, attackers can expose or manipulate the back-end database of a Web application. This paper proposes the construction and outlines the design of a static analysis framework (called SAFELI) for identifying SIA vulnerabilities at compile time. SAFELI statically inspects MSIL bytecode of an ASP.NET Web application, using symbolic execution. At each hotspot that submits SQL query, a hybrid constraint solver is used to find out the corresponding user input that could lead to breach of information security. Once completed, SAFELI has the future potential to discover more delicate SQL injection attacks than black-box Web security inspection tools.

We present a design for verification approach to developing reliable web services. We focus on composite web services which consist of asynchronously communicating peers. Our goal is to automatically verify properties of interactions among such peers. We propose a design pattern that eases the development of such web services and enables a modular, assume-guarantee style verification strategy. In the proposed design pattern, each peer is associated with a behavioral interface description which specifies how that peer will interact with other peers. Using these peer interfaces we automatically generate BPEL specifications to publish for interoperability. Assuming that the participating peers behave according to their interfaces, we verify safety and liveness properties about the global behavior of the composite web service during behavior verification. During interface verification, we check that each peer implementation conforms to its interface. Using the modularity in the proposed design pattern, we are able to perform the interface verification of each peer and the behavior verification as separate steps. Our experiments show that, using this modular approach, one can automatically and efficiently verify web service implementations.

We present a framework for analyzing interactions among Web services that communicate with asynchronous messages. We model the interactions among the peers participating in a composite Web service as conversations, the global sequences of messages exchanged among the peers. This naturally leads to the following model checking problem: Given an LTL property and a composite Web service, do the conversations generated by the composite Web service satisfy the property? We show that asynchronous messaging leads to state space explosion for bounded message queues and undecidability of the model checking problem for unbounded message queues. We propose a technique called synchronizability analysis to tackle this problem. If a composite Web service is synchronizable, its conversation set remains the same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite Web services with unbounded message queues can be verified completely using a finite state model checker such as SPIN. We also show that synchronizability analysis can be used to check the reliability of top-down conversation specifications and we contrast the conversation model with the Message Sequence Charts. We integrated synchronizability analysis to a tool we developed for analyzing composite Web services.

A conversation protocol is a top-down specification framework which specifies desired global behaviors of a Web service composition. In our earlier work (Fu et al., 2003) we studied the problem of realizability, i.e., given a conversation protocol, can a Web service composition be synthesized to generate behaviors as specified by the protocol. Several sufficient realizability conditions were proposed by Fu et al. (2003) to ensure realizability. Conversation protocols studied by Fu et al. (2003), however, are essentially abstract control flows without data semantics. This paper extends the work by Fu et al. (2003) and achieves more accurate analysis by considering data semantics: to overcome the state-space explosion caused by the data content, we propose a symbolic analysis technique for each realizability condition. In addition, we show that the analysis of the autonomy condition can be done using an iterative refinement approach.

The use of XML as the de facto data exchange standard has allowed integration of heterogeneous web based software systems regardless of implementation platforms and programming languages. On the other hand, the rich tree-structured data representation, and the expressive XML query languages (such as XPath) make formal specification and verification of software systems that manipulate XML data a challenge. In this paper, we present our initial efforts in automated verification of XML data manipulation operations using the SPIN model checker. We present algorithms for translating (bounded) XML data and XPath expressions to Promela, the input language of SPIN. The techniques presented in this paper constitute the basis of our Web Service Analysis Tool (WSAT) which verifies LTL properties of composite web services.

This paper presents a set of tools and techniques for analyzing interactions of composite web services which are specified in BPEL and communicate through asynchronous XML messages. We model the interactions of composite web services as conversations, the global sequence of messages exchanged by the web services. As opposed to earlier work, our tool-set handles rich data manipulation via XPath expressions. This allows us to verify designs at a more detailed level and check properties about message content. We present a framework where BPEL specifications of web services are translated to an intermediate representation, followed by the translation of the intermediate representation to a verification language. As an intermediate representation we use guarded automata augmented with unbounded queues for incoming messages, where the guards are expressed as XPath expressions. As the target verification language we use Promela, input language of the model checker SPIN. Since SPIN model checker is a finite-state verification tool we can only achieve partial verification by fixing the sizes of the input queues in the translation. We propose the concept of synchronizability to address this problem. We show that if a composite web service is synchronizable, then its conversation set remains same when asynchronous communication is replaced with synchronous communication. We give a set of sufficient conditions that guarantee synchronizability and that can be checked statically. Based on our synchronizability results, we show that a large class of composite web services with unbounded input queues can be completely verified using a finite state model checker such as SPIN.

This paper introduces a framework for modeling and specifying the global behavior of e-service compositions. Under this framework, peers (individual e-services) communicate through asynchronous messages and each peer maintains a queue for incoming messages. A global "watcher" keeps track of messages as they occur. We propose and study a central notion of a "conversation", which is a sequence of (classes of) messages observed by the watcher. We consider the case where the peers are represented by Mealy machines (finite state machines with input and output). The sets of conversations exhibit unexpected behaviors. For example, there exists a composite e-service based on Mealy peers whose set of conversations is not context free (and not regular). (The set of conversations is always context sensitive.) One cause for this is the queuing of messages; we introduce an operator "prepone" that simulates queue delays from a global perspective and show that the set of conversations of each Mealy e-service is closed under prepone. We illustrate that the global prepone fails to completely capture the queue delay effects and refine prepone to a "local" version on conversations seen by individual peers. On the other hand, Mealy implementations of a composite e-service will always generate conversations whose "projections" are consistent with individual e-services. We use projection-join to reflect such situations. However, there are still Mealy peers whose set of conversations is not the local prepone and projection-join closure of any regular language. Therefore, we propose conversation specifications as a formalism to define the conversations allowed by an e-service composition. We give two technical results concerning the interplay between the local behaviors of Mealy peers and the global behaviors of their compositions. One result shows that for each regular language, its local prepone and projection-join closure corresponds to the set of conversations by some Mealy peers effectively constructed from . The second result gives a condition on the shape of a composition which guarantees that the set of conversations that can be realized is the local prepone and projection-join closure of a regular language.