College of Science & Engineering
This group's research applies automated program analysis techniques to computer software, generally operating on compiled binaries, to improve the software's quality and security, such as creating test cases or finding bugs that represent security vulnerabilities. Two key techniques used in this work are symbolic execution and logical decision procedures, which automate reasoning about the possible execution paths through software while retaining precision (e.g., not using information-losing approximations). Decision procedures are back-end tools that check whether logical combinations of mathematical statements are true or false: they allow symbolic execution to determine whether particular execution paths are feasible, and create input test cases for them if so. Because these techniques perform precise reasoning, they require substantial computing power to produce full results, as the software analyzed gets bigger; but generally they are organized into larger tasks that are highly parallelizable.
These researchers are using MSI for two projects:
- Heap-Related Software Vulnerabilities: The "heap" is the name for the memory region programs use for allocating objects whose lifetime is not known at the time a program is compiled. Because decisions about heap allocation must be made at runtime, they require a library with data-structures to efficiently keep track of what memory has been allocated to what object. However, if a buggy program comes under attack, heap data structures can also be a point of vulnerability, because the heap management library may be tricked into changing memory in a way useful to an attacker if the data that it uses is maliciously corrupted. Vulnerabilities that can be exploited together with a heap management library are a cutting-edge area for automatic vulnerability finding using symbolic exploration, which this group is exploring using their FuzzBALL binary symbolic execution tool.
- Improving Algorithms for Model Counting: Model counting refers to the task of counting the number of satisfying assignments to a formula: it generalizes the more common satisfiability task for decision procedures that asks whether at least one satisfying assignment exists, and is usually significantly more challenging. This group has an ongoing research project investigating more efficient (sometimes approximate) techniques for model counting over the logical formulas that describe the behavior of software. They use these techniques for instance to assess whether the execution of a program or the report generated by a crash might reveal private information, in which they use model counting to implement information-theoretic measures of program behavior such as entropy or channel capacity. They are currently running experiments comparing a state-of-the-art exact model counting tool with probabilistic or conservatively approximate approaches they have implemented.