Reducing memory consumption of ProVerif with hash consing techniques

Links:   Paper   |   Slides   |   Code artifact

We have added a new internal library to ProVerif which allows us to adapt the classic techniques of hash consing to the internal representation of terms, thus maximising memory sharing. In particular, with this new library, two semantically equal messages will be guaranteed to be physically equal (they will point to the same address in memory). Once this representation was added, we had to adapt the classical operations of ProVerif on terms such as matching or unification. The internal algorithm of ProVerif being mainly based on the saturation of Horn clauses, a maximal sharing of the memory within each clause but also within the whole set of Horn clauses generated by ProVerif allows us to considerably reduce the memory consumption. While maximizing memory sharing within a clause is fairly straightforward, for Horn clauses sets, the problem becomes much more difficult due to the presence of variables that may have to be considered as distinct in two different clause sets.