On Refinement−Closed Security Properties and Nondeterministic Compositions
<p> Refinement-closed security properties allow the verification of systems for all possible implementations. Some systems, however, have refinements that do not represent possible implementations. In particular, real instantiations of abstract systems comprising security-critical components s...
| Автори: | , |
|---|---|
| Формат: | Conference item |
| Опубліковано: |
2009
|
| _version_ | 1826306146826190848 |
|---|---|
| author | Murray, T Lowe, G |
| author_facet | Murray, T Lowe, G |
| author_sort | Murray, T |
| collection | OXFORD |
| description | <p> Refinement-closed security properties allow the verification of systems for all possible implementations. Some systems, however, have refinements that do not represent possible implementations. In particular, real instantiations of abstract systems comprising security-critical components surrounded by maximally hostile unrefined components are often characterised only by compositions of refinements of the abstract system's components, rather than all refinements of the abstract system. In this case, refinement-closed security properties that examine multiple behaviours of a system at once can be falsely violated by the presence of inconsistent pairs of behaviour arising from different, incompatible refinements of the system's components. </p> <p> We show how to weaken a class of such properties, which includes both information flow and causation properties, to allow them to be applied to these sorts of abstract systems. The weakened properties ignore all pairs of inconsistent behaviour that would have violated the original property from which they are derived. We also show how to adapt existing automated tests for these properties to allow them to be used to test for their weakened counterparts instead. This enables greater flexibility in the application of these sorts of properties to compositions of nondeterministic components. </p> |
| first_indexed | 2024-03-07T06:43:31Z |
| format | Conference item |
| id | oxford-uuid:fa19b10b-a133-4031-a93f-aaf45c4bf20b |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:43:31Z |
| publishDate | 2009 |
| record_format | dspace |
| spelling | oxford-uuid:fa19b10b-a133-4031-a93f-aaf45c4bf20b2022-03-27T13:03:03ZOn Refinement−Closed Security Properties and Nondeterministic CompositionsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:fa19b10b-a133-4031-a93f-aaf45c4bf20bDepartment of Computer Science2009Murray, TLowe, G<p> Refinement-closed security properties allow the verification of systems for all possible implementations. Some systems, however, have refinements that do not represent possible implementations. In particular, real instantiations of abstract systems comprising security-critical components surrounded by maximally hostile unrefined components are often characterised only by compositions of refinements of the abstract system's components, rather than all refinements of the abstract system. In this case, refinement-closed security properties that examine multiple behaviours of a system at once can be falsely violated by the presence of inconsistent pairs of behaviour arising from different, incompatible refinements of the system's components. </p> <p> We show how to weaken a class of such properties, which includes both information flow and causation properties, to allow them to be applied to these sorts of abstract systems. The weakened properties ignore all pairs of inconsistent behaviour that would have violated the original property from which they are derived. We also show how to adapt existing automated tests for these properties to allow them to be used to test for their weakened counterparts instead. This enables greater flexibility in the application of these sorts of properties to compositions of nondeterministic components. </p> |
| spellingShingle | Murray, T Lowe, G On Refinement−Closed Security Properties and Nondeterministic Compositions |
| title | On Refinement−Closed Security Properties and Nondeterministic Compositions |
| title_full | On Refinement−Closed Security Properties and Nondeterministic Compositions |
| title_fullStr | On Refinement−Closed Security Properties and Nondeterministic Compositions |
| title_full_unstemmed | On Refinement−Closed Security Properties and Nondeterministic Compositions |
| title_short | On Refinement−Closed Security Properties and Nondeterministic Compositions |
| title_sort | on refinement closed security properties and nondeterministic compositions |
| work_keys_str_mv | AT murrayt onrefinementclosedsecuritypropertiesandnondeterministiccompositions AT loweg onrefinementclosedsecuritypropertiesandnondeterministiccompositions |