Abstract
“Classical” proofs of secure systems are based on reducing the hardness of one problem (defined by the protocol) to that of another (a known difficult computational problem). In standard program development [1, 3, 14] this “comparative approach” features in stepwise refinement: describe a system as simply as possible so that it has exactly the required properties and then apply sound refinement rules to obtain an implementation comprising specific algorithms and data-structures.
More recently the stepwise refinement method has been extended to include “information flow” properties as well as functional properties, thus supporting proofs about secrecy within a program refinement method.
In this paper we review the security-by-refinement approach and illustrate how it can be used to give an elementary treatment of some well known security principles.
Keywords
A.K. McIver — We acknowledge the support of the Australian Research Council Grant DP140101119.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
For simplicity we do not consider the empty set, i.e. outputs of the form \((\mathsf{v}, \{\})\).
- 3.
Equivalently it can be done by publishing the value in any visible variable and then overwriting that variable with its former value, leaving perfect recall to retain the information revealed.
- 4.
This abstract algebraic property also captures the capability of a “known plain text attack”. An encryption mechanism is susceptible to a known plain-text attack if, given the message m and the encryption E.m.k is able to work out the key k. If such an attack succeeds against an encryption method then we would say that the encryption mechanism satisfies (5).
- 5.
We prove in the Appendix Sect. A.1 that this property holds for E implemented with \(\oplus \), exclusive-or.
References
Abrial, J.-R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)
Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF 2012), pp. 265–279, June 2012
Back, R.-J.R.: Correctness preserving program refinements: proof theory and applications, Tract 131, Mathematisch Centrum, Amsterdam (1980)
Denning, D.: Cryptography and Data Security. Addison-Wesley, Boston (1983)
Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 75–86. IEEE Computer Society (1984)
Landauer, J., Redmond, T.: A lattice of information. In: Proceedings of the 6th IEEE Computer Security Foundations Workshop (CSFW 1993), pp. 65–70, June 1993
Leino, K.R.M., Joshi, R.: A semantic approach to secure information flow. Sci. Comput. Program. 37(1–3), 113–138 (2000)
Mantel, H.: Preserving information flow properties under refinement. In: Proceedings of the IEEE Symposium Security and Privacy, pp. 78–91 (2001)
McIver, A.K.: The secret art of computer programming. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 61–78. Springer, Heidelberg (2009)
McIver, A.K., Morgan, C.C.: A calculus of revelations. Presented at VSTTE Theories Workshop, October 2008. http://www.cs.york.ac.uk/vstte08/
McIver, A.K., Morgan, C.C.: Sums and Lovers: Case Studies in Security, Compositionality and Refinement. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 289–304. Springer, Heidelberg (2009)
McIver, A., Meinicke, L., Morgan, C.: Compositional closure for bayes risk in probabilistic noninterference. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 223–235. Springer, Heidelberg (2010)
McIver, A., Morgan, C., Smith, G., Espinoza, B., Meinicke, L.: Abstract channels and their robust information-leakage ordering. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 83–102. Springer, Heidelberg (2014)
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Upper Saddle River (1994). http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/
Morgan, C.C.: The shadow knows: refinement of ignorance in sequential programs. In: Uustalu, T. (ed.) Math Prog Construction. Springer, vol. 4014, pp. 359–378. Springer, Treats Dining Cryptographers (2006)
Morgan, C.C., Knows, T.S.: Refinement of ignorance in sequential programs. Sci. Comput. Program. 74(8), 629–653 (2009). Treats Oblivious Transfer
Sabelfeld, A., Sands, D.: A PER model of secure information flow in sequential programs. High.-Ord. Symbolic Comput. 14(1), 59–91 (2001)
Schmidt, B., Schaller, P., Basin, D.: Impossibility results for secret establishment. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF), pp. 261–273 (2010)
Shamir, A.: How to share a secret. Commun. ACM 22(11), 612–613 (1979)
Shannon, C.E.: Theory of secrecy systems. Bell Syst. Tech. J. 28, 656–715 (1949)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Some Proofs
A Some Proofs
1.1 A.1 Learning a Value
We prove (9) for the special case where E is the exclusive-OR, \(\oplus \). We re-state (9) here for \(\oplus \).
where \(P= P'; \mathbf{vis }_B ~b {:}{=}\,X; \mathbf{reveal }~X\).
Assume that B has (private) variables \(b_1, b_2 , \dots b_k\), and that A has (private) variables \(a_1, a_2 \dots a_m\). We also assume that each variable is assigned exactly once and then never changed.
B’s knowledge of the state after executing \(P'\) can be summarised as follows:
-
1.
B knows the values of all its own variables \(b_1, b_2 , \dots b_k\).
-
2.
B knows the values of any encrypted value sent over the public channel. Each of those values is of the form
$$\begin{aligned} a_{i_1} \oplus a_{i_2} \oplus \dots \oplus a_{i_n}, \end{aligned}$$for some selection of variables drawn from \(a_1, a_2 \dots a_m\).
-
3.
B can learn new facts by using the facts he already has and computing new values using \(\oplus \). Let \(\mathcal{K}\) be the set of facts so-computed using \(\oplus \).
Notice that whenever a value \(\alpha \in \mathcal{K}\) we have that \(P'; \mathbf{reveal }_B~ \alpha = P'\).
Assume that \(Y \not \in \mathcal{K}\), but that when B learns X then he can deduce Y. We will show that \(X \oplus Y\) is contained in \(\mathcal{K}\).
Since \(Y \not \in \mathcal{K}\), this means that \(Y = X \oplus \alpha \) for some fact \(\alpha \in \mathcal{K}\). But with this we reason:
implying that \(X \oplus Y\) (i.e. E.Y.X as at (9)) is contained in \(\mathcal{K}\).
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
McIver, A.K. (2016). Program Refinement, Perfect Secrecy and Information Flow. In: Liu, Z., Zhang, Z. (eds) Engineering Trustworthy Software Systems. Lecture Notes in Computer Science(), vol 9506. Springer, Cham. https://doi.org/10.1007/978-3-319-29628-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-29628-9_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-29627-2
Online ISBN: 978-3-319-29628-9
eBook Packages: Computer ScienceComputer Science (R0)