We integrate programming constructs for managing confidentiality in an ML-like imperative and higher-order programming language, dealing with both access control and information flow control. Our language includes in particular a construct for declassifying information, and constructs for granting, restricting or testing the read access level of a program. We introduce a type and effect system to statically check access rights and information flow. We show that typable programs are secure, that is, they do not attempt at making illegal read accesses, nor illegal information leakage. This provides us with a natural restriction on declassification, namely that a program may only declassify information that is has the right to read.


Access control declassification language-based security secure information flow stack inspection type and effect systems 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Almeida Matos, A., Boudol, G.: On declassification and the non-disclosure policy. In: CSFW′05, pp. 226–240 (2005) Revised version accepted for publication in the J. of Computer Security, available from the authors web page.Google Scholar
  2. 2.
    Banerjee, A., Naumann, D.A.: Stack-based access control for secure information flow. J. of Functional Programming. special issue on Language-Based Security 15, 131–177 (2005).zbMATHMathSciNetGoogle Scholar
  3. 3.
    Boudol, G.: On typing information flow. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 366–380. Springer, Heidelberg (2005).CrossRefGoogle Scholar
  4. 4.
    Broberg, N., Sands, D.: Flow locks: towards a core calculus for dynamic flow policies. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 180–196. Springer, Heidelberg (2006).Google Scholar
  5. 5.
    Chong, S., Myers, A.C.: Security policies for downgrading. In: 11th ACM Conf. on Computer and Communications Security (2004).Google Scholar
  6. 6.
    Cohen, E.: Information transmission in computational systems. In:6th ACM Symp. on Operating Systems Principles, pp. 133–139 (1977).Google Scholar
  7. 7.
    Denning, D.E.: A lattice model of secure information flow. CACM 19(5), 236–243 (1976).zbMATHMathSciNetGoogle Scholar
  8. 8.
    Fournet, C., Gordon, A.: Stack inspection: theory and variants. In: POPL′02, pp. 307–318 (2002).Google Scholar
  9. 9.
    Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symp. on Security and Privacy, pp. 11–20 (1982).Google Scholar
  10. 10.
    Lampson, B.W.: A note on the confinement problem. CACM 16(10), 613–615 (1973).Google Scholar
  11. 11.
    Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: POPL′88, pp. 47–57 (1988)Google Scholar
  12. 12.
    Li, P., Zdancewic, S.: Downgrading policies and relaxed noninterference. In: POPL′05, pp. 158–170 (2005)Google Scholar
  13. 13.
    Myers, A.: JFlow: practical mostly-static information flow control. In: POPL′99 (1999)Google Scholar
  14. 14.
    Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: ACM Symp. on Operating Systems Principles, pp. 129–142 (1997).Google Scholar
  15. 15.
    Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification and qualified robustness. J. of Computer Security 14(2), 157–196 (2006)Google Scholar
  16. 16.
    Pottier, F., Conchon, S.: Information flow inference for free. In: ICFP′00, pp. 46–57 (2000)Google Scholar
  17. 17.
    Pottier, F., Skalka, C., Smith, S.: A systematic approach to static access control. ACM TOPLAS 27(2), 344–382 (2005)CrossRefGoogle Scholar
  18. 18.
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. on Selected Areas in Communications 21(1), 5–19 (2003)CrossRefGoogle Scholar
  19. 19.
    Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, Springer, Heidelberg (2004)Google Scholar
  20. 20.
    Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: CSFW′00 (2000)Google Scholar
  21. 21.
    Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: CSFW′05, pp. 255–269 (2005)Google Scholar
  22. 22.
    Simonet, V.: The Flow Caml system: documentation and user’s manual INRIA Tech. Rep. 0282 (2003)Google Scholar
  23. 23.
    Skalka, C., Smith, S.: Static enforcement of security with types. In: ICFP′00, pp. 34–45 (2000)Google Scholar
  24. 24.
    Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. of Computer Security 4(3), 167–187 (1996)Google Scholar
  25. 25.
    Wright, A., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Zdancewic, S.: Challenges for information-flow security. In: PLID′04 (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Gérard Boudol
    • 1
  • Marija Kolundžija
    • 1
  1. 1.INRIASophia AntipolisFrance

Personalised recommendations