"Finding bugs without running or even looking at code" by Jay Parlar

Jay Parlar explains how to use the Alloy model checker to find complex architectural bugs without running or reading code.

What if you could find complex bugs in systems without ever having looked at any of the code, without running the code, without cloning the code, or even knowing what language the code is written in or where its git repo lives? What if you could validate the correctness of an architectural proposal before writing code? While this might sound impossible, it's in fact quite doable, and happening every day! Tools called "model checkers" can be used to model and analyze the architecture/design of a system. Model checkers can simulate every possible sequence of operations your system might ever encounter, and check if desired properties always hold. And if a property doesn't hold, the model checker will show you an exact sequences of operations that violates it. Benefit can be had both in the early design stages of a project, or if you're a newcomer trying to get up-to-speed on an existing system. Examples of both will be shown. This talk will describe the model checker Alloy (alloytools.org). I'll show how we used it to invalidate a large amount of work by one group (before multiple teams started to try integrating with that work). I'll also show how we employed it to find a highly subtle security flaw in another group's project, without ever looking at a single line of code from either group. In both cases, we did this simply by talking to teams about the architecture of their systems, and translating those designs into formal specifications. Jay Parlar Okta @parlar Jay Parlar has been a software developer for ~20 years, and holds a PhD in Software Engineering. His major focus the past ~3 years has been on the application of formal methods to real industry problems. This has resulted in interesting successes with Alloy, TLA+, and in writing a custom model checker in Z3. But he’d also love to talk to you about Python, running and fountain pens!