File:An application of Alloy to static analysis for secure information flow and verification of software systems (IA anpplicationofal1094510320).pdf
Original file (1,275 × 1,650 pixels, file size: 804 KB, MIME type: application/pdf, 183 pages)
Captions
Summary[edit]
An application of Alloy to static analysis for secure information flow and verification of software systems ( ) | ||
---|---|---|
Author |
Shaffer, Alan B. |
|
Title |
An application of Alloy to static analysis for secure information flow and verification of software systems |
|
Publisher |
Monterey, California. Naval Postgraduate School, 2008. |
|
Description |
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 this problem, the use of control dependency tracing has been explored to present a precise, formal definition for information flow. This work describes a security Domain Model (DM), designed in the Alloy formal specification language, for conducting static analysis of programs to identify illicit information flows, such as control dependency flaws and covert channel vulnerabilities. The model includes a formal definition for trusted subjects, which are granted extraordinary privileges to perform system operations that require relaxation of the mandatory access control (MAC) policy mechanisms imposed on normal subjects, but are trusted to behave benignly and not to degrade system security. The DM defines the concepts of program state, information flow and security policy rules, and specifies the behavior of a target program. The DM is compiled from a representation of the target program, written in a specialized Implementation Modeling Language (IML), and a specification of the security policy written in the Alloy language. The Alloy Analyzer tool is used to perform static analysis of the DM to detect potential security policy violations in the target program. This approach demonstrates that it is possible to establish a framework for formally representing a program implementation and for formalizing the security rules defined by a security policy, enabling the verification of that program representation for adherence to the security policy. Subjects: Computer software; Verification.; Security domain model; static analysis; automated program verification; trusted subjects; covert channels; dynamic slicing; specification language |
|
Language | English | |
Publication date | December 2008 | |
Current location |
IA Collections: navalpostgraduateschoollibrary; fedlink |
|
Accession number |
anpplicationofal1094510320 |
|
Source | ||
Permission (Reusing this file) |
Approved for public release, distribution unlimited |
Licensing[edit]
Public domainPublic domainfalsefalse |
This file is a work of a sailor or employee of the U.S. Navy, taken or made as part of that person's official duties. As a work of the U.S. federal government, it is in the public domain in the United States.
|
||
This file has been identified as being free of known restrictions under copyright law, including all related and neighboring rights. |
https://creativecommons.org/publicdomain/mark/1.0/PDMCreative Commons Public Domain Mark 1.0falsefalse
File history
Click on a date/time to view the file as it appeared at that time.
Date/Time | Thumbnail | Dimensions | User | Comment | |
---|---|---|---|---|---|
current | 15:27, 14 July 2020 | 1,275 × 1,650, 183 pages (804 KB) | Fæ (talk | contribs) | FEDLINK - United States Federal Collection anpplicationofal1094510320 (User talk:Fæ/IA books#Fork8) (batch 1993-2020 #7736) |
You cannot overwrite this file.
File usage on Commons
The following page uses this file:
Metadata
This file contains additional information such as Exif metadata which may have been added by the digital camera, scanner, or software program used to create or digitize it. If the file has been modified from its original state, some details such as the timestamp may not fully reflect those of the original file. The timestamp is only as accurate as the clock in the camera, and it may be completely wrong.
Short title |
|
---|---|
Author | Pam Silva |
Software used | PScript5.dll Version 5.2 |
File change date and time | 08:39, 20 January 2009 |
Date and time of digitizing | 04:16, 7 December 2008 |
Date metadata was last modified | 08:39, 20 January 2009 |
Conversion program | Acrobat Distiller 8.1.0 (Windows) |
Encrypted | no |
Page size | 612 x 792 pts (letter) |
Version of PDF format | 1.4 |