Hostname: page-component-586b7cd67f-r5fsc Total loading time: 0 Render date: 2024-11-28T16:02:40.907Z Has data issue: false hasContentIssue false
  • English
  • Français

Hidden-Markov program algebra with iteration

Published online by Cambridge University Press:  10 November 2014

ANNABELLE MCIVER ,
LARISSA MEINICKE  and
CARROLL MORGAN
ANNABELLE MCIVER
Affiliation:
Dept Comp Sci, Macquarie University, NSW, Australia Email: [email protected]
LARISSA MEINICKE
Affiliation:
Dept Comp Sci, Univ Queensland, Qld, Australia Email: [email protected]
CARROLL MORGAN
Affiliation:
School Comp Sci and Eng, Univ NSW, NSW, Australia Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We use hidden Markov models to motivate a quantitative compositional semantics for noninterference-based security with iteration, including a refinement- or ‘implements’ relation that compares two programs with respect to their information leakage; and we propose a program algebra for source-level reasoning about such programs, in particular as a means of establishing that an ‘implementation’ program leaks no more than its ‘specification’ program.

This joins two themes: we extend our earlier work, having iteration but only qualitative (Morgan 2009), by making it quantitative; and we extend our earlier quantitative work (McIver et al. 2010) by including iteration.

We advocate stepwise refinement and source-level program algebra – both as conceptual reasoning tools and as targets for automated assistance. A selection of algebraic laws is given to support this view in the case of quantitative noninterference; and it is demonstrated on a simple iterated password-guessing attack.

Type
Special Issue: Quantitative Information Flow
Information
Mathematical Structures in Computer Science , Volume 25 , Issue 2: Quantitative Information Flow , February 2015 , pp. 320 - 360
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Wikipedia (2011) en.wikipedia.org.Google Scholar
Aldini, A. and Pierro, A. D. (2004) A quantitative approach to noninterference for probabilistic systems. Electronic Notes in Theoretical Computer Science 99 155–182.Google Scholar
Alvim, M., Andres, M. and Palamidessi, C. (2010) Information flow in interactive systems. In: Proceedings 21st CONCUR. Springer Lecture Notes in Computer Science 6269 102–116.Google Scholar
Ash, R. B. (1972) Real Analysis and Probability, Academic Press.Google Scholar
Back, R. J. and von Wright, J. (1998) Refinement Calculus: A Systematic Introduction, Springer.Google Scholar
Backes, M. and Pfitzmann, B. (2002), Computational probabilistic non-interference. In: 7th European Symposium on Research in Computer Security. Lecture Notes in Computer Science 2502 1–23.Google Scholar
Bishop, C. (2006) Pattern Recognition and Machine Learning, Information Science and Statistics, Springer.Google Scholar
Braun, C., Chatzikokolakis, K. and Palamidessi, C. (2008) Compositional methods for information-hiding. In: Proceeding FOSSACS'08. Springer Lecture Notes in Computer Science 4962 443–457.Google Scholar
Braun, C., Chatzikokolakis, K. and Palamidessi, C. (2009) Quantitative notions of leakage for one-try attacks. In: Proceedings MFPS. Electronic Notes in Theoretical Computer Science 249 75–91.Google Scholar
Chatzikokolakis, K. and Palamidessi, C. (2007) A framework for analyzing probabilistic protocols and its application to the partial secrets exchange. Theoretical Computer Science 389 (3)512–27.CrossRefGoogle Scholar
Chatzikokolakis, K., Palamidessi, C. and Panangaden, P. (2007) Probability of error in information-hiding protocols. In: Proceedings CSF, IEEE Computer Society 341–354.Google Scholar
Cohn, H. (1974) A ratio limit theorem for the finite nonhomogeneous markov chains. Israel Journal of Mathematics 19 329–334.Google Scholar
Deng, Y. and Du, W. (2009) Kantorovich metric in computer science: A brief survey. Electronic Notes in Theoretical Computer Science 253 (3)119–133.CrossRefGoogle Scholar
Dudley, R. (2002) Real Analysis and Probability, Cambridge University Press.Google Scholar
Giry, M. (1981) A categorical approach to probability theory. In: Categorical Aspects of Topology and Analysis. Springer Lecture Notes in Mathematics 915 68–85.Google Scholar
Goguen, J. and Meseguer, J. (1984) Unwinding and inference control. In: Proceedings IEEE Symposium on Security and Privacy, IEEE Computer Society 75–86.Google Scholar
Halmos, P. (1973) The legend of von Neumann. The American Mathematical Monthly 80 (4)382–394.Google Scholar
Halpern, J. and O'Neill, K. (2002) Secrecy in multiagent systems. In: Proceedings 15th IEEE Computer Security Foundations Workshop 32–46.Google Scholar
Hart, S., Sharir, M. and Pnueli, A. (1983) Termination of probabilistic concurrent programs, ACM Transactions on Programming Language and Systems 5 356–380.Google Scholar
He, J., Seidel, K. and McIver, A. (1997) Probabilistic models for the guarded command language. Science of Computer Programming 28 171–192.Google Scholar
Jones, C. and Plotkin, G. (1989) A probabilistic powerdomain of evaluations. In: Proceedings of the IEEE 4th Annual Symposium on Logic in Computer Science, Los Alamitos, Calif. Computer Society Press 186–195.Google Scholar
Jurafsky, D. and Martin, J. (2000) Speech and Language Processing, Prentice Hall International.Google Scholar
Katoen, J. P., McIver, A. K., Meinicke, L. A. and Morgan, C. C. (2010) Linear-invariant generation for probabilistic programs: Automated support for proof-based methods. In: Proceedings Static Analysis Symposium, Springer 390–406.Google Scholar
Köpf, B. and Basin, D. (2007) An information-theoretic model for adaptive side-channel attacks. In: Proceedings 14th ACM Conference Computer and Communications Security.Google Scholar
Kozen, D. (1985) A probabilistic PDL. Journal of Computer and System Sciences 30 (2)162–178.Google Scholar
Malacaria, P. (2010) Risk assessment of security threats for looping constructs. Journal of Computer Security 18 (2)191–228.CrossRefGoogle Scholar
McIver, A., Gonzalia, C. and Morgan, C. (2009) Probabilistic affirmation and refutation: Case studies. In: Proceedings Automatic Program Verification.Google Scholar
McIver, A., Meinicke, L. and Morgan, C. (2010) Compositional closure for Bayes risk in probabilistic noninterference. In: Abramsky, S.et al., (eds.) Proceedings ICALP 2010. Lecture Notes in Computer Science 6199 223–235. Extended abstract.CrossRefGoogle Scholar
McIver, A. and Morgan, C. (2005) Abstraction, Refinement and Proof for Probabilistic Systems, Monographs in Computer Science, Springer, New York.Google Scholar
McIver, A. and Morgan, C. (2008) A calculus of revelations. Presented at VSTTE Theories Workshop. Available at www.cs.york.ac.uk/vstte08/.Google Scholar
McShane, E. (1937) Jensen's inequality. Bulletin of the American Mathematical Society 43 (8)521–527.Google Scholar
Moggi, E. (1989) Computational lambda-calculus and monads. In: Proceedings 4th Symposium LiCS 14–23.Google Scholar
Morgan, C. (1994) Programming from Specifications, 2nd edition, Prentice-Hall. Available at web.comlab.ox.ac.uk/oucl/publications/books/PfS/.Google Scholar
Morgan, C. (1996) Proof rules for probabilistic loops. In: Jifeng, H., Cooke, J. and Wallis, P. (eds.) Proceedings BCS-FACS 7th Refinement Workshop, Workshops in Computing, Springer. Available at ewic.bcs.org/conferences/1996/refinement/papers/paper10.htm.Google Scholar
Morgan, C. (2005) Of probabilistic wp and CSP. In: Abdallah, A., Jones, C. and Sanders, J., (eds.) Communicating Sequential Processes: The First 25 Years, Springer.Google Scholar
Morgan, C. (2006) The shadow knows: Refinement of ignorance in sequential programs. In: Uustalu, T. (ed.) Mathematics of Program Construction, 4014359–378. Springer. (Treats Dining Cryptographers.)Google Scholar
Morgan, C. (2009) The shadow knows: Refinement of ignorance in sequential programs. Science of Computer Programming 74 (8)629–653. (Treats Oblivious Transfer.)Google Scholar
Morgan, C. (2010) Compositional noninterference from first principles. Formal Aspects of Computing 1–24.Google Scholar
Morgan, C., McIver, A. and Seidel, K. (1996) Probabilistic predicate transformers. ACM Transactions on Programming Language and Systems 18 (3)325–353. doi.acm.org/10.1145/229542.229547.Google Scholar
Mu, C. and Clark, D. (2009) Quantitative analysis of secure information flow via probabilistic semantics. In: Proceedings ARES'09, IEEE 49–57.Google Scholar
Nelson, G. (1989) A generalization of Dijkstra's calculus. ACM Transactions on Programming Language and Systems 11 (4)517–561.Google Scholar
Roscoe, A. (1992) An alternative order for the failures model. Journal of Logic Computation 2 (5)557–577.Google Scholar
Sabelfeld, A. and Sands, D. (2000) Probabilistic noninterference for multi-threaded programs. In: 13th IEEE Computer Security Foundations Workshop (CSFW'00), 200–214.Google Scholar
Smith, G. (2003) Probabilistic noninterference through weak probabilistic bisimulation. In: 16th IEEE Computer Security Foundations Workshop (CSFW'03).Google Scholar
Sonin, I. (2008) The decomposition-separation theorem for finite nonhomogeneous markov chains and related problems. In: Markov Processes and Related Topics: A Festschrift for Thomas G Kurtz, volume 4, IMS 1–15.Google Scholar
Tarski, A. (1955) A lattice-theoretic fixpoint theorem and its applications. Pacific Journal of Mathematics 5 285–309.Google Scholar
van Breugel, F. (2005) The metric monad for probabilistic nondeterminism. Draft available at http://www.cse.yorku.ca/~franck/research/drafts/monad.pdf.Google Scholar
Volpano, D. and Smith, G. (1998) Probabilistic noninterference in a concurrent language. In: 11th IEEE Computer Security Foundations Workshop (CSFW'98), 34–43.Google Scholar
Wirth, N. (1971) Program development by stepwise refinement. Communications of the ACM 14 (4)221–227.Google Scholar
Worrell, J. (2010) Private communication.Google Scholar
Yasuoka, H. and Terauchi, T. (2010) Quantitative information flow – verification hardness and possibilities. In: Proceedings 23rd IEEE CSF Symposium, 15–27.CrossRefGoogle Scholar