research-article

Open access

On integrating confidentiality and functionality in a formal method

Authors:

Michael J. Banks,

Jeremy L. JacobAuthors Info & Claims

Formal Aspects of Computing, Volume 26, Issue 5

Pages 963 - 992

https://doi.org/10.1007/s00165-013-0285-4

Published: 01 September 2014 Publication History

PDF eReader

Abstract

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.

References

[1]

Abrial J-R The B-book: assigning programs to meanings 1996 New York Cambridge University Press

Crossref

Google Scholar

[2]

Banks MJ (2012) On confidentiality and formal methods. PhD thesis, Department of Computer Science, University of York, UK

Google Scholar

[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

Google Scholar

[4]

Boyd CA, Mathuria A (2003) Protocols for Authentication and key establishment. Information security and cryptography. Springer, Berlin

Google Scholar

[5]

Clark JA, Stepney S, and Chivers H Breaking the model: finalisation and a taxonomy of security attacks Electron Notes Theor Comput Sci 2005 137 2 225-242

Digital Library

Google Scholar

[6]

Cavalcanti A, Sampaio A, and Woodcock J A refinement strategy for Circus Form Asp Comput 2003 15 2–3 146-181

Digital Library

Google Scholar

[7]

Cavalcanti ALC and Woodcock JCP Predicate transformers in the semantics of Circus IEE Proc Softw 2003 150 2 85-94

Crossref

Google Scholar

[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

Google Scholar

[9]

Dijkstra EW (1976) A discipline of programming. Prentice-Hall series in automatic computation. Prentice-Hall, Inc., Englewood Cliffs, New Jersey

Google Scholar

[10]

Dijkstra EW and Scholten CS Predicate calculus and program semantics 1990 New York Texts and monographs in computer science. Springer

Crossref

Google Scholar

[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

Google Scholar

[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

Google Scholar

[13]

Hoare CAR and He J Unifying theories of programming 1998 New York Prentice Hall international series in computer science. Prentice Hall Inc.

Google Scholar

[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

Google Scholar

[15]

Hoare CAR Communicating sequential processes 1985 New York Prentice Hall international series in computer science. Prentice Hall Inc.

Digital Library

Google Scholar

[16]

ISO (2002) Information technology—Z formal specification notation —syntax, type system and semantics. Technical Report ISO/IEC 13568, International Organization for Standardization

Google Scholar

[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

Google Scholar

[18]

Jacob JL Basic theorems about security J Comput Secur 1992 1 4 385-411

Digital Library

Google Scholar

[19]

Jones CB Systematic software development using VDM 1990 2 Upper Saddle River Prentice-Hall Inc.

Digital Library

Google Scholar

[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

Google Scholar

[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

Google Scholar

[22]

Morgan C (1994) Programming from specifications. Prentice Hall international series in computer science, 2nd edn. Prentice Hall Inc., Hertfordshire

Google Scholar

[23]

Morgan C The shadow knows: refinement and security in sequential programs Sci Comput Program 2009 74 8 629-653

Digital Library

Google Scholar

[24]

Morgan C Compositional noninterference from first principles Form Asp Comput 2012 24 1 3-26

Digital Library

Google Scholar

[25]

Nelson G A generalization of Dijkstra’s calculus ACM Trans Program Lang Syst 1989 11 4 517-561

Digital Library

Google Scholar

[26]

Oliveira M, Cavalcanti A, and Woodcock J A UTP semantics for Circus Form Asp Comput 2009 21 1 3-32

Digital Library

Google Scholar

[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

Google Scholar

[28]

Oliveira MV (2005) Formal derivation of state-rich reactive programs using Circus. PhD thesis, Department of Computer Science, University of York

Google Scholar

[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

Google Scholar

[30]

Roscoe AW The theory and practice of concurrency 1997 Upper Saddle River Prentice Hall PTR

Digital Library

Google Scholar

[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

Google Scholar

[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

Google Scholar

[33]

Saiedian H An invitation to formal methods Computer 1996 29 4 16-17

Digital Library

Google Scholar

[34]

Santen T Preservation of probabilistic information flow under refinement Inf Comput 2008 206 2–4 213-249

Digital Library

Google Scholar

[35]

Shannon CE Communication theory of secrecy systems Bell Syst Tech J 1949 28 4 656-715

Crossref

Google Scholar

[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

Google Scholar

[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

Google Scholar

[38]

Woodcock J and Davies J Using Z: specification, refinement, and proof 1996 New York Prentice Hall international series in computer science. Prentice Hall

Digital Library

Google Scholar

[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

Google Scholar

[40]

Woodcock J, Larsen PG, Bicarregui J, and Fitzgerald J Formal methods: practice and experience ACM Comput Surv 2009 41 4 1-36

Digital Library

Google Scholar

[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

Google Scholar

[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

Google Scholar

Cited By

View all

Naumann DNgo M(2019)Whither Specifications as ProgramsUnifying Theories of Programming10.1007/978-3-030-31038-7_3(39-61)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-31038-7_3
Boiten EJacob J(2014)Sealed Containers in ZProceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 847710.1007/978-3-662-43652-3_12(136-141)Online publication date: 2-Jun-2014
https://dl.acm.org/doi/10.1007/978-3-662-43652-3_12

Index Terms

On integrating confidentiality and functionality in a formal method

Index terms have been assigned to the content through auto-classification.

Recommendations

Specifying confidentiality in circus
FM'11: Proceedings of the 17th international conference on Formal methods

This paper presents an approach for extending the Circus formalism to accommodate information flow security concerns. Working with the semantics of Circus, we introduce a notation for specifying which aspects of Circus processes are confidential and ...
Formal methods for security in the Xenon hypervisor

This paper reports on the Xenon project's use of formal methods. Xenon is a higher-assurance secure hypervisor based on re-engineering the Xen open-source hypervisor. The Xenon project used formal specifications both for assurance and as guides for ...
Unifying theories of confidentiality
UTP'10: Proceedings of the Third international conference on Unifying theories of programming

This paper presents a framework for reasoning about the security of confidential data within software systems. A novelty is that we use Hoare and He's Unifying Theories of Programming (UTP) to do so and derive advantage from this choice. We identify how ...

Reviews

Reviewer: Goran Trajkovski

Miracles happen and are now formalized. Moreover, they can exist in formal methods where functionality and confidentiality of systems coexist in efforts to build secure systems by design. Functionality and confidentially have so far been irreconcilable attributes in formal systems. In Banks and Jacob's paper, inconsistencies between confidentiality and functionality are referred to as miracles. The formal techniques they present aim at "verifying that a system design's functionality and confidentiality attributes are mutually consistent, and for ensuring that consistency is maintained by refinement steps." The formal method is based on the Circus formalism and can be easily extended to any formal methods within this family. While functionality in formal methods is of predominant concern, confidentiality is emphasized here. The paper shows how confidentiality can be highlighted and coexist with functionality, and be verifiable. Circus is elevated to accommodate for the inferences of adversarial users. What do we get at the end__?__ We get an approach where refinement steps do not compromise the feasibility of a process design. Now software can be developed to be secure without deep knowledge of security. While no tool exists yet to support this approach, the moment when it is available may not be far off. The paper is written with ultimate rigor, ample details, and examples. The formalisms are explained and easy to follow. It is self-contained, and anyone with some background in formal system can start immersing him/herself easily into a world where miracles happen-and when they do, they are contained. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 26, Issue 5

Sep 2014

213 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 September 2014

Accepted: 21 June 2013

Revision received: 30 April 2013

Received: 20 September 2012

Published in FAC Volume 26, Issue 5

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
62
Total Downloads

Downloads (Last 12 months)33
Downloads (Last 6 weeks)7

Reflects downloads up to 20 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Naumann DNgo M(2019)Whither Specifications as ProgramsUnifying Theories of Programming10.1007/978-3-030-31038-7_3(39-61)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-31038-7_3
Boiten EJacob J(2014)Sealed Containers in ZProceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 847710.1007/978-3-662-43652-3_12(136-141)Online publication date: 2-Jun-2014
https://dl.acm.org/doi/10.1007/978-3-662-43652-3_12

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

References

Cited By

Index Terms

Recommendations

Specifying confidentiality in circus

Formal methods for security in the Xenon hypervisor

Unifying theories of confidentiality

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations