A Security Domain Model for Static Analysis and Verification of Software Programs
Shaffer, Alan B.
MetadataShow full item record
Unauthorized information flows can result from malicious software exploiting covert channels and overt flaws in access control design. To address this problem, we present a precise, formal definition for information flow that relies on control flow dependency tracing through program execution, and extends Dennings’ and follow-on classic work in secure information flow . We describe a formal security Domain Model (DM) for conducting static analysis of programs to identify illicit information flows, access control flaws and covert channel vulnerabilities. The DM is comprised of an Invariant Model, which defines the generic concepts of program state, information flow, and security policy rules; and an Implementation Model, which specifies the behavior of a target program. The DM is compiled from a representation of the program, written in a domain-specific Implementation Modeling Language (IML), and a specification of the security policy written in Alloy. The Alloy Analyzer tool is used to perform static analysis of the DM to automatically detect potential covert channel vulnerabilities and security policy violations in the target program.
RightsThis publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Showing items related by title, author, creator and subject.
Naval Postgraduate School Center for Homeland Defense and Security (CHDS) (Monterey, California. Naval Postgraduate SchoolCenter for Homeland Defense and Security, 2010-05);May 2010. Academic homeland security programs have proliferated in the past eight years, with more than 270 colleges and universities in the United States offering certificates and degrees in homeland security and related ...
An application of Alloy to static analysis for secure information flow and verification of software systems Shaffer, Alan B. (Monterey, California. Naval Postgraduate School, 2008., 2008-12);Within a multilevel secure (MLS) system, flaws in design and implementation can result in overt and covert channels, both of which may be exploited by malicious software to cause unauthorized information flows. To address ...
Naval Postgraduate School (U.S.); Meyer Institute; NPS Maritime Defense and Security Research Program (MDP-TF) (Monterey, California. Naval Postgraduate SchoolMaritime Defense and Security Research Program, 2004-07);"Recent events have highlighted the importance and necessity of developing Maritime Domain Protection (MDP) and homeland security. Essential components of this development include the evolution of new doctrine, capabilities, ...