It was a busy weekend. I competed with PPP in the 20th Defcon CTF. Unlike last year, I competed remotely from Pittsburgh. This year’s Defcon CTF ran much more smoothly than last year. PPP got 2nd place. We are disappointed we didn’t win, but we did pretty well. We only had about 12 people on our team. Someone said the winning team had about 50 people on it! Pretty crazy.

Anyway, I spent more time thinking about the VSA problem I posted about last time, and my conclusion is that SSA form can actually be harmful for abstract interpretation. In dataflow, the order vertices are visited in does not matter, since the solution to the dataflow should be the meet over all paths.

This property does not hold for abstract interpretation, and the final result can vary depending on the path taken. Converting to SSA form effectively changes the path taken by the abstract interpretation algorithm, so it should not be too surprising that we get a different answer.

I decided to deal with this by changing our VSA implementation to operate on non-SSA CFGs. This makes sense for VSA, but also for CFG recovery in general, since converting to SSA in a dynamic fashion seems difficult anyway.

Here’s the final result I get from VSA for my toy example:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

VSA @BB_Entry
 R_ESP_1:u32 -> (R_ESP_1:u32 |=> 0[0,0])

VSA @BB_Exit
 R_ESP_1:u32 -> (R_ESP_1:u32 |=> 0[0,0])
 x_81:u32 -> ($ |=> 1[1,3])

VSA @BB_Indirect

VSA @BB_Error

VSA @BB_0
 R_ESP_1:u32 -> (R_ESP_1:u32 |=> 0[0,0])
 x_81:u32 -> ($ |=> 0[0,0])

VSA @BB_1
 R_ESP_1:u32 -> (R_ESP_1:u32 |=> 0[0,0])
 x_81:u32 -> ($ |=> 1[1,3])

VSA @BB_2
 R_ESP_1:u32 -> (R_ESP_1:u32 |=> 0[0,0])
 x_81:u32 -> ($ |=> 1[1,3])

Here’s the CFG again for reference: