<p>This paper matches some of your criteria:</p>

<ul>
<li>Nenad Dedic, Mariusz H. Jakubowski, Ramarathnam Venkatesan: <a href="http://research.microsoft.com/apps/pubs/default.aspx?id=77270" rel="nofollow">A Graph Game Model for Software Tamper Protection</a>. Information Hiding 2007: 80-95</li>
</ul>

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

CC BY-SA 3.0
2012-01-17T08:36:25.990Z
2012-01-17T08:36:25.990Z
Dave Clarke
<p>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 </p>

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

<p>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. </p>

<p>Is this what you are looking for?</p>

CC BY-SA 3.0
2012-02-01T13:47:10.177Z
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
CC BY-SA 3.0
2012-01-17T12:36:59.957Z
2012-01-17T12:36:59.957Z
Klaus Draeger
<p>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. </p>

<p><a href="http://dl.acm.org/citation.cfm?id=512973" rel="nofollow">Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fix points</a>.</p>

CC BY-SA 3.0
2012-01-17T02:27:56.590Z
2012-01-17T02:27:56.590Z
Ahmed Masud
<p>I am looking into some security analysis of arbitrary code which is represented as a graph</p>

<p>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 ?</p>

<p>Can anyone direct to any specific terms or papers i should be looking into ?</p>

CC BY-SA 3.0
2012-01-17T08:54:32.613Z
I'm not sure what you mean by "A provable graph walk which is shorter than a graph walk itself."
Dave Clarke
CC BY-SA 3.0
2012-02-01T13:38:05.850Z
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
<graph-theory><security>
representing code path as graph walks.. a provable graph walk?
O A
# representing code path as graph walks.. a provable graph walk?

(Asked by: username_0 on 2012-01-16)

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 ?

**Tags:** graph-theory, security
> **Comments:**
> **username_1**: I'm not sure what you mean by "A provable graph walk which is shorter than a graph walk itself."  
> **username_0**: 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  

---

## 3 answers

### Answer by username_1 on 2012-01-17. Score: 1 | Accepted answer

This paper matches some of your criteria:

* Nenad Dedic, Mariusz H. Jakubowski, Ramarathnam Venkatesan: [A Graph Game Model for Software Tamper Protection](http://research.microsoft.com/apps/pubs/default.aspx?id=77270). Information Hiding 2007: 80-95

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


---

### Answer by username_2 on 2012-01-17. Score: 1

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?

> **Comments:**
> **username_0**: 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...  

---

### Answer by username_3 on 2012-01-17. Score: 0

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.

[Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fix points](http://dl.acm.org/citation.cfm?id=512973).


---

