×

On refinement-closed security properties and nondeterministic compositions. (English) Zbl 1335.68179

Miller, Alice (ed.) et al., Proceedings of the 8th international workshop on automated verification of critical systems (AVoCS 2008), Glasgow, UK, September 30 – October 1, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 250, No. 2, 49-68 (2009).
Summary: 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.{ }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.
For the entire collection see [Zbl 1281.68035].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68M12 Network protocols
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
94A60 Cryptography

Software:

FDR2
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Alur, R.; Cerný, P.; Zdancewic, S. A., Preserving secrecy under refinement, (Proceedings of the 33rd International Colloquium on Automata, Languages and Programming. Proceedings of the 33rd International Colloquium on Automata, Languages and Programming, LNCS, 4052 (2006)), 107-118 · Zbl 1133.94307
[2] Bossi, A., R. Focardi, C. Piazza and S. Rossi, Refinement operators and information flow securityProceedings of the IEEE International Conference on Software Engineering and Formal Methods (SEFM’03); Bossi, A., R. Focardi, C. Piazza and S. Rossi, Refinement operators and information flow securityProceedings of the IEEE International Conference on Software Engineering and Formal Methods (SEFM’03) · Zbl 1278.68158
[3] Bryans, J., Reasoning about XACML policies using CSPSWS ’05: Proceedings of the 2005 workshop on Secure web services; Bryans, J., Reasoning about XACML policies using CSPSWS ’05: Proceedings of the 2005 workshop on Secure web services
[4] Formal Systems (Europe) Limited, “Failures Divergences Refinement: FDR2 User Manual,” (2005), available at: http://www.fsel.com/documentation/fdr2/fdr2manual.ps; Formal Systems (Europe) Limited, “Failures Divergences Refinement: FDR2 User Manual,” (2005), available at: http://www.fsel.com/documentation/fdr2/fdr2manual.ps
[5] Langerak, R., E. Brinksma and J.-P. Katoen, Causal ambiguity and partial orders in event structuresProceedings of the 8th International Conference on Concurrency Theory (CONCUR ’97); Langerak, R., E. Brinksma and J.-P. Katoen, Causal ambiguity and partial orders in event structuresProceedings of the 8th International Conference on Concurrency Theory (CONCUR ’97)
[6] Lowe, G., On CSP refinement tests that run multiple copies of a processProceedings of the Seventh International Workshop on Automated Verification of Critical Systems, AVoCS ’07; Lowe, G., On CSP refinement tests that run multiple copies of a processProceedings of the Seventh International Workshop on Automated Verification of Critical Systems, AVoCS ’07 · Zbl 1339.68169
[7] Lowe, G., On information flow and refinement-closureProceedings of the Workshop on Issues in the Theory of Security (WITS ’07); Lowe, G., On information flow and refinement-closureProceedings of the Workshop on Issues in the Theory of Security (WITS ’07)
[8] Mantel, H., Preserving information flow properties under refinementProceedings of the 2001 IEEE Symposium on Security and Privacy; Mantel, H., Preserving information flow properties under refinementProceedings of the 2001 IEEE Symposium on Security and Privacy
[9] Murray, T., Analysing object-capability securityProceedings of the Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS’08); Murray, T., Analysing object-capability securityProceedings of the Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS’08)
[10] Murray, T. and G. Lowe, Authority analysis for least privilege environmentsProceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA’07); Murray, T. and G. Lowe, Authority analysis for least privilege environmentsProceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA’07)
[11] MyThS, Models of information flow based on non-interleaving, causal models of concurrency (2005), available at:
[12] Roscoe, A. and L. Wulf, Composing and decomposing systems under security propertiesProceedings of the Eighth IEEE Computer Security Foundations Workshop; Roscoe, A. and L. Wulf, Composing and decomposing systems under security propertiesProceedings of the Eighth IEEE Computer Security Foundations Workshop
[13] Roscoe, A. W., The Theory and Practice of Concurrency (1997), Prentice Hall: Prentice Hall Upper Saddle River, NJ, USA
[14] Ryan, P.; Schneider, S.; Goldsmith, M.; Lowe, G.; Roscoe, B., Modelling and Analysis of Security Protocols: the CSP Approach (2000), Addison Wesley
[15] van Glabbeek, R. and F. Vaandrager, Bundle event structures and CCSPProceedings of the 14th International Conference on Concurrency Theory (CONCUR ’03); van Glabbeek, R. and F. Vaandrager, Bundle event structures and CCSPProceedings of the 14th International Conference on Concurrency Theory (CONCUR ’03) · Zbl 1274.68262
[16] Winskel, G., An introduction to event structuresREX School of Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency; Winskel, G., An introduction to event structuresREX School of Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.