A Security Domain Model for Static Analysis and Verification of Software Programs
Abstract
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 [7][19][27]. 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.
Rights
This 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.Collections
Related items
Showing items related by title, author, creator and subject.
-
Homeland Security Affairs Journal, Volume VI - 2010: Issue 2, May
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 ... -
SITREP: The NPS Maritime Defense and Security Research Program Newsletter ; v. 6 (July 2004)
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, ...