Binary Program Analysis
Program analysis is an old dream in computer science. Unfortunately, it has been shown impossible (in the general case) when computer science was just starting to rise from mathematics and electrical engineering in the very beginning of the twentieth century. Some people even consider that the discovery of this impossibility result itself, found by Kurt Gödel, is at the origin of computer science.
But, even if full program analysis has been shown impossible, research in this field did not stop. It is still possible to ensure full verification of program in some particular conditions and, in most of the cases, partial verification may be enough to catch most of the bugs in a program. Thus, research in the most efficient techniques to analyze programs has been conducted since the beginning of computer science and is still quite vivid nowadays.
Since recently, program analysis was performed based on hand-made models or source code of the original program. But, recently, thanks to progress in this field, people started to consider to base their analysis directly on the binary form of the program. Nevertheless, a certain amount of problems, specifically linked to binary analysis have to be solved first. Most of these problems are related to the recovery of the high-level of the original program:
- Recovery of the program control-flow;
- Recovery of the variables types;
- Recovery of the high-level constructs of the program (procedures, libraries, modules, objects, …);
- Scaling-up to big program analysis.
For now, I am actively working on the ‘recovery of the program control-flow‘ problem with the help of the Insight framework. But, there is still a lot of work to do in this field.
While working on binary analysis, we encountered several obfuscated programs. I realized then that obfuscation and analysis were exactly dual. And, trying to figure out how to perform one will give you hints on how to perform the other. Moreover, there were a lot of demands about formalizing and improving the current knowledge in obfuscation. Still, obfuscation, in its general form, has also been shown impossible by Barak et al. [Ba12]. But, a lot of recent works [Wyseur09, GGHRSW13, Klinec13] have raised quite interesting techniques to be investigated and applied to real programs.
I am just starting this topic, I need a bit more time to take some insight of it.
Verification of real-time systems is a topic that has been investigated since the very beginning of computer science. Obviously because most of the embedded programs have to interact in real-time with the an environment that cannot be totally controlled or tamed.
Despite several theoretical and practical breakthroughs in the way of modeling real-time system, this problem remain a hard one, essentially because we try to control events occurring within continuous time with a discrete machine.
Timed automata model, introduced by Rajeev Alur and David Dill in 1995, bring a full and complete theoretical framework to reason about time systems in a discrete way. Introducing a link between the usual finite automata theory and real-time systems. The major breakthrough brought by this model was a finite abstraction of continuous time allowing to explore reachable states of a discrete system equipped with clocks.
My co-authors and I, have contributed to this field in several ways and in various topics:
- Updatable Timed Automata [BDFP04]: This model is an extension of the original timed automata model. We proved it as strictly more expressive than the original model [BDFP00a] and yet we proved that deciding of the emptiness of the language of a given automata was P-space complete [BDFP00b]. I did implement this extension in the Uppaal tool at the beginning of my stay in Denmark.
- Tight Alive Clocks Analysis [BBFL03]: Most of the lambda users, when asked to build a timed model for the first time, tend to use much more clocks than really needed. The problem is that each clock might increase exponentially the complexity of the verification. Using static-analysis techniques on the model to locally reduce the set of active clocks in the tightest possible way had really a huge impact in the tool. And, many models started to be verified, where they could even be considered before.
- Timed Games & Control
work was really a major breakthrough because we did settle
down and use for real-world cases, a practical model to
express timed games and synthesize control algorithms given
a modelization of the problem.
was the tool that came out of this work and it had quite
some success in solving a few user cases.
Practical applications of our work in this field was really a surprise (at least to me) because we were dealing with high-complexity problems, but thanks to a combination of choosing the right algorithms and abstractions together with the right implementation and data-structures, we manage to get through interesting practical problems.