Within a Multi-Level Secure (MLS) system, trusted subjects are granted privileges to perform operations that are not possible by ordinary subjects controlled by Mandatory Access Control (MAC) policy enforcement mechanisms. These subjects are trusted not to conduct malicious activity or degrade system security. The authors present a formal definition for trusted subject behaviors, which depends upon a representation of information flow and control dependencies generated during a program execution. They describe a security Domain Model (DM) designed in the alloy specification language for conducting static analysis of programs to identify illicit information flows, access control flaws and covert channel vulnerabilities.