Automatic Abstraction for Congruences -- A Story of Beauty and the Beast

Andy King

My work at Portcullis focuses on deriving invariants from binaries to support security engineers (white-hats). The talk will explain how filthy bit-level operations can be modeled with matrices of linear congruence equations. By composing the matrices (something that is beautifully simple), the invariants in the binary then just drop-out, giving a way to discover what a program actually does without even running it (a problem that one would initially think to be a beast).