Ponce
Search…
Ponce limitations
Ponce and Triton, the framework that Ponce relies on, have some limitations due to the nature of concolic execution. It is important to understand these limitations before you start using Ponce.
Symbolic index while doing a memory load or write
When the index used to read a memory value is symbolic, like in:
1
x = aray[symbolic_index]
Copied!
Some problems arise that could lead to the loose of track of the tainted/symbolized user controled input.
This is a common problem with symbolic/concolic execution, there are some mitigations but it's not trivial to solve it.
One simple example where this happens:
1
#include<stdio.h>
2
3
char * alphabet = "ABCDEFGHIJKLMNOPQRSTUVWXYZ";
4
5
int toUpper(char *userinput) {
6
for (int i=0; i < strlen(userinput); i++){
7
// We loose here the symbolic tracking, when using a symbolic index to access non symbolic data, alphabet
8
userinput[i] = alphabet[userinput[i] - 'a'];
9
}
10
}
11
12
int main(){
13
char * userinput = malloc(10);
14
memcpy(userinput, "aaaaaaaaa", 10);
15
// Let's image aaaaaaaaa is the userinput that is symbolic
16
toUpper(userinput);
17
// After the execution of the function userinput is not symbolic anymore
18
return 0;
19
}
Copied!
Concolic execution only analyzed the executed instructions
It's obvious but sometimes the implications are not so easy to spot.
This means that symbolic tracking is lost in cases like the following:
1
int check(char myinput) // Input is symbolic/tainted
2
{
3
int flag = 0;
4
if (myinput == 'A') //This condition is symbolic/tainted
5
flag = 1
6
else
7
flag =- 1;
8
return flag; // flag is not symbolic/tainted!
9
}
Copied!
Concolic execution only see one of the branches of the condition, so it doesn't have a way to figure out that the flag value depends on the result of the symbolic condition.
Triton, thereforce Ponce, doesn't work very well with floating instructions
Last modified 1yr ago