InvPurge : Reducing Invariant Noise with Logical Differencing

Sammanfattning

Smart contracts that facilitate decentralized finance(DeFi) applications have been a desired target for hackers due to the underlying financial stakes. Recent work aims to mitigate these attacks by relying on logical predicates or invariants. A promising approach to support this effort is through automated invariant generation. However notable invariant generation tool InvCon+ suffers from a noise problem. This problem stems from the generation of redundant invariants that cover similar but weaker conditions as other invariants generated. In this work we present INVPURGE an invariant reduction tool to mitigate this issue. Our findings show that INVPURGE is both effective and accurate in reducing invariants from InvCon+.