Research Projects and Tools
String analysis is a static analysis technique that determines the string values that a variable can hold at specific points in a program. We develop an automata-based string analyzer, called Stranger (STRing AutomatoN GEneratoR), for real-world web applications. Stranger takes advantage on symbolic representation of automata, which allows the practical handling of automata on very large alphabets. Stranger also incorporates various novel approximation techniques and targets on proving the correctness of secured web applications. We later extend this approach to systems having both string and integer variables. By exchanging length information between string and arithmetic automata, we improve precision of both string and size analysis. Recently, we are interested in backward analysis and path-sensitive analysis using multi-track automata. We also investigate the essence of string systems, and characterize the decidability of reachability analysis on various string systems. Stranger is implemented on top of Pixy and Mona projects. Stranger and benchmarks can be downloaded from here. [SPIN 2008, TACAS 2009, ASE 2009]
We propose a novel method for modular verification of BPEL service composition. We first use symbolic fixpoint computation to derive relations of the incoming and outgoing messages for well-defined web services based on reachability analysis. The relations are collected and serve as a repository of summarizations of individual web services. We then compose the summarization of external invocations, resulting in scalable verification of web service composition. We realize our ideas in VeriBPEL. The technical features include (1) a novel symbolic encoding for modeling the concurrency semantics of systems having both internal multi-threading and external message passing, and (2) a method for summarizing concurrently running processes, along with a modular verification framework that utilizes these summaries for scalable verification. [SIGSOFT/FSE2008]
We aim to verify specifications of object oriented systems based on infinite state model checking techniques. We target on object constraint language and propose size abstraction and size analysis. We conducted a case study on the OCL specifications of Java Card APIs. The experiments indicate our abstraction is precise enough to verify/falsify target systems, while coarse enough to perform complex model checking techniques efficiently. [ESEC/FSE2007]
Neurons are arguably one of the most interesting cell-types in the human body. A large number of neurons working in a cooperative manner are able to perform tasks that are not yet matched by the tools we can build with our current technology. Spiking Neuron P-systems (SNPs) incorporate ideas from spiking neurons into membrane computing. In this project, we give characterizations of sets definable by partially blind multicounter machines in terms of k-output SNPs operating in a sequential mode. [UC2006] [NC2008]
Fabricating large memory and processor arrays is subject to physical failures resulting in yield degradation. The strategy of incorporating spare rows and columns to obtain reasonable production yields was first proposed in the 1970s, and continues to serve as an important role in recent VLSI developments. Since the spare allocation problem (SAP) is NP-complete but requires solving during fabrication, an efficient exact spare allocation algorithm has great value. In this project, we proposed a novel Boolean encoding to reduce exact SAP to the satisfiablity problem, so that we can leverage the capability of modern SAT solvers. [DFT2005]
We propose a new SAT-based model checking algorithm to solve the reachability problem of real-time systems. In our algorithm, the behavior of region automata is encoded as Boolean formulas, and hence any SAT solver can be used to explore the region graph efficiently. Although our SAT-based algorithm performs better than other algorithms in flaw detection, it is less effective inproving properties. To overcome the problem, we incorporate a complete inductive method in our algorithm to improve the performance when the property is satisfied. We implement both algorithms in a tool called xBMC and report experimental results. The experiments show that the combination of efficient encoding and inductive methods offers an effective and practical method for the analysis of timing behavior. [FORMATS/FTRTFT2004][ATVA2004][IJFCS2006]
WebSSARI stands for Web application Security via Static Analysis and Runtime Inspection. Viewing Web application vulnerabilities as a secure information flow problem, we created a lattice-based static analysis algorithm derived from type systems and typestate. During the analysis, sections of code considered vulnerable are instrumented with runtime guards, thus securing Web applications in the absence of user intervention. Soundness, i.e no false negative, is achieved by applying formal methods including typestate checking and bounded model checking. I worked on designing and developing core checkers including: (1) A light-weight Type Checker, and (2) A heavy-weight Bounded Model Checker. [WWW2004][DSN2004]
Here is a related link. Parts of the techniques have been commercialized by Armorize Technologies, Inc..
I was involved in designing and developing RED 4.0 on top of RED, the full Timed-CTL symbolic model checker initiated by Prof. Farn Wang in 1996. RED 4.0 enhanced RED in the following directions: (1) Symbolic Simulation, (2) Numerical Coverage Estimation, (3) Greatest Fixpoint Computation and (4) Symmetric Analysis with Pointer Data Structure. [RTCSA2003][CIAA2003][FORTE2003][TSE2004][TSE2006]
TimeC is a C-like language that supports basic C statements, timed statements, e.g., duration and switch-event, and Open Verification Library(OVL) assertions. I developed an optimized translator that automatically translates programs written in TimeC into timed automata and TCTL formula in the input format of RED. Integrating the translator as the front end of RED, we can automatically verify real-time systems specified in TimeC. [RTCSA2003][JEC2004]