Information Flow Analysis in Logical Form

1. Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 147–160 (1999)

   Google Scholar 

2. Amtoft, T., Banerjee, A.: Information flow analysis in logical form. Technical Report CIS TR 2004-3, Kansas State University (April 2004)

   Google Scholar 

3. Andrews, G.R., Reitman, R.P.: An axiomatic approach to information flow in programs. ACM Transactions on Programming Languages and Systems 2(1), 56–75 (1980)

   Article  MATH  Google Scholar 

4. Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a Java-like language. In: IEEE Computer Security Foundations Workshop (CSFW), pp. 253–270. IEEE Computer Society Press, Los Alamitos (2002)

   Google Scholar 

5. Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: IEEE Computer Security Foundations Workshop, CSFW (2004) (to appear)

   Google Scholar 

6. Clark, D., Hankin, C., Hunt, S.: Information flow for Algol-like languages. Computer Languages 28(1), 3–28 (2002)

   MATH  Google Scholar 

7. Cohen, E.S.: Information transmission in sequential programs. In: DeMillo, R.A., Dobkin, D.P., Jones, A.K., Lipton, R.J. (eds.) Foundations of Secure Computation, pp. 297–335. Academic Press, London (1978)

   Google Scholar 

8. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 238–252. ACM Press, New York (1977)

   Google Scholar 

9. Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: Proceedings of the ACM Symposium on Artificial Intelligence and Programming Languages, August 1977. SIGPLAN Notices, vol. 12, pp. 1–12. ACM Press, New York (1977)

   Chapter  Google Scholar 

10. Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. Technical Report 2004-01, Department of Computing Science, Chalmers University of Technology and Göteborg University (2004); A fuller version of a paper appearing in Workshop on Issues in the Theory of Security (2003)

    Google Scholar 

11. Denning, D., Denning, P.: Certification of programs for secure information flow. Communications of the ACM 20(7), 504–513 (1977)

    Article  MATH  Google Scholar 

12. Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 186–197 (2004)

    Google Scholar 

13. Goguen, J., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, pp. 11–20 (1982)

    Google Scholar 

14. Heintze, N., Riecke, J.G.: The SLam calculus: programming with secrecy and integrity. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 365–377 (1998)

    Google Scholar 

15. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

16. Hunt, S., Sands, D.: Binding time analysis: A new PERspective. In: Partial Evaluation and Semantics-Based Program Manipulation (PEPM 1991). Sigplan Notices, vol. 26(9), pp. 154–165 (1991)

    Google Scholar 

17. Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 14–26 (2001)

    Google Scholar 

18. Joshi, R., Leino, K.R.M.: A semantic approach to secure information flow. Science of Computer Programming 37, 113–138 (2000)

    Article  MATH  MathSciNet  Google Scholar 

19. McCullough, D.: Specifications for multi-level security and a hook-up. In: IEEE Symposium on Security and Privacy, April 27-29, pp. 161–166 (1987)

    Google Scholar 

20. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999), Web page at www.imm.dtu.dk/~riis/PPA/ppa.html

    MATH  Google Scholar 

21. O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

22. O’Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 268–280 (2004)

    Google Scholar 

23. Ørbæk, P., Palsberg, J.: Trust in the λ-calculus. Journal of Functional Programming 7(6), 557–591 (1997)

    Article  MathSciNet  Google Scholar 

24. Pottier, F., Simonet, V.: Information flow inference for ML. ACM Transactions on Programming Languages and Systems 25(1), 117–158 (2003)

    Article  Google Scholar 

25. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 55–74. IEEE Computer Society Press, Los Alamitos (2002)

    Chapter  Google Scholar 

26. Sabelfeld, A., Myers, A.: A model for delimited information release. In: Proceedings of the International Symposium on Software Security, ISSS 2003 (2004) (to appear)

    Google Scholar 

27. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)

    Article  Google Scholar 

28. Sabelfeld, A., Sands, D.: A Per model of secure information flow in sequential programs. Higher-order and Symbolic Computation 14(1), 59–91 (2001)

    Article  MATH  Google Scholar 

29. Volpano, D., Smith, G.: A type-based approach to program security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 607–621. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

Download references