Timed Abstract Non-interference

  • Roberto Giacobazzi
  • Isabella Mastroeni
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


In this paper, we introduce a timed notion of abstract non-interference. This is obtained by considering semantics which observe time elapsed in computations. Timing channels can be modeled in this way either by letting the attacker to observe time as a public variable or reckon the time elapsed by observing the computational traces’ length, corresponding to observe the program counter. In the first case abstract non-interference provides a model for abstracting the information about time, namely we can for example consider models of attackers that can observe only intervals of time, or other more abstract properties. In the second case abstract non-interference provides a model for attackers able to observe properties of trace length, e.g., the public memory during the whole computation. We investigate when adding the observation of time does not increase the attacker’s power in disclosing confidential information about data. This models the absence of timing channels in language-based security.


Abstract interpretation security non-interference timing channels 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Agat, J.: Transforming out timing leaks. In: Proc. of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), pp. 40–53. ACM Press, New York (2000)CrossRefGoogle Scholar
  2. 2.
    Alpern, B., Demers, A.J., Schneider, F.B.: Safety without stuttering. Information Processing Letters 23(4), 177–180 (1986)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Barbuti, R., De Francesco, N., Santone, A., Tesei, L.: A notion of non-interference for timed automata. Fundamenta Informaticae 51, 1–11 (2002)zbMATHMathSciNetGoogle Scholar
  5. 5.
    Bell, D.E., LaPadula, L.J.: Secure computer systems: Mathematical foundations and model. Technical Report M74-244, MITRE Corp. Badford, MA (1973)Google Scholar
  6. 6.
    Clark, D., Hankin, C., Hunt, S.: Information flow for algol-like languages. Computer Languages 28(1), 3–28 (2002)zbMATHGoogle Scholar
  7. 7.
    Cohen, E.S.: Information transmission in sequential programs. In: Foundations of Secure Computation, pp. 297–335 (1978)Google Scholar
  8. 8.
    Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277(1-2), 47–103 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Denning, D.E., Denning, P.: Certification of programs for secure information flow. Communications of the ACM 20(7), 504–513 (1977)zbMATHCrossRefGoogle Scholar
  10. 10.
    Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: Proc. of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), pp. 186–197. ACM-Press, NY (2004)CrossRefGoogle Scholar
  11. 11.
    Giacobazzi, R., Mastroeni, I.: Proving abstract non-interference. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 280–294. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Giacobazzi, R., Mastroeni, I.: Adjoining declassification and attack models by abstract interpretation. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 295–310. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Giacobazzi, R., Mastroeni, I.: Generalized abstract non-interference for automata. In: Gorodetsky, V., Kotenko, I., Skormin, V.A. (eds.) MMM-ACNS 2005. LNCS, vol. 3685, pp. 221–234. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. of the ACM. 47(2), 361–416 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Hunt, S., Mastroeni, I.: The PER model of abstract non-interference. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 171–185. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Joshi, R., Leino, K.R.M.: A semantic approach to secure information flow. Science of Computer Programming 37, 113–138 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    Morgado, J.: Some results on the closure operators of partially ordered sets. Portug. Math. 19(2), 101–139 (1960)zbMATHMathSciNetGoogle Scholar
  19. 19.
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. on selected ares in communications 21(1), 5–19 (2003)CrossRefGoogle Scholar
  20. 20.
    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
  21. 21.
    Skalka, C., Smith, S.: Static enforcement of security with types. In: ICFP 2000, pp. 254–267. ACM Press, New York (2000)Google Scholar
  22. 22.
    Volpano, D.: Safety versus secrecy. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 303–311. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  23. 23.
    Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. Journal of Computer Security 7(2,3), 231–253 (1999)Google Scholar
  24. 24.
    Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(2,3), 167–187 (1996)Google Scholar
  25. 25.
    Zanardini, D.: Higher-order abstract non-interference. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 417–432. Springer, Heidelberg (2005) (to appear)CrossRefGoogle Scholar
  26. 26.
    Zdancewic, S., Myers, A.C.: Robust declassification. In: Proc. of the IEEE Computer Security Foundations Workshop, pp. 15–23. IEEE Computer Society Press, Los Alamitos (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Roberto Giacobazzi
    • 1
  • Isabella Mastroeni
    • 2
  1. 1.Dipartimento di InformaticaUniversità di VeronaVeronaItaly
  2. 2.Department of Computing and InformationSciences – Kansas State UniversityManhattanUSA

Personalised recommendations