I am an Assistant Professor in the Electrical and Computer Engineering (ECE) Department at the University of Florida. My research aims to improve reliability and security of systems using formal methods and program analysis. I am looking for motivated and hardworking students who are excited about finding novel solutions for systems security and IoT problems. Interested students are encouraged to apply for the Ph.D. program and send me a non-generic email.
Before joining the ECE Department, I have worked as a Research Scientist at the Computer and Information Sciences and Engineering (CISE) Department at UF between 2004 and 2014. I am still affiliated with the CISE Department as a graduate faculty.
I have received my Ph.D. in computer science from
the Computer Science Department of
University of California, Santa Barbara in 2004. My Ph.D. thesis
was on "Specification and Automated Verification of Concurrency
Controller Components" and was supervised by Tevfik Bultan.
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.
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). Check out the full list of deep bugs/vulnerabilities found by MOXCAFE.
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.
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.
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.
It is a challenge to ensure that a computational element, whether hardware or software, is not compromised and is working as expected. One way to deal with this type of problem is to monitor the run-time behavior to check for divergent behaviors. We are developing scalable techniques that can abstract the potentially big state space of the golden reference to accurately detect divergences.
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.
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.
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.
This course helps students develop modeling, formal specification, and automated verification skills for analyzing complex hardware and/or software systems. The course covers both the theory behind automated verification techniques and practical aspects of verification via hands-on experience with various automated verification tools and guest lectures by practitioners (Fall 2014, 2015, 2016). This course is open to both undergrads and grads.
This course helps students develop a deep understanding of operating system concepts and systems programming fundamentals and gain hands-on experience in systems programming by using Pthreads and by implementing Linux device drivers and testing/verifying systems code for deadlock and race-freedom (Spring 2015, 2016, and 2017). This course is open to both undergrads and grads.