Our Audit Approach

Our Static Analysis Approach

Broadly speaking, static analysis tools come in two flavors, depending on the kind of guarantees they can provide. Complete tools are adept at finding bugs and guarantee that any malfeasance they detect is a genuine bug, making them ideal for non-expert end users. However, complete tools are in general unable to demonstrate that particular bugs don't exist—they exhibit false negatives. Sound tools, in contrast, are adept at demonstrating that particular classes of bugs do not exist. Like a typechecker, they rule out misbehavior before the program ever runs—misbehavior specific to your program. However, this strong guarantee comes at a cost: sound tools can raise false positives, which can be difficult to identify as such. This particular feature makes them ideal for use by expert auditors.