research-article

On the computational soundness of cryptographically masked flows

Author:

Peeter LaudAuthors Info & Claims

ACM SIGPLAN Notices, Volume 43, Issue 1

Pages 337 - 348

https://doi.org/10.1145/1328897.1328479

Published: 07 January 2008 Publication History

Abstract

To speak about the security of information flow in programs employing cryptographic operations, definitions based on computational indistinguish ability of distributions over program states have to be used. These definitions, as well as the accompanying analysis tools, are complex and error-prone to argue about. Cryptographically masked flows, proposed by Askarov, Hedin and Sabelfeld, are an abstract execution model and security definition that attempt to abstract away the details of computational security. This abstract model is useful because analysis of programs can be conducted using the usual techniques for enforcing non-interference.

In this paper we investigate under which conditions this abstract model is computationally sound, i.e. when does the security of a program in their model imply the computational security of this program. This paper spells out a reasonable set of conditions and then proposes a simpler abstract model that is nevertheless no more restrictive than the cryptographically masked flows together with these conditions for soundness.

References

[1]

Martin Abadi. Secrecy by Typing in Security Protocols. Journal of the ACM, 46(5):749--786, September 1999.

Digital Library

[2]

Martin Abadi and Jan Jürjens. Formal Eavesdropping and Its Computational Interpretation. In Naoki Kobayashi and Benjamin C. Pierce, editors, Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, volume 2215 of LNCS, pages 82--94, Sendai, Japan, October 2001. Springer-Verlag.

Digital Library

[3]

Martin Abadi and Phillip Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, and Takayasu Ito, editors, International Conference IFIP TCS 2000, volume 1872 of LNCS, pages 3--22, Sendai, Japan, August 2000. Springer-Verlag.

Digital Library

[4]

Pedro AdÜao, Gergei Bana, Jonathan Herzog, and Andre Scedrov. Soundness of formal encryption in the presence of key-cycles. In Sabrina De Capitani di Vimercati, Paul F. Syverson, and Dieter Gollmann, editors, ESORICS, volume 3679 of Lecture Notes in Computer Science, pages 374--396. Springer, 2005.

Digital Library

[5]

Johan Agat. Transforming out timing leaks. In POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 40--53, Boston, Massachusetts, January 2000. ACM Press.

Digital Library

[6]

Aslan Askarov and Andrei Sabelfeld. Gradual release: Unifying declassification, encryption and key release policies. In Pfitzmann and McDaniel (2007), pages 207--221.

Digital Library

[7]

Aslan Askarov, Daniel Hedin, and Andrei Sabelfeld. Cryptographically masked flows. In Kwangkeun Yi, editor, SAS, volume 4134 of Lecture Notes in Computer Science, pages 353--369. Springer, 2006.

Digital Library

[8]

Michael Backes, Birgit Pfitzmann, and Michael Waidner. A Universally Composable Cryptographic Library. In Proceedings of the 10th ACM Conference on Computer and Communications Security, Washington, DC, October 2003. ACM Press. Extended version available as Report 2003/015 of Cryptology ePrint Archive.

Digital Library

[9]

Mihir Bellare and Chanathip Namprempre. Authenticated Encryption: Relations among Notions and Analysis of the Generic Composition Paradigm. In Tatsuaki Okamoto, editor, Advances in Cryptology -- ASIACRYPT 2000, 6th International Conference on the Theory and Application of Cryptology and Information Security, volume 1976 of LNCS, pages 531--545, Kyoto, Japan, December 2000. Springer-Verlag.

Digital Library

[10]

Mihir Bellare and Phillip Rogaway. Random Oracles are Practical: A Paradigm for Designing Efficient Protocols. In CCS '93, Proceedings of the 1st ACM Conference on Computer and Communications Security, pages 62--73, Fairfax, Virginia, November 1993. ACM Press.

Digital Library

[11]

Mihir Bellare, Anand Desai, Eron Jokipii, and Phillip Rogaway. A Concrete Security Treatment of Symmetric Encryption. In 38th Annual Symposium on Foundations of Computer Science, pages 394--403, Miami Beach, Florida, October 1997. IEEE Computer Society Press.

Digital Library

[12]

John Black, Phillip Rogaway, and Thomas Shrimpton. Encryption-scheme security in the presence of key-dependent messages. In Kaisa Nyberg and Howard M. Heys, editors, Selected Areas in Cryptography, volume 2595 of Lecture Notes in Computer Science, pages 62--75. Springer, 2002.

Digital Library

[13]

Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne Riis Nielson. Static analysis for secrecy and non-interference in networks of processes. In Victor E. Malyshkin, editor, PaCT, volume 2127 of Lecture Notes in Computer Science, pages 27--41. Springer, 2001.

Digital Library

[14]

Veronique Cortier and Bogdan Warinschi. Computationally Sound, Automated Proofs for Security Protocols. In Shmuel Sagiv, editor, Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, volume 3444 of LNCS, pages 157--171, Edinburgh, UK, April 2005. Springer-Verlag.

Digital Library

[15]

Danny Dolev and Andrew C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(12):198--208, March 1983.

Digital Library

[16]

Cedric Fournet and Tamara Rezk. Cryptographically Sound Implementations for Typed Information-Flow Security. In POPL 2008, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, January 2008. ACM Press.

Digital Library

[17]

Joseph A. Goguen and Jose Meseguer. Security Policies and Security Models. In Proceedings of the 1982 IEEE Symposium on Security and Privacy, pages 11--20, Oakland, California, April 1982. IEEE Computer Society Press.

[18]

Oded Goldreich. Foundations of Cryptography. Volume 1 -- Basic Tools. Cambridge University Press, 2001.

Digital Library

[19]

Jonathan Herzog. Computational Soundness of Formal Adversaries. Master's thesis, Massachusetts Institute of Technology, September 2002.

[20]

Peeter Laud. Semantics and Program Analysis of Computationally Secure Information Flow. In David Sands, editor, Programming Languages and Systems, 10th European Symposium on Programming, ESOP 2001, volume 2028 of LNCS, pages 77--91, Genova, Italy, April 2001. Springer-Verlag.

Digital Library

[21]

Peeter Laud. Handling Encryption in Analyses for Secure Information Flow. In Pierpaolo Degano, editor, Programming Languages and Systems, 12th European Symposium on Programming, ESOP 2003, volume 2618 of LNCS, pages 159--173, Warsaw, Poland, April 2003. Springer-Verlag.

[22]

Peeter Laud and Varmo Vene. A Type System for Computationally Secure Information Flow. In Maciej Liśkiewicz and Rüdiger Reischuk, editors, 15th International Symposium on Fundamentals of Computation Theory (FCT) 2005, volume 3623 of LNCS, pages 365--377, Lübeck, Germany, August 2005. Springer-Verlag.

Digital Library

[23]

John McLean. Security models and information flow. In IEEE Symposium on Security and Privacy, pages 180--189, 1990.

[24]

Andrew C. Myers. JFlow: Practical Mostly-Static Information Flow Control. In POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 228--241, San Antonio, Texas, January 1999. ACM Press.

Digital Library

[25]

Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: A Formal Introduction. Wiley, 1992.

Digital Library

[26]

Birgit Pfitzmann and Patrick McDaniel, editors. 2007 IEEE Symposium on Security and Privacy (S&P 2007), 20-23 May 2007, Oakland, California, USA, 2007. IEEE Computer Society.

[27]

Andrei Sabelfeld and Andrew C. Myers. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, January 2003.

Digital Library

[28]

Andrei Sabelfeld and David Sands. A Per Model of Secure Information Flow in Sequential Programs. In S. Doaitse Swierstra, editor, Programming Languages and Systems, 8th European Symposium on Programming, ESOP'99, volume 1576 of LNCS, pages 40--58, Amsterdam, The Netherlands, March 1999. Springer-Verlag.

Digital Library

[29]

Andrei Sabelfeld and David Sands. Dimensions and principles of declassification. In CSFW, pages 255--269. IEEE Computer Society, 2005.

Digital Library

[30]

Geoffrey Smith and Rafael Alpizar. Secure Information Flow with Random Assignment and Encryption. In 4th ACM Workshop on Formal Methods in Security Engineering, pages 33--43, 2006.

Digital Library

[31]

Geoffrey Smith and Dennis M. Volpano. Secure Information Flow in a Multi-threaded Imperative Language. In POPL '98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 355--364, San Diego, California, January 1998. ACM Press.

Digital Library

[32]

Jeffrey A. Vaughan and Steve Zdancewic. A cryptographic decentralized label model. In Pfitzmann and McDaniel (2007), pages 192--206.

Digital Library

Cited By

Gancher JGibson SSingh PDharanikota SParno B(2023)Owl: Compositional Verification of Security Protocols via an Information-Flow Type System2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179477(1130-1147)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179477
Jia LVaughan JMazurak KZhao JZarko LSchorr JZdancewic SHook JThiemann P(2008)AURAProceedings of the 13th ACM SIGPLAN international conference on Functional programming10.1145/1411204.1411212(27-38)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411204.1411212
Jia LVaughan JMazurak KZhao JZarko LSchorr JZdancewic S(2008)AURAACM SIGPLAN Notices10.1145/1411203.141121243:9(27-38)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411203.1411212
Show More Cited By

Index Terms

On the computational soundness of cryptographically masked flows
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics
      1. Operational semantics

Recommendations

On the computational soundness of cryptographically masked flows
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

To speak about the security of information flow in programs employing cryptographic operations, definitions based on computational indistinguish ability of distributions over program states have to be used. These definitions, as well as the accompanying ...
Cryptographically-masked flows

Cryptographic operations are essential for many security-critical systems. Reasoning about information flow in such systems is challenging because typical (noninterference-based) information-flow definitions allow no flow from secret to public data. ...
Cryptographically-Masked flows
SAS'06: Proceedings of the 13th international conference on Static Analysis

Cryptographic operations are essential for many security-critical systems. Reasoning about information flow in such systems is challenging because typical (noninterference-based) information-flow definitions allow no flow from secret to public data. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 43, Issue 1

POPL '08

January 2008

420 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1328897

Issue’s Table of Contents

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2008
448 pages
ISBN:9781595936899
DOI:10.1145/1328438
General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Published in SIGPLAN Volume 43, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
429
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)3

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gancher JGibson SSingh PDharanikota SParno B(2023)Owl: Compositional Verification of Security Protocols via an Information-Flow Type System2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179477(1130-1147)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179477
Jia LVaughan JMazurak KZhao JZarko LSchorr JZdancewic SHook JThiemann P(2008)AURAProceedings of the 13th ACM SIGPLAN international conference on Functional programming10.1145/1411204.1411212(27-38)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411204.1411212
Jia LVaughan JMazurak KZhao JZarko LSchorr JZdancewic S(2008)AURAACM SIGPLAN Notices10.1145/1411203.141121243:9(27-38)Online publication date: 20-Sep-2008
https://dl.acm.org/doi/10.1145/1411203.1411212
Acay CGancher JRecto RMyers A(2024)Secure Synthesis of Distributed Cryptographic Applications2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00021(433-448)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00021
Gancher JGibson SSingh PDharanikota SParno B(2023)Owl: Compositional Verification of Security Protocols via an Information-Flow Type System2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179477(1130-1147)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179477
Kozyri ESchneider F(2020)RIFJournal of Computer Security10.3233/JCS-19131628:2(191-228)Online publication date: 1-Jan-2020
https://dl.acm.org/doi/10.3233/JCS-191316
Waye LBuiras PArden ORusso AChong SThuraisingham BEvans DMalkin TXu D(2017)Cryptographically Secure Information Flow Control on Key-Value StoresProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security10.1145/3133956.3134036(1893-1907)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.1145/3133956.3134036
Backes MKünnemann RMohammadi EWeippl EKatzenbeisser SKruegel CMyers AHalevi S(2016)Computational Soundness for Dalvik BytecodeProceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security10.1145/2976749.2978418(717-730)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2976749.2978418
Said NAbdellatif TBensalem SBozga M(2016)A Model-Based Approach to Secure Multiparty Distributed SystemsLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques10.1007/978-3-319-47166-2_62(893-908)Online publication date: 5-Oct-2016
https://doi.org/10.1007/978-3-319-47166-2_62
Askarov AMoore SDimoulas CChong S(2015)Cryptographic Enforcement of Language-Based Information ErasureProceedings of the 2015 IEEE 28th Computer Security Foundations Symposium10.1109/CSF.2015.30(334-348)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1109/CSF.2015.30
Show More Cited By

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents