Controlled Declassification Based on Intransitive Noninterference

  • Heiko Mantel
  • David Sands
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3302)


Traditional noninterference cannot cope with common features of secure systems like channel control, information filtering, or explicit downgrading. Recent research has addressed the derivation and use of weaker security conditions that could support such features in a language-based setting. However, a fully satisfactory solution to the problem has yet to be found. A key problem is to permit exceptions to a given security policy without permitting too much. In this article, we propose an approach that draws its underlying ideas from intransitive noninterference, a concept usually used on a more abstract specification level. Our results include a new bisimulation-based security condition that controls tightly where downgrading can occur and a sound security type system for checking this condition.


Security Policy Security Level Security Condition Covert Channel Security Domain 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Aga00]
    Agat, J.: Transforming out Timing Leaks. In: Proceedings of the ACM Symposium on Principles of Programming Languages, pp. 40–53 (2000)Google Scholar
  2. [BL76]
    Bell, D.E., LaPadula, L.: Secure Computer Systems: Unified Exposition and Multics Interpretation. Technical Report MTR-2997, MITRE (1976)Google Scholar
  3. [BP02]
    Backes, M., Pfitzmann, B.: Computational Probabilistic Non-interference. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol. 2502, pp. 1–23. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. [BPR04]
    Bossi, A., Piazza, C., Rossi, S.: Modelling Downgrading in Information Flow Security. In: Proc. of IEEE CSFW (to appear, 2004)Google Scholar
  5. [CHM02]
    Clark, D., Hunt, S., Malacaria, P.: Quantitative Analysis of the Leakage of Confidential Data. In: Quantitative Aspects of Programming Languages—Selected papers from QAPL 2001. ENTCS, vol. 59 (2002)Google Scholar
  6. [Coh78]
    Cohen, E.S.: Information Transmission in Sequential Programs. In: Foundations of Secure Computation, pp. 297–335. Academic Press, London (1978)Google Scholar
  7. [Den76]
    Denning, D.E.: A Lattice Model of Secure Information Flow. Communications of the ACM 19(5), 236–243 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  8. [DHW02]
    Di Pierro, A., Hankin, C., Wiklicky, H.: Approximate Non-Interference. In: Proceedings of IEEE CSFW, pp. 1–17 (2002)Google Scholar
  9. [Koc96]
    Kocher, P.C.: Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104–113. Springer, Heidelberg (1996)Google Scholar
  10. [Lau03]
    Laud, P.: Handling Encryption in an Analysis for Secure Information Flow. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol. 2618, pp. 159–173. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. [Low02]
    Lowe, G.: Quantifying Information Flow. In: Proceedings of IEEE CSFW, pp. 18–31 (2002)Google Scholar
  12. [Man01]
    Mantel, H.: Information Flow Control and Applications – Bridging a Gap. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 153–172. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. [MRST01]
    Mitchell, J., Ramanathan, A., Scedrov, A., Teague, V.: A Probabilistic Polynomial-Time Calculus for Analysis of Cryptographic Protocols (Preliminary report). In: Proc. of the Conf. on the Math. Foundations of Programming Semantics 1976. ENTCS, vol. 45 (2001)Google Scholar
  14. [MSZ04]
    Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing Robust Declassification. In: Proc. of IEEE CSFW (to appear, 2004)Google Scholar
  15. [Ohe04]
    von Oheimb, D.: Information Flow Control Revisited: Noninfluence = Noninterference + Nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 225–243. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. [Pin95]
    Pinsky, S.: Absorbing Covers and Intransitive Non-Interference. In: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, USA, pp. 102–113 (1995)Google Scholar
  17. [RG99]
    Roscoe, A.W., Goldsmith, M.H.: What is Intransitive Noninterference? In: Proceedings of IEEE CSFW, pp. 228–238 (1999)Google Scholar
  18. [Rus92]
    Rushby, J.M.: Noninterference, Transitivity, and Channel-Control Security Policies. Technical Report CSL-92-02, SRI International (1992)Google Scholar
  19. [SM03a]
    Sabelfeld, A., Myers, A.C.: A Model for Delimited Information Release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174–191. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. [SM03b]
    Sabelfeld, A., Myers, A.C.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)CrossRefGoogle Scholar
  21. [SS00]
    Sabelfeld, A., Sands, D.: Probabilistic Noninterference for Multi-threaded Programs. In: Proceedings of IEEE CSFW, pp. 200–214 (2000)Google Scholar
  22. [SS01]
    Sabelfeld, A., Sands, D.: A Per Model of Secure Information Flow in Sequential Programs. HOSC 14(1), 59–91 (2001)zbMATHGoogle Scholar
  23. [VS97]
    Volpano, D., Smith, G.: Eliminating Covert Flows with Minimum Typings. In: Proceedings of IEEE CSFW, pp. 156–168 (1997)Google Scholar
  24. [VS00]
    Volpano, D.M., Smith, G.: Verifying Secrets and Relative Secrecy. In: Proceedings of POPL, pp. 268–276 (2000)Google Scholar
  25. [Zda03]
    Zdancewic, S.: A Type System for Robust Declassification. In: Proc. of the Conf. on the Math. Foundations of Programming Semantics. ENTCS (2003)Google Scholar
  26. [ZM01]
    Zdancewic, S., Myers, A.C.: Robust Declassification. In: Proceedings of IEEE CSFW, pp. 15–23 (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Heiko Mantel
    • 1
  • David Sands
    • 2
  1. 1.Information SecurityETH ZürichSwitzerland
  2. 2.Chalmers University of TechnologyGöteborgSweden

Personalised recommendations