Verifying information flow goals in Security-Enhanced Linux

In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transiti...

Full description

Saved in:
Bibliographic Details
Published in:Journal of computer security 2005-01, Vol.13 (1), p.115-134
Main Authors: Guttman, Joshua D., Herzog, Amy L., Ramsdell, John D., Skorupka, Clement W.
Format: Article
Language:English
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c310t-5414f7081b995d7d4375cd606747b408f8fc0393a34433332076981d6c55e58c3
cites
container_end_page 134
container_issue 1
container_start_page 115
container_title Journal of computer security
container_volume 13
creator Guttman, Joshua D.
Herzog, Amy L.
Ramsdell, John D.
Skorupka, Clement W.
description In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an SELinux configuration, provides our framework. Information flow security goal statements expressed in linear temporal logic provide a clear description of the objectives that SELinux is intended to achieve. We use model checking to determine whether security goals hold in a given system. These formal models combined with appropriate algorithms have led to automated tools for the verification of security properties in an SELinux system. Our approach has been used in other security management contexts over the past decade, under the name rigorous automated security management.
doi_str_mv 10.3233/JCS-2005-13105
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_miscellaneous_29091399</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>29091399</sourcerecordid><originalsourceid>FETCH-LOGICAL-c310t-5414f7081b995d7d4375cd606747b408f8fc0393a34433332076981d6c55e58c3</originalsourceid><addsrcrecordid>eNotkEtLAzEUhYMoWKtb17Nyl3rzmiS4kqG-KLioirswzSQ1Ms3UZAbtv3dqvZsDl4_D4UPoksCMUcaun6olpgACE0ZAHKEJUVJgpSk_RhPQtMSUyvdTdJbzJwAlRKsJunlzKfhdiOsiRN-lTd2HLha-7b6LdVe3eXwXS2eHFPodnsePOlrXFIsQh59zdOJHwl385xS93s1fqge8eL5_rG4X2I5Deiw44V6CIiutRSMbzqSwTQml5HLFQXnlLTDNasY5G4-CLLUiTWmFcEJZNkVXh95t6r4Gl3uzCdm6tq2j64ZsqAZNmNYjODuANnU5J-fNNoVNnXaGgNk7MqMjs3dk_hyxXx21V9A</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>29091399</pqid></control><display><type>article</type><title>Verifying information flow goals in Security-Enhanced Linux</title><source>EBSCOhost Business Source Ultimate</source><creator>Guttman, Joshua D. ; Herzog, Amy L. ; Ramsdell, John D. ; Skorupka, Clement W.</creator><contributor>Gorrieri, Roberto</contributor><creatorcontrib>Guttman, Joshua D. ; Herzog, Amy L. ; Ramsdell, John D. ; Skorupka, Clement W. ; Gorrieri, Roberto</creatorcontrib><description>In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an SELinux configuration, provides our framework. Information flow security goal statements expressed in linear temporal logic provide a clear description of the objectives that SELinux is intended to achieve. We use model checking to determine whether security goals hold in a given system. These formal models combined with appropriate algorithms have led to automated tools for the verification of security properties in an SELinux system. Our approach has been used in other security management contexts over the past decade, under the name rigorous automated security management.</description><identifier>ISSN: 0926-227X</identifier><identifier>EISSN: 1875-8924</identifier><identifier>DOI: 10.3233/JCS-2005-13105</identifier><language>eng</language><ispartof>Journal of computer security, 2005-01, Vol.13 (1), p.115-134</ispartof><lds50>peer_reviewed</lds50><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c310t-5414f7081b995d7d4375cd606747b408f8fc0393a34433332076981d6c55e58c3</citedby></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><contributor>Gorrieri, Roberto</contributor><creatorcontrib>Guttman, Joshua D.</creatorcontrib><creatorcontrib>Herzog, Amy L.</creatorcontrib><creatorcontrib>Ramsdell, John D.</creatorcontrib><creatorcontrib>Skorupka, Clement W.</creatorcontrib><title>Verifying information flow goals in Security-Enhanced Linux</title><title>Journal of computer security</title><description>In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an SELinux configuration, provides our framework. Information flow security goal statements expressed in linear temporal logic provide a clear description of the objectives that SELinux is intended to achieve. We use model checking to determine whether security goals hold in a given system. These formal models combined with appropriate algorithms have led to automated tools for the verification of security properties in an SELinux system. Our approach has been used in other security management contexts over the past decade, under the name rigorous automated security management.</description><issn>0926-227X</issn><issn>1875-8924</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2005</creationdate><recordtype>article</recordtype><recordid>eNotkEtLAzEUhYMoWKtb17Nyl3rzmiS4kqG-KLioirswzSQ1Ms3UZAbtv3dqvZsDl4_D4UPoksCMUcaun6olpgACE0ZAHKEJUVJgpSk_RhPQtMSUyvdTdJbzJwAlRKsJunlzKfhdiOsiRN-lTd2HLha-7b6LdVe3eXwXS2eHFPodnsePOlrXFIsQh59zdOJHwl385xS93s1fqge8eL5_rG4X2I5Deiw44V6CIiutRSMbzqSwTQml5HLFQXnlLTDNasY5G4-CLLUiTWmFcEJZNkVXh95t6r4Gl3uzCdm6tq2j64ZsqAZNmNYjODuANnU5J-fNNoVNnXaGgNk7MqMjs3dk_hyxXx21V9A</recordid><startdate>20050101</startdate><enddate>20050101</enddate><creator>Guttman, Joshua D.</creator><creator>Herzog, Amy L.</creator><creator>Ramsdell, John D.</creator><creator>Skorupka, Clement W.</creator><scope>AAYXX</scope><scope>CITATION</scope><scope>7SC</scope><scope>8FD</scope><scope>JQ2</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope></search><sort><creationdate>20050101</creationdate><title>Verifying information flow goals in Security-Enhanced Linux</title><author>Guttman, Joshua D. ; Herzog, Amy L. ; Ramsdell, John D. ; Skorupka, Clement W.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c310t-5414f7081b995d7d4375cd606747b408f8fc0393a34433332076981d6c55e58c3</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2005</creationdate><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Guttman, Joshua D.</creatorcontrib><creatorcontrib>Herzog, Amy L.</creatorcontrib><creatorcontrib>Ramsdell, John D.</creatorcontrib><creatorcontrib>Skorupka, Clement W.</creatorcontrib><collection>CrossRef</collection><collection>Computer and Information Systems Abstracts</collection><collection>Technology Research Database</collection><collection>ProQuest Computer Science Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><jtitle>Journal of computer security</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Guttman, Joshua D.</au><au>Herzog, Amy L.</au><au>Ramsdell, John D.</au><au>Skorupka, Clement W.</au><au>Gorrieri, Roberto</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Verifying information flow goals in Security-Enhanced Linux</atitle><jtitle>Journal of computer security</jtitle><date>2005-01-01</date><risdate>2005</risdate><volume>13</volume><issue>1</issue><spage>115</spage><epage>134</epage><pages>115-134</pages><issn>0926-227X</issn><eissn>1875-8924</eissn><abstract>In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux security server, together with a labeled transition system representing an SELinux configuration, provides our framework. Information flow security goal statements expressed in linear temporal logic provide a clear description of the objectives that SELinux is intended to achieve. We use model checking to determine whether security goals hold in a given system. These formal models combined with appropriate algorithms have led to automated tools for the verification of security properties in an SELinux system. Our approach has been used in other security management contexts over the past decade, under the name rigorous automated security management.</abstract><doi>10.3233/JCS-2005-13105</doi><tpages>20</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 0926-227X
ispartof Journal of computer security, 2005-01, Vol.13 (1), p.115-134
issn 0926-227X
1875-8924
language eng
recordid cdi_proquest_miscellaneous_29091399
source EBSCOhost Business Source Ultimate
title Verifying information flow goals in Security-Enhanced Linux
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-30T20%3A29%3A35IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Verifying%20information%20flow%20goals%20in%20Security-Enhanced%20Linux&rft.jtitle=Journal%20of%20computer%20security&rft.au=Guttman,%20Joshua%20D.&rft.date=2005-01-01&rft.volume=13&rft.issue=1&rft.spage=115&rft.epage=134&rft.pages=115-134&rft.issn=0926-227X&rft.eissn=1875-8924&rft_id=info:doi/10.3233/JCS-2005-13105&rft_dat=%3Cproquest_cross%3E29091399%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c310t-5414f7081b995d7d4375cd606747b408f8fc0393a34433332076981d6c55e58c3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=29091399&rft_id=info:pmid/&rfr_iscdi=true