The Security PAttern ChEcker
SPACE is a specification-free tool for finding missing security checks in Ruby on Rails web applications using a catalog of access control patterns in which each pattern models a common access control use case. SPACE checks that for every kind of data exposure allowed by an application's code, some security pattern in our catalog also allows the exposure. The user provides a mapping from application types to the types of our catalog, and then SPACE identifies security bugs automatically.
A preliminary version of SPACE is available here. This archive contains a modified version of Derailer that produces exposures suitable for comparison to our pattern catalog, along with the constraint specializer for producing Alloy constraints.