# representing code path as graph walks.. a provable graph walk?

I am looking into some security analysis of arbitrary code which is represented as a graph

Are there any papers on whcih graphs walks are valid code paths ? Or a provable graph walk which is shorter than a graph walk itself ?

Can anyone direct to any specific terms or papers i should be looking into ?

• I'm not sure what you mean by "A provable graph walk which is shorter than a graph walk itself." Commented Jan 17, 2012 at 8:54
• Your paper below is very helpful and I am following all its citations... Specifically, i was hoping to find some sort of iterative hash/signature of the graph walk / code path... so that if the code path is n elements, the hash size is log(n) or whatever
– O A
Commented Feb 1, 2012 at 13:38

This paper matches some of your criteria:

It uses random walks on the flow graph of a program to make the program more tamper resistant.

What is your notion of validity? If it means that the branches you take are consistent with the data, then your problem sounds very similar to the counterexample analysis which has to be done as a part of abstraction refinement. In a nutshell, your edges have transition relations associated with them, and you need to check satisfiability of an expression like

$\tau_1(X_1,X_2)\wedge\dots\wedge\tau_n(X_n,X_{n+1})$,

where the $X_i$ are copies of your set of state variables. This is usually handed to an SMT (SAT Modulo Theories) solver such as YICES or Z3.

Is this what you are looking for?

• Ok great. But is there any discussions on how to reduce the size of the expression ? So that satisfiability of a much shorter expression provides (with high probability) proof of the graph walk...
– O A
Commented Feb 1, 2012 at 13:47

Hi i find the question interesting. I haven't seen much on the topic of graph-theoretic approach to software analysis, validation or bounds checking (and in general anything similar that would pertain to software security) in the literature.