Talk given at LAAS, CNRS, Toulouse, France. Feb 19th, 2010.
[ Slides in PDF ]
Abstract: Applications can fail in the field due to subtle runtime errors introduced by hardware and software faults. Further, they can be subject to security attacks by malicious users. Therefore, it becomes necessary to design runtime mechanisms for detecting errors and attacks in applications. Fault-injection and attack-injection (to a lesser extent) are the de-facto methods for evaluating the efficacy of such mechanisms. However, they both rely on statistical or anecdotal evidence to uncover gaps in the coverage provided by the mechanisms and may not expose corner cases that cause the application failures or compromises.
We propose the use of formal methods as a complement to traditional fault-injection to uncover corner cases of errors and security attacks in applications. Our approach uses a combination of symbolic execution and model checking to systematically inject faults and attacks and evaluate their consequences. We present two systems that embody these ideas, SymPLFIED for fault injection and, SymPLAID for attack injection. The main advantage of our approach is that it operates directly on the assembly language representation of the program and requires very little manual intervention. Further, by using symbolic abstraction techniques, we can control state-space explosion and scale the technique to realistic programs. We demonstrate the approach on two applications, one in the aircraft control domain (tcas) and the other in the security domain (OpenSSH). We are working on scaling this approach to even larger programs. I will also discuss how we can use formal methods to perform better error diagnosis and to benchmark applications’ dependability.
