In the last few years, reports about software vulnerabilities have become prominent even in mainstream media, because the bugs can be exploited to steal sensitive data, or take over control of devices.
Given that our methods for program analysis are designed to identify all paths through the code, including corner-cases, it should come as no surprise that they can be used to identify security exploits. The biggest research challenge is to analyse all components of the software in its entirety, to ascertain that none of the safeguards placed in the code, such as different layers of sanitisation, don’t prevent the exploit. Our researchers thus concentrate on designing security-driven code abstractions.
Read our published work
Towards Automated Bounded Model Checking of API Implementations by Daniel Neville, Andrew Malton, Martin Brain, and Daniel Kroening
Due to their complexity, currently available bounded model checking techniques based on Boolean Satisfiability and Satisfiability Modulo Theories inadequately handle non-linear floating-point and integer arithmetic. Using a numerical approach, we reduce a bounded model checking problem to a constraint satisfaction problem. Currently available techniques attempt to solve the constraint problem but can guarantee neither global convergence nor correctness. Using the IPOPT and ANTIGONE non-linear programming (NLP) solvers, we transform the original constraint satisfaction problem from one having disjunctions of constraints into one having conjunctions of constraints with a few introduced auxiliary variables. The transformation lowers the computing cost and preserves the Boolean structure of the original problem while complying with limits of NLP solvers.