Summary

From the conference brochure:

If you have ever tried to completely & accurately describe the insecurities (at every level of abstraction) in a system, you have probably noticed that there is no widely known, repeatable, and reasonably doable method for doing so. You could easily conclude that whole halting problem thing is stopping people. ;)

The thing about undecidable problems is that there exist algorithms which will solve particular cases, there exist algorithms which can make good predictions or approximations for particular cases, and there exist algorithms which can solve pieces of the problem. Essentially, by approaching the problem from different angles, you can move the insolubility around. For example, formal verification can be used in some situations, to prove or disprove a program’s adherence to a formal specification. This moves some security-related insolubility from the program to the specification.

Brenda will present a brief overview of Trike (the way she, Eleanor Saitta and Michael Eddington are currently organizing this problem), the key differences between Trike and previous threat modeling work, the algorithm Trike uses to automatically generate all the top-level threats for a system, some assumptions that make this possible, and a description of where she thinks the insolubility will end up when the problem is organized this way.

Slides & Demo

If you were at the talk, you recall that the slides and demo didn’t work entirely properly. Well, they still don’t, and they aren’t going to. Sorry. :(