Advertisement

Enforcing Information Flow Policies by a Three-Valued Analysis

  • Josée Desharnais
  • Erwanne P. Kanyabwero
  • Nadia Tawbi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7531)

Abstract

This paper presents an approach to enforce information flow policies using a three-valued type-based analysis on a core imperative language. Our analysis aims first at reducing false positives generated by static analysis, and second at preparing for instrumentation. False positives arise in the analysis of real computing systems when some information is missing at compile time, for example the name of a file, and consequently, its security level. The key idea of our approach is to distinguish between negative and may responses. Instead of rejecting in the latter cases, we type instructions with an additional type, unknown, indicating uncertainty, possibly preparing for a light instrumentation. During the static analysis step, the may responses are identified and annotated with the unknown security type, while the positive and negative responses are treated as is usually done. This work is done in preparation of a hybrid security enforcement mechanismWe prove that our type system is sound by showing that it satisfies non-interference. The novelty is the handling of three security types, but we also treat variables and channels in a special way. Programs interact via communication channels. Secrecy levels are associated to channels rather than to variables whose security levels change according to the information they store.

Keywords

Type System Secure Information Security Level Channel Variable Typing Rule 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Volpano, D., Irvine, C., Smith, G.: A sound type system for secure ow analysis. Journal of Computer Security 4(2-3), 167–187 (1996)Google Scholar
  2. 2.
    Hunt, S., Sands, D.: On flow-sensitive security types. In: Proceedings of the ACM Symposium on Principles of Programming Languages (January 2006)Google Scholar
  3. 3.
    Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: Proceedings of the IEEE Computer Security Foundations Symposium (2010)Google Scholar
  4. 4.
    Denning, D.E.: A lattice model of secure information flow. Communications of the ACM 19, 236–243 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
  5. 5.
    Smith, G.: Principles of secure information flow analysis. In: Malware Detection, vol. 27, pp. 291–307. Springer (2007)Google Scholar
  6. 6.
    O’Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: Proceedings of the IEEE Computer Security Foundations Workshop (July 2006)Google Scholar
  7. 7.
    Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4-5), 291–347 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-Insensitive Noninterference Leaks More Than Just a Bit. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 333–348. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Denning, D.E., Denning, P.J.: Certi cation of programs for secure information flow. Communications of the ACM 20, 504–513 (1977)zbMATHCrossRefGoogle Scholar
  10. 10.
    Smith, G.: A new type system for secure information flow. In: Proceedings of the IEEE Workshop on Computer Security Foundations, pp. 115–125 (2001)Google Scholar
  11. 11.
    Pottier, F., Simonet, V.: Information flow inference for ML. ACM Transactions on Programming Languages and Systems 25, 117–158 (2003)CrossRefGoogle Scholar
  12. 12.
    Myers, A.C.: J ow: Practical mostly-static information flow control. In: Proceedings of the ACM Symposium on Principles of Programming Languages (1999)Google Scholar
  13. 13.
    Banerjee, A., Naumann, D.A.: Secure information flow and pointer con nement in a java-like language. In: Proceedings of the IEEE Computer Security Foundations Workshop (2002)Google Scholar
  14. 14.
    Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the IEEE Workshop on Computer Security Foundations (2004)Google Scholar
  15. 15.
    Terauchi, T., Aiken, A.: Secure Information Flow as a Safety Problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Sabelfeld, A., Sands, D.: A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation 14(1), 59–91 (2001)zbMATHCrossRefGoogle Scholar
  17. 17.
    Barthe, G., Prensa Nieto, L.: Secure information flow for a concurrent language with scheduling. Journal of Computer Security 15, 647–689 (2007)Google Scholar
  18. 18.
    Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proceedings of the IEEE Workshop on Computer Security Foundations (2000)Google Scholar
  19. 19.
    Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: Proceedings of the IEEE Computer Security Foundations Workshop (June-July 2003)Google Scholar
  20. 20.
    Smith, G.: Improved typings for probabilistic noninterference in a multi-threaded language. Journal of Computer Security 14(6), 591–623 (2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Josée Desharnais
    • 1
  • Erwanne P. Kanyabwero
    • 1
  • Nadia Tawbi
    • 1
  1. 1.Department of Computer Science and Software EngineeringUniversité LavalCanada

Personalised recommendations