mr-ma / composition-framework

1 stars 3 forks source link

Build dependency constraints between Vanilla-OH hash and assert calls #18

Closed mr-ma closed 5 years ago

mr-ma commented 5 years ago

In the ILP optimisation we need to make sure that no OH hash is added to the code unless it is verified by an assert. We can build the connection between hash and assert calls based on the global variable that they use. Furthermore, we need to identify all the hash calls that precede asserts with the same global variable. For this purpose, we could use the suggested analysis in #12

Use a DFS - back edges are not allowed by assumption (no cycles). Starting from the entry BB we know all possible BB whose execution may precede a specific BB. Taking the address of a BB means that anybody can call the BB - hence, it is only preceded by the entry block.

dennisfischer commented 5 years ago

Will have a look

dennisfischer commented 5 years ago

This was a rather though task imo. https://github.com/dennisfischer/sip-oblivious-hashing/commit/c8dc84b0465a30d5ed1fa843312c828673680dc8

Have a look at the isReachablePath function. Lacking documentation (in runOnModule lines 2800+) I build the callgraph without allow back edges. I had to make the assumption that we always have a function called main and this function is the entry point to the program.

Assuming the analysis is correct, then the analysis even finds asserts without hashes. These are removed by ILP.

dennisfischer commented 5 years ago

There's a minor change missing. I just remembered that functions whose address have been taken are not considered in this implementation. However, we must assume that anybody can call them.

dennisfischer commented 5 years ago

https://github.com/dennisfischer/sip-oblivious-hashing/commit/8da39a893254b94f5667c3b8cd6da210bcf14f41