×

zbMATH — the first resource for mathematics

On integrating confidentiality and functionality in a formal method. (English) Zbl 1342.68191
Summary: This paper proposes a formal method, based on Circus, for developing software systems that respect a joint specification of functionality and confidentiality attributes. We extend the semantics of Circus to capture the information that users can infer about a system’s behaviour, enabling confidentiality and functionality attributes of a system to be specified together. We represent inconsistencies between functionality and confidentiality properties as miracles, rendering insecure functionality infeasible. We present techniques for verifying that a system design’s functionality and confidentiality attributes are mutually consistent, and for ensuring that consistency is maintained by refinement steps.

MSC:
68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Circus; Z
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, New York · Zbl 0915.68015
[2] Banks MJ (2012) On confidentiality and formal methods. PhD thesis, Department of Computer Science, University of York, UK · Zbl 1093.68555
[3] Bresciani R, Butterfield A (2011) Towards a UTP-style framework to deal with probabilities. Technical report, Foundations and Methods Group, Trinity College Dublin, Dublin, Ireland · Zbl 1146.68401
[4] Boyd CA, Mathuria A (2003) Protocols for Authentication and key establishment. Information security and cryptography. Springer, Berlin · Zbl 1043.68014
[5] Clark, JA; Stepney, S; Chivers, H, Breaking the model: finalisation and a taxonomy of security attacks, Electron Notes Theor Comput Sci, 137, 225-242, (2005)
[6] Cavalcanti, A; Sampaio, A; Woodcock, J, A refinement strategy for circus, Form Asp Comput, 15, 146-181, (2003) · Zbl 1093.68555
[7] Cavalcanti, ALC; Woodcock, JCP, Predicate transformers in the semantics of circus, IEE Proc Softw, 150, 85-94, (2003)
[8] Cavalcanti A, Woodcock J (2006) A tutorial introduction to CSP in unifying theories of programming. In: Refinement techniques in software engineering. Lecture notes in computer science, vol 3167. Springer, Berlin, pp 220-268
[9] Dijkstra EW (1976) A discipline of programming. Prentice-Hall series in automatic computation. Prentice-Hall, Inc., Englewood Cliffs, New Jersey · Zbl 1242.68071
[10] Dijkstra EW, Scholten CS (1990) Predicate calculus and program semantics. Texts and monographs in computer science. Springer, New York · Zbl 0698.68011
[11] Goguen JA, Meseguer J (1982) Security policies and security models. In: Proceedings of the 1982 IEEE symposium on security and privacy. IEEE Computer Society, pp 11-20 · Zbl 1178.68166
[12] Goguen JA, Meseguer J (1984) Unwinding and inference control. In: Proceedings of the 1984 IEEE symposium on security and privacy. IEEE Computer Society, pp 75-86
[13] Hoare CAR, He J (1998) Unifying theories of programming. Prentice Hall international series in computer science. Prentice Hall Inc., New York
[14] He J, Hoare CAR, Sanders JW (1986) Data refinement refined (resumé). In: Robinet B, Wilhelm R (eds) ESOP’86: Proceedings of the European symposium on programming. Lecture notes in computer science, vol 213. Springer, Berlin pp 187-196
[15] Hoare CAR (1985) Communicating sequential processes. Prentice Hall international series in computer science. Prentice Hall Inc., New York · Zbl 0637.68007
[16] ISO (2002) Information technology—Z formal specification notation —syntax, type system and semantics. Technical Report ISO/IEC 13568, International Organization for Standardization
[17] Jacob JL (1989) On the derivation of secure components. In: Proceedings of the 1989 IEEE symposium on security and privacy. IEEE Computer Society, pp 242-247
[18] Jacob, JL, Basic theorems about security, J Comput Secur, 1, 385-411, (1992)
[19] Jones CB (1990) Systematic software development using VDM, 2nd edn. Prentice-Hall Inc., Upper Saddle River · Zbl 0743.68048
[20] Mantel H (2000) Unwinding possibilistic security properties. In: Computer Security—ESORICS 2000. Lecture notes in computer science, vol 1895. Springer, Berlin, pp 238-254
[21] McLean J (1987) Reasoning about security models. In: Proceedings of the 1987 IEEE symposium on security and privacy, IEEE Computer Society Press, pp 123-131
[22] Morgan C (1994) Programming from specifications. Prentice Hall international series in computer science, 2nd edn. Prentice Hall Inc., Hertfordshire
[23] Morgan, C, The shadow knows: refinement and security in sequential programs, Sci Comput Program, 74, 629-653, (2009) · Zbl 1178.68166
[24] Morgan, C, Compositional noninterference from first principles, Form Asp Comput, 24, 3-26, (2012) · Zbl 1242.68071
[25] Nelson, G, A generalization of dijkstra’s calculus, ACM Trans Program Lang Syst, 11, 517-561, (1989)
[26] Oliveira, M; Cavalcanti, A; Woodcock, J, A UTP semantics for circus, Form Asp Comput, 21, 3-32, (2009) · Zbl 1165.68048
[27] O’Halloran C (1990) A calculus of information flow. In: ESORICS 90—first European symposium on research in computer security, AFCET, pp 147-159
[28] Oliveira MV (2005) Formal derivation of state-rich reactive programs using Circus. PhD thesis, Department of Computer Science, University of York
[29] Roscoe AW (1995) CSP and determinism in security modelling. In: Proceedings of the 1995 IEEE symposium on security and privacy. IEEE Computer Society, pp 114-127
[30] Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall PTR, Upper Saddle River
[31] Ryan P, Schneider SA (1999) Process algebra and non-interference. In: 12th IEEE computer security Foundations Workshop (CSFW’99), IEEE Computer Society, pp 214-227 · Zbl 1242.68071
[32] Ryan P (2001) Mathematical models of computer security. In: Foundations of security analysis and design. Lecture notes in computer science, vol 2171. Springer, Berlin, pp 1-62 · Zbl 1007.68129
[33] Saiedian, H, An invitation to formal methods, Computer, 29, 16-17, (1996)
[34] Santen, T, Preservation of probabilistic information flow under refinement, Inf Comput, 206, 213-249, (2008) · Zbl 1146.68401
[35] Shannon, CE, Communication theory of secrecy systems, Bell Syst Tech J, 28, 656-715, (1949) · Zbl 1200.94005
[36] Woodcock J, Cavalcanti A (2002) The semantics of Circus. In: ZB 2002: formal specification and development in Z and B. Lecture notes in computer science, vol 2272, chap 10. Springer, Berlin, pp 184-203 · Zbl 1044.68560
[37] Woodcock J, Cavalcanti A (2004) A tutorial introduction to designs in Unifying Theories of Programming. In: Integrated formal methods. Lecture notes in computer science, vol 2999. Springer Berlin, pp 40-66 · Zbl 1196.68031
[38] Woodcock J, Davies J (1996) Using Z: specification, refinement, and proof. Prentice Hall international series in computer science. Prentice Hall, New York · Zbl 0855.68060
[39] Wing JM (1998) A symbiotic relationship between formal methods and security. In: Conference on computer security, dependability, and assurance: from needs to solutions. IEEE Computer Society, pp 26-38
[40] Woodcock, J; Larsen, PG; Bicarregui, J; Fitzgerald, J, Formal methods: practice and experience, ACM Comput Surv, 41, 1-36, (2009)
[41] Woodcock J (2010) The miracle of reactive programming. In: Butterfield A (ed) Unifying theories of programming. Lecture notes in computer science, vol 5713, chap 12. Springer, Berlin, pp 202-217 · Zbl 1286.68096
[42] Wei K, Woodcock J, Burns A (2011) Timed Circus: timed CSP with the miracle. In: 2011 16th IEEE international conference on engineering of complex computer systems (ICECCS). IEEE, April, pp 55-64
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.