Formal Methods

This project is about formal validation of error and attack detectors and is part of my PhD thesis at the University of Illinois.


Fault-injection is a commonly used technique to evaluate fault-tolerant systems. It consists of perturbing the state of the system by injecting a fault and testing if the system is resilient to the fault. While fault-injection is valuable, it is an ad-hoc technique and is not guaranteed to find all the corner case errors that escape detection and cause the system to fail. To alleviate this drawback, we propose a formal approach to validate the fault-tolerance of detection mechanisms in general-purpose programs. The main advantage of this approach is that it can exhaustively explore the effects of all faults in a fault-model on a program protected with one or more error-detectors, and can quickly isolate the failure-causing errors. Further, the approach operates directly on the program expressed in assembly language and does not require any special annotations (other than generic descriptions of the failures). Finally, the approach does not pre-suppose specific detection mechanisms such as duplication, and can work with an arbitrary set of error detectors.

We extend the above approach for identifying security attacks in applications. The goal is to understand whether an attacker who is within the program (i.e., an insider) can achieve their desired objective (i.e., authenticate themselves incorrectly to the system) by strategically corrupting one or more data values in the program’s address space. Earlier work has shown that such attacks are feasible. To the best of our knowledge, ours is the first approach to systematically discover these insider attacks and guarantee completeness of the discovery process under a given attack model.

Project Summary

Formal framework for validating error/attack detectors

The goal of this project is to validate the error/attack detectors embedded in a program for their efficacy in detecting faults or security attacks. The above figure shows the formal framework used for validation. The framework accepts as inputs the assembly code of the program with one or more detectors that need to be verified. The technique directly works on the assembly language code and produces as output the set of errors/attacks that escape the detection mechanisms and cause failure/compromise. Based on the output of the framework, the detection mechanisms can be improved to close the exposed holes.

The key technique used for validation is symbolic execution-based model checking. The approach symbolically executes the program under errors/attacks and uses formal model-checking to solve for specific error or attack constraints. SymPLFIED finds errors while SymPLAID finds attacks. The main difference between these two systems is the precision of the constraint solver used – SymPLAID is more precise but can model only a small number of attacks. This is because opportunities for security attacks tend to fewer in number than errors, but require higher precision to avoid false-positives. SymPLFIED on the other hand is less precise, but can model a large number of errors without running out of space.

Project Publications.

Collaborators : Nithin Nakka, Flore Yuan, Zbigniew Kalbarczyk, and Ravishankar Iyer .