Advertisement

Semantics and Program Analysis of Computationally Secure Information Flow

  • Peeter Laud
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)

Abstract

This paper presents a definition of secure information flow. It is not based on noninterference, but on computational indistinguishability of the secret inputs, when the public outputs are observed. This definition allows cryptographic primitives to be handled. This paper also presents a Denning-style information-flow analysis for programs that use encryption as a primitive operation. The proof of the correctness of the analysis is sketched.

Keywords

Secure Information Security Parameter Public Output Covert Channel Cryptographic Primitive 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A Core Calculus of Dependency. In proc. of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, January 20-22, 1999, ACM Press, pp. 147–160, 1999.Google Scholar
  2. 2.
    Abadi, M., Rogaway, P.: Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.): proc. of the International Conference IFIP TCS 2000 Sendai, Japan, August 17-19, 2000 (LNCS 1872), Springer-Verlag pp. 3–22, 2000.Google Scholar
  3. 3.
    Cohen, E.: Information Transmission in Sequential Programs. In: DeMillo, R.A., Dobkin, D.P., Jones, A.K., Lipton, R.J. (eds.): Foundations of Secure Computation. Academic Press, pp. 297–335. 1978.Google Scholar
  4. 4.
    Denning, D.E.: A Lattice Model of Secure Information Flow. Communications of the ACM 19(5), pp. 236–243, 1976.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Denning, D.E., Denning, P.: Certification of Programs for Secure Information Flow. Communications of the ACM 20(7), pp. 504–513, 1977.zbMATHCrossRefGoogle Scholar
  6. 6.
    Goldreich, O.: The Foundations of Modern Cryptography. In: Kaliski, B. (ed.): proc. of CRYPTO’ 97, Santa Barbara, CA, August 17-21, 1997 (LNCS 1294), Springer-Verlag, pp. 46–74, 1997.Google Scholar
  7. 7.
    Heintze, N., Riecke, J.G.: The SLam Calculus: Programming with Secrecy and Integrity. In proc. of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, January 19-21, 1998, ACM Press, pp. 365–377, 1998.Google Scholar
  8. 8.
    Kaliski, B., Staddon, J.: PKCS #1: RSA Cryptography Standard. Version 2.0. RSA Laboratories, September 1998.Google Scholar
  9. 9.
    Landi, W.: Interprocedural Aliasing in the Presence of Pointers. PhD thesis, Rutgers University, 1992.Google Scholar
  10. 10.
    Leino, K.R.M., Joshi, R.: A Semantic Approach to Secure Information Flow. In: Jeuring, J. (ed.): proc. of “Mathematics of Program Construction, MPC’98”, Marstrand, Sweden, June 15-17, 1998 (LNCS 1422), Springer-Verlag, 254–271, 1998.Google Scholar
  11. 11.
    Myers, A.C.: JFlow: Practical Mostly-Static Information Flow Control. In proc. of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, January 20-22, 1999, ACM Press, pp. 228–241, 1999.Google Scholar
  12. 12.
    Reitman, R.P., Andrews, G.R.: Certifying information flow properties of programs: an axiomatic approach. In proc. of the 6th Annual ACM Symposium on Principles of Programming Languages, San Antonio, TX, January 1979, ACM Press, pp. 283–290, 1979.Google Scholar
  13. 13.
    Sabelfeld, A., Sands, D.: A Per Model of Secure Information Flow in Sequential Programs. In: Swierstra, S.D. (ed.): proc. of the 8th European Symposium on Programming, ESOP’99, Amsterdam, The Netherlands, 22-28 March, 1999 (LNCS 1576), Springer-Verlag, pp. 40–58, 1999.Google Scholar
  14. 14.
    Volpano, D., Smith, G., Irvine, C.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4(2,3), pp. 167–187, 1996.Google Scholar
  15. 15.
    Volpano, D., Smith, G.: Verifying secrets and relative secrecy. In proc. of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, MA, January 19-21, 2000, ACM Press, pp. 268–276, 2000.Google Scholar
  16. 16.
    Volpano, D.: Secure Introduction of One-way Functions. In proc. of the 13th IEEE Computer Security Foundations Workshop. Cambridge, UK, July 3-5, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Peeter Laud
    • 1
  1. 1.FR InformatikUniversität des SaarlandesSaarlandes

Personalised recommendations