>_

About Frank


Frank is a doctoral student in the Department of Computing at Imperial College London, and holds a Diploma in Computer Science from the Technische Universität Dresden. He found particular interest in Symbolic Execution, software analysis and testing, so decided to continue expanding his knowledge of it later on in his life. Previously, Frank had worked as a Research Assistant for the System Engineering Group at his university. He had taught for several years as well, but decided to do more research instead.


Frank finds enjoyment in his PhD research, since it allows him to explore new ideas without the pressure of industry, which he otherwise finds rather stressful. He works in the Software Reliability Group under the supervision of Dr Cristian Cadar, who is responsible for developing the KLEE system, which forms the basis of Frank’s PhD research.




>_

Symbolic Execution


Symbolic execution is a method of auto-testing a program by passing in variable inputs to a function. It will then use an interpreter to run through the function or program. When a conditional statement is reached, it will branch, limiting the scope of the variable input to that which either causes a true or false outcome for the conditional statement, depending on the requirements of that branch.


The current best implementation of this system is the KLEE program, which has been used to test Unix library files and has achieved high levels of program coverage. It was able to find several bugs within the files and then provided test cases based on the scope of the various inputs at that particular branch.


Symbolic execution itself has been around since the 1970s, when it was first propounded in the paper on the SELECT system by Boyer, Elspas and Levitt. In the beginning however, it faced several major difficulties. The main difficulty impeding further development was that symbolic execution is very resource intensive and computers at the time were just not powerful enough to run the process.


The other major issue was the lack of optimisations, especially in pruning branches of the program dynamically. By 2008 however, when the KLEE paper was published, computing power had greatly increased and many more optimisations were available to them than were around in the 1970s. This allowed for vastly improved program coverage, reaching up to 99% of some files when tested and being capable of handling code in the thousands of lines, instead of the simple programs previously testable.



>_

Frank's Work


The main obstacle to overcome in Symbolic Execution regards the fact that to test every possible path of program input for a program is of an exponential complexity, and hence becomes very time consuming. It becomes infeasible therefore to test immensely long programs, over and over whenever the slightest alteration is made to the code base. It would be advantageous to have an efficient solution to this complexity problem – hence Resumable Symbolic Execution.


Whilst not decreasing the overall complexity, Resumable Symbolic Execution allows the previously generated code paths to be saved, so that whenever a change is committed to the code, the entire tree does not have to be generated from scratch, rather, it can be extended from the prior generated tree, dramatically decreasing execution time. This allows for much easier scaling for larger programs, especially if they have been built from scratch with the testing added progressively.


The present implementation of this is as an add-on to the KLEE symbolic virtual machine, creating Resumable Paths from the intermediate representation (LLVM) of languages like C++.



>_

Example of KLEE


The following is a function, in C, detailing how to get the sign of a given integer input, along with the symbolic execution tree that represents how the KLEE program would interpret the function. Each if statement is represented by a branch in the tree and with alpha acting as the variable input, the way this is limited is detailed on the side of each branch.

            
       1 int get_sign(int x) {
       2  if (x == 0)
       3 		return 0;
       4 
       5  if (x < 0)
       6 		return -1;
       7 
       8  else
       9  	return 1;
      10 
      11 int main() {
      12 		int a;
      13     klee_make_symbolic(&a, sizeof(a), "a");
      14     return 0;
Symbolic execution tree