I am interested in applying formal methods and program analysis techniques for improving systems reliability with an emphasis on systems and Internet of Things security.

Projects

api model guided analysis

Component-level analysis provides scalability. In complex frameworks, component-level analysis requires a precise modeling of the environment to yield precise analysis. We developed an API modeling language, PROSE, and an API model guided symbolic execution tool, PROMPT to enable precise component-level analysis. PROMPT has been implemented on top of the KLEE symbolic execution engine. PROMPT is available at https://github.com/sysrel/PROMPT. See SECDEV’20 tutorial slides.

Model Extraction for Callback-based Frameworks (MOXCAFE)

Complex frameworks such as operating system kernels use the callback mechanism to achieve extensibility. However, the callback mechanism creates challenges for program analysis. We use a staged programming model guided analysis to detect bugs/vulnerabilities that involve callbacks, which we call deep vulnerabilities. Our tool, MOXCAFE, has been implemented using the LLVM compiler framework. We have detected a new double-free (and use-after-free) vulnerability in a USB audio/video grabber device (see CVE-2017-17975 for more details).

State Machines with Callback Mechanism (SMACK)

Programming models based on the callback mechanism provide extensibility and are widely used in modern software, e.g., Linux kernel and Android Framework. However, callbacks introduce challenges in the context of concurrency. Our modeling language SMACK extends state machine based formalism using callback instantiation constructs. SMACK models have a formal semantics and can be analyzed using model checkers.

Partial Predicate Abstraction

Predicate abstraction is an effective technique for analyzing infinite-state systems. An alternative approach is representing the state space concretely and approximating the solutions to the fixpoint computations for model checking. As models to be verified get large each technique easily reaches its limit, i.e., in terms number of predicates and number of constraints, respectively. Combining the two approaches by abstracting part of the state space and keeping the remaining part in its concrete domain provides a balance for state space reduction and precision.

Detecting Malicious USB Devices

Universal Serial Bus (USB) is a protocol that is not designed to be secure. This creates multiple attack surfaces including tricky behaviors that are normally allowed by the protocol, e.g., the BadUSB attack, and data integrity violations that can crash the system software stack such as the USB Core layer and the device drivers. In this work we leverage domain specific knowledge to come up with scalable analysis techniques.

Change Impact Analysis (CHIMP)

As software gets complex, it becomes even more difficult to get concurrency right. In this project, we developed a static analysis tool to detect code changes that introduced deadlocks into Java programs. We applied our tool to various components of large-scale projects and detected real deadlocks and linked them to the code changes. You can download CHIMP here.

Previous Projects

Action Language Verifier (ALV)

ALV is an infinite-state model checker for Computational Tree Logic (CTL) developed by VLab of UCSB. It uses a composite symbolic representation approach to represent each domain using the most suitable representation, e.g., BDDs for the boolean domain and polyhedra based representation for the integer domain. It uses fixpoint approximations to achieve convergence.

Java Race Finder (JRF)

JRF is an extension project for Java Path Finder (JPF), a model checker for Java programs. It incorporates Java Memory Model to precisely detect race conditions. It can also provide suggestions on how to fix detected race conditions.