Presented at AppSec USA 2014
Sept. 19, 2014, 10:30 a.m.
Threat modeling is an important part of any secure development process. By identifying potential threats early in the development, you can build effective mitigations into your system, rather than relying on costly patches and bug fixes.
Existing techniques for modeling threats involve a whiteboard or some form of diagramming, with a few specialized tools capable of generating a list of threats that may be applicable to your system. These tools are indispensable, but provide a limited form of feedback and interaction. You can't, for example, state a security policy that you care about and check whether it can be violated by an attacker's actions; specify a concrete design decision (allocation of functionality, component deployment, etc.,) and assess its security impact; or strengthen the system with a mitigation and observe how the attacker reformulates its strategy.
In this talk, I will present a demo of Poirot, a tool designed to assist developers in modeling and analyzing the security of their system during the design phase. With Poirot, you can specify your system and desired security policies, and perform an automatic analysis to generate attacks that may lead to the violation of a policy. The process is interactive; as you learn more about the system and its environment, you can modify the system model in Poirot and re-run the analysis to assess the impact of changes. Unlike existing modeling tools, where threats are treated as static entities, every threat in Poirot is represented by a dynamic agent that can actively perform actions and adapt to changes in a system. In addition, Poirot comes with a built-in, extensible database of threats that can be instantiated against a particular system, freeing you from the tedious task of enumerating a threat list. Finally, Poirot leverages recent progress in software verification to perform an exhaustive analysis that achieves a much stronger coverage than traditional testing. During this talk, I will demonstrate the application of Poirot to several web applications, and highlight the tool's strengths as well as limitations.
I am a PhD candidate and a member of the Software Design Group in the Computer Science and Artificial Intelligence Laboratory (CSAIL) at MIT. My research projects have focused on developing tools and techniques for software modeling and verification, with applications to security and safety-critical systems.