skip to main content
10.1145/1328438.1328478acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Cryptographically sound implementations for typed information-flow security

Published: 07 January 2008 Publication History

Abstract

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues.
We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract access-control policy for reading and writing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing.
We build a translation from well-typed source programs and policies to cryptographic implementations. To establish its correctness, we develop a type system for the target language. Our typing rules enforce a correct usage of cryptographic primitives against active adversaries; from an information-flow viewpoint, they capture controlled forms of robust declassification and endorsement. We showtype soundness for a variant of the non-interference property, then show that our translation preserves typability.
We rely on concrete primitives and hypotheses for cryptography, stated in terms of probabilistic polynomial-time algorithms and games. We model these primitives as commands in our target language. Thus, we develop a uniform language-based model of security, ranging from computational non-interference for probabilistic programs down to standard cryptographic hypotheses.

References

[1]
Martín Abadi. Protection in programming-language translations. In 25th International Colloquium on Automata, Languages and Programming, volume 1443 of LNCS, pages 868--883. Springer-Verlag, 1998.
[2]
Martín Abadi and Phillip Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryp-tology, 15(2):103--127, 2002.
[3]
Martín Abadi, Ricardo Corin, and Ćedric Fournet. Computational secrecy by typing for the pi calculus. In APLAS'06, volume 4279 of LNCS, pages 253--269. Springer-Verlag, November 2006.
[4]
Pedro Adão and Ćedric Fournet. Cryptographically sound implementations for communicating processes (extended abstract). In 33rd International Colloquium on Automata, Languages and Programming, volume 4052 of LNCS, pages 83--94. Springer-Verlag, July 2006.
[5]
Aslan Askarov, Daniel Hedin, and Andrei Sabelfeld. Cryptographically-masked flows. In Proceedings of the 13th International Static Analysis Symposium, LNCS, Seoul, Korea, 2006. Springer-Verlag.
[6]
M. Backes, B. Pfitzmann, and M. Waidner. A composable cryptographic library with nested operations. In 10th ACM Conference on Computer and Communications Security, pages 220--230, 2003.
[7]
Michael Backes. Quantifying probabilistic information flow in computational reactive systems. In ESORICS'05, volume 3679 of LNCS, pages 336--354. Springer-Verlag, September 2005.
[8]
Mihir Bellare and Phillip Rogaway. The game-playing technique, December 2004. At http://www.cs.ucdavis.edu/~rogaway/papers/games.html.
[9]
Mihir Bellare, Alexandra Boldyreva, and Silvio Micali. Public-key encryption in a multi-user setting: Security proofs and improvements. In EU-ROCRYPT, pages 259--274, 2000.
[10]
Dorothy E. Denning. A lattice model of secure information flow. Commun. ACM, 19(5):236--243, 1976.
[11]
Shafi Goldwasser, Silvio Micali, and Ronald Rivest. A digital signature scheme secure against adaptive chosen-message attack. SIAM Journal on Computing, 17(2):281--308, 1988.
[12]
Holger Hermanns. Interactive Markov Chains: The Quest for Quantified Quality. Springer Berlin/Heidelberg, 2002.
[13]
Peeter Laud. Secrecy types for a simulatable cryptographic library. In 12th ACM Conference on Computer and Communications Security, pages 26--35, 2005.
[14]
Peeter Laud. Semantics and program analysis of computationally secure information flow. In 10th European Symposium on Programming (ESOP 2001), volume 2028 of LNCS. Springer-Verlag, April 2001.
[15]
Peeter Laud. On the computational soundness of cryptographically-masked flows. In Proceedings of the 35th Symposium on Principles of Programming Languages, San Francisco, USA, 2008. ACM Press.
[16]
Peeter Laud and Varmo Vene. A type system for computationally secure information flow. In Fundamentals of Computation Theory, LNCS, pages 365--377. Springer-Verlag, 2005.
[17]
Wenbo Mao. Modern Cryptography: Theory and Practice. Prentice Hall Professional Technical Reference, 2003.
[18]
David Monniaux. Analyse de programmes probabilistes par interprétation abstraite. PhD thesis, Université Paris IX Dauphine, 2001.
[19]
Andrew C. Myers and Barbara Liskov. Protecting privacy using the decentralized label model. ACM Trans. Softw. Eng. Methodol., 9(4):410--442, 2000.
[20]
Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. Enforcing robust declassification and qualified robustness. Journal of Computer Security, 14(2):157--196, 2006.
[21]
Charles Rackoff and Daniel R. Simon. Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack. In CRYPTO'91, volume 576 of LNCS, pages 433--444. Springer-Verlag, 1991.
[22]
Andrei Sabelfeld and Andrew Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), 2003.
[23]
Geoffrey Smith and Rafael Alpízar. Secure information flow with random assignment and encryption. In FMSE '06: Proceedings of the fourth ACM workshop on Formal methods in security, pages 33--44, 2006.
[24]
Jeffrey A. Vaughan and Steve Zdancewic. A cryptographic decentralized label model. In IEEE Symposium on Security and Privacy, pages 192--206, May 2007.
[25]
Steve Zdancewic and Andrew Myers. Robust declassification. In 14th IEEE Computer Security Foundations Workshop, pages 15--23, 2001.
[26]
Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. Secure program partitioning. ACM Trans. Comput. Syst., 20(3): 283--328, 2002.
[27]
Lantian Zheng, Steve Chong, Andrew Myers, and Steve Zdancewic. Using replication and partitioning to build secure distributed systems. In 15th IEEE Symposium on Security and Privacy, 2003.

Cited By

View all
  • (2024)Computationally Bounded Robust Compilation and Universally Composable Security2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00024(265-278)Online publication date: 8-Jul-2024
  • (2023)PROSPECTProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620638(7161-7178)Online publication date: 9-Aug-2023
  • (2023)Adversarial Reachability for Program-level Security AnalysisProgramming Languages and Systems10.1007/978-3-031-30044-8_3(59-89)Online publication date: 22-Apr-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
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
  • 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
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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. compilers
  2. computational model
  3. confidentiality
  4. cryptography
  5. integrity
  6. non-interference
  7. probabilistic programs
  8. secure information flow
  9. type systems

Qualifiers

  • Research-article

Conference

POPL08

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)17
  • Downloads (Last 6 weeks)4
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Computationally Bounded Robust Compilation and Universally Composable Security2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00024(265-278)Online publication date: 8-Jul-2024
  • (2023)PROSPECTProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620638(7161-7178)Online publication date: 9-Aug-2023
  • (2023)Adversarial Reachability for Program-level Security AnalysisProgramming Languages and Systems10.1007/978-3-031-30044-8_3(59-89)Online publication date: 22-Apr-2023
  • (2021)Viaduct: an extensible, optimizing compiler for secure distributed programsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454074(740-755)Online publication date: 19-Jun-2021
  • (2020)RIFJournal of Computer Security10.3233/JCS-19131628:2(191-228)Online publication date: 1-Jan-2020
  • (2020)End-to-end information flow security for web services orchestrationScience of Computer Programming10.1016/j.scico.2019.102376187(102376)Online publication date: Feb-2020
  • (2020)Type-Based Declassification for FreeFormal Methods and Software Engineering10.1007/978-3-030-63406-3_11(181-197)Online publication date: 19-Dec-2020
  • (2019)On the expressiveness and semantics of information flow typesJournal of Computer Security10.3233/JCS-191382(1-28)Online publication date: 6-Dec-2019
  • (2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
  • (2019)Information Flow Control for Distributed Trusted Execution Environments2019 IEEE 32nd Computer Security Foundations Symposium (CSF)10.1109/CSF.2019.00028(304-30414)Online publication date: Jun-2019
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media