NPS logo Naval Postgraduate School
Dudley Knox Library
        View Item 
        •   Calhoun Home
        • Faculty and Researchers
        • Faculty and Researchers' Publications
        • View Item
        •   Calhoun Home
        • Faculty and Researchers
        • Faculty and Researchers' Publications
        • View Item
        • How to search in Calhoun
        • My Accounts
        • Ask a Librarian
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of CalhounCollectionsThis Collection

        My Account

        LoginRegister

        Statistics

        Most Popular ItemsStatistics by CountryMost Popular Authors

        Toward a Security Domain Model for Static Analysis and Verification of Information Systems

        Thumbnail
        Download
        Icon07paper_domainmodel.pdf (75.72Kb)
        Download Record
        Download to EndNote/RefMan (RIS)
        Download to BibTex
        Author
        Shaffer, Alan
        Auguston, Mikhail
        Irvine, Cynthia E.
        Levin, Tim.
        Date
        2007
        Metadata
        Show full item record
        Abstract
        Evaluation of high assurance secure computer systems requires that they be designed, developed, verified and tested using rigorous processes and formal methods. The evaluation process must include correspondence between security policy objectives, security specifications, and program implementation. This research presents an approach to the verification of programs represented in a specialized Implementation Modeling Language (IML) using a formal security Domain Model (DM). The DM is comprised of an invariant part, which defines the generic concepts of program state, information flow, and other security properties; and a variable part, specifying the behavior of the target program. The DM is written using the Alloy formal specification language, and its verification is accomplished using the Alloy Analyzer tool. It was found that, by separating the structural framework of the security policy from the semantics of the target program, efficiency of the Alloy Analyzer in detecting execution paths that violate the security properties specified in the DM is significantly improved.
        Description
        OOPSLA Workshop on Domain-Specific Modeling (DSM '07). Montreal, Canada.
        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.
        URI
        http://hdl.handle.net/10945/7151
        Collections
        • Center for Information Systems Security Studies and Research (CISR) Papers
        • Faculty and Researchers' Publications

        Related items

        Showing items related by title, author, creator and subject.

        • Thumbnail

          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 ...
        • Thumbnail

          Crowdsourced formal verification: a business case analysis toward a human-centered business model 

          Baur, Andreas (Monterey, California: Naval Postgraduate School, 2015);
          The DARPA project Crowd Sourced Formal Verification (CSFV) tries to investigate whether offering free games via the Internet that translate player’s actions into program annotations helps to overcome the challenges of the ...
        • Thumbnail

          Deploying crowd-sourced formal verification systems in a DoD network 

          Dumlupinar, Mahmut Firuz (Monterey, California: Naval Postgraduate School, 2013-09);
          Manual formal software verification is an expensive and time-consuming process. Military software is currently verified manually by highly skilled analysts. To reduce the high costs of the formal verification, DARPA started ...
        Feedback

        411 Dyer Rd. Bldg. 339
        Monterey, CA 93943

         

        circdesk@nps.edu
        (831) 656-2947
        DSN 756-2947

        Start Your Research

        • Research Guides
        • How to Cite
        • Search Basics
        • Ask a Librarian
        • Library Liaisons
        • Graduate Writing Center
        • Thesis Processing Office
        • Statistics, Maps & More
        • Copyright at NPS

        Find & Download

        • Databases List
        • Articles, Books & More
        • NPS Theses
        • NPS Faculty Publications: Calhoun
        • Journal Titles
        • Course Reserves

        Use the Library

        • My Accounts
        • Request Article or Book
        • Borrow, Renew, Return
        • Remote Access
        • Workshops & Tours
        • For Faculty & Researchers
        • For International Students
        • For Alumni
        • Print, Copy, Scan, Fax
        • Rooms & Study Spaces
        • Floor Map
        • Computers & Software
        • Adapters, Lockers & More

        Collections

        • NPS Archive: Calhoun
        • Restricted Resources
        • Special Collections & Archives
        • Federal Depository
        • Homeland Security Digital Library

        About

        • Hours
        • Library Staff
        • About Us
        • Visit Us

        NPS-Licensed Resources - Terms & Conditions

        Copyright Notice

         
         

          Federal Depository Library  

        NPS Home Privacy Policy Copyright Accessibility Contact Webmaster

        Export search results

        The export option will allow you to export the current search results of the entered query to a file. Different formats are available for download. To export the items, click on the button corresponding with the preferred download format.

        A logged-in user can export up to 15000 items. If you're not logged in, you can export no more than 500 items.

        To select a subset of the search results, click "Selective Export" button and make a selection of the items you want to export. The amount of items that can be exported at once is similarly restricted as the full export.

        After making a selection, click one of the export format buttons. The amount of items that will be exported is indicated in the bubble next to export format.

        Export citations

        Export the current results of the search query as a citation list. Select one of the available citation styles, or add a new one using the "Citations format" option present in the "My account" section.

        The list of citations that can be exported is limited to items.

        Export citations

        Export the current item as a citation. Select one of the available citation styles, or add a new one using the "Citations format" option present in the "My account" section.

        Export Citations