A formal domain-specific model for security, using the Alloy specification language and Alloy Analyzer tool, as a means of conducting automated static analysis of software programs for adherence to a security policy. See above website for access to multiple Alloy models used during our testing.