Compile-time detection of information flow in sequential programs

  • Jean-Pierre Banâtre
  • Ciarán Bryce
  • Daniel Le Métayer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 875)


We give a formal definition of the notion of information flow for a simple guarded command language. We propose an axiomatisation of security properties based on this notion of information flow and we prove its soundness with respect to the operational semantics of the language. We then identify the sources of non determinism in proofs and we derive in successive steps an inference algorithm which is both sound and complete with respect to the inference system.


formal verification program analysis verification tools computer security information flow 


  1. 1.
    Abramsky (S.) and Hankin (C. L.), “Abstract interpretation of declarative languages”, Ellis Horwood, 1987.Google Scholar
  2. 2.
    Aho (A. V.), Sethi (R.) and Ullman (J. D.), “Compilers: Principles, Techniques and Tools”, Addison Wesley, Reading, Mass, 1986.Google Scholar
  3. 3.
    Andrews (G.R.), Reitman (R.P.), “An Axiomatic Approach to Information Flow in Programs”, in ACM Transactions on Programming Languages and Systems, volume 2 (1), January 1980, pages 504–513.CrossRefGoogle Scholar
  4. 4.
    Banâtre (J.-P.) and C. Bryce, (C.), “A security proof system for networks of communicating processes”, Irisa research report, no 744, June 1993.Google Scholar
  5. 5.
    Banâtre (J.-P.) and C. Bryce, (C.), and Le Métayer (D.), “Mechanical proof of security properties”, Irisa research report, no 825, May 1994.Google Scholar
  6. 6.
    Cohen (E.), “Information Transmission in Computational Systems”, in Proceedings ACM Symposium on Operating System Principles, 1977, pages 133–139.Google Scholar
  7. 7.
    Cytron (R.), Ferrante (J.), Rosen (B. K.) and Wegman (M. N.), “Efficiently computing Static Single Assignment form and the control dependence graph”, in A CM Transactions on Programming Languages and Systems, Vol. 13, No 4, October 1991, pages 451–490.CrossRefGoogle Scholar
  8. 8.
    Denning (D.E.), Secure Information Flow in Computer Systems, Phd Thesis, Purdue University, May 1975.Google Scholar
  9. 9.
    Denning (D.E.), Denning (P.J.), “Certification of Programs for Secure Information Flow”, in Communications of the ACM, volume 20 (7), July 1977, pages 504–513.CrossRefGoogle Scholar
  10. 10.
    Hankin (C. L.) and Le Métayer (D.), “Deriving Algorithms from Type Inference Systems: Application to Strictness Analysis”, in Proceedings ACM POPL, 1994, pages 202–212.Google Scholar
  11. 11.
    Hoare (C.A.R.), Communicating Sequential Processes, Prentice-Hall London, 1985.Google Scholar
  12. 12.
    Jones (A.), Lipton (R.), “The Enforcement of Security Policies for Computations”, in Proceedings of the 5th Symposium on Operating System Principles, November 1975, pages 197–206.Google Scholar
  13. 13.
    Kennedy K. W., “A Survey of Data Flow Analysis Techniques”, in Program Flow Analysis, S. S. Muchnik and N. D. Jones, Eds, Prentice-Hall, Englewood Cliffs, NJ, 1981.Google Scholar
  14. 14.
    Lampson (B.), “A note on the Confinement Problem”, in Communications of the ACM, volume 16 (10), October 1973, pages 613–615.CrossRefGoogle Scholar
  15. 15.
    Landi (W.) and Ryder (B. G.), “Pointer-induced aliasing: a problem classification”, in Proceedings ACM POPL, 1991, pages 93–103.Google Scholar
  16. 16.
    Landi (W.) and Ryder (B. G.), “A safe approximate algorithm for interprocedural pointer aliasing”, in Proceedings ACM Programming Language Design and Implementation, 1992, pages 235–248.Google Scholar
  17. 17.
    McLean (J.), “A Formal Method for the Abstract Specification of Software”, in Journal of the ACM, 31, July 1984, pages 600–627.CrossRefGoogle Scholar
  18. 18.
    McLean (J.), “Proving Non-interference and Functional Correctness Using Traces”, in Journal of Computer Security, 1(1), Spring 1992, pages 37–57.Google Scholar
  19. 19.
    Mizuno (M.), Schmidt (D.), “A Security Control Flow Control Algorithm and Its Denotational Semantics Correctness Proof”, Journal on the Formal Aspects of Computing, 4 (6A), november 1992, pages 722–754.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Jean-Pierre Banâtre
    • 1
  • Ciarán Bryce
    • 1
  • Daniel Le Métayer
    • 1
  1. 1.IRISARennes CedexFrance

Personalised recommendations