Abstract
This paper investigates a technique for using automated program verifiers to check conformance with information flow policy, in particular for programs acting on shared, dynamically allocated mutable heap objects. The technique encompasses rich policies with forms of declassification and supports modular, invariant-based verification of object-oriented programs. The technique is based on the known idea of self-composition, whereby noninterference for a command is reduced to an ordinary partial correctness property of the command sequentially composed with a renamed copy of itself. The first contribution is to extend this technique to encompass heap objects, which is difficult because textual renaming is inapplicable. The second contribution is a systematic means to validate transformations on self-composed programs. Certain transformations are needed for effective use of existing automated program verifiers and they exploit conservative flow inference, e.g., from security type inference. Experiments with the technique using ESC/Java2 and Spec# verifiers are reported.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: ACM Symposium on Principles of Programming Languages (POPL) (2006)
Amtoft, T., Banerjee, A.: Information flow analysis in logical form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 100–115. Springer, Heidelberg (2004)
Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM 52(6), 894–960 (2005)
Banerjee, A., Naumann, D.A.: Stack-based access control for secure information flow. Journal of Functional Programming 15(2), 131–177 (2005)
Banerjee, A., Naumann, D.A.: A logical account of secure declassification (extended abstract) (submitted, 2006)
Barnett, M., M. Leino, K.R., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: IEEE Computer Security Foundations Workshop (CSFW), pp. 100–114 (2004)
Barthe, G., Rezk, T.: Non-interference for a JVM-like language. In: Fähndrich, M. (ed.) Proceedings of TLDI 2005, pp. 103–112. ACM Press, New York (2005)
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 14–25 (2004)
Cohen, E.S.: Information transmission in sequential programs. In: Richard, A.K.J., DeMillo, A., Dobkin, D.P., Lipton, R.J. (eds.) Foundations of Secure Computation, pp. 297–335. Academic Press, London (1978)
Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005)
Darvas, A., Müller, P.: Reasoning about method calls in JML specifications. In: ECOOP workshop on Formal Techniques for Java-like Programs (2005)
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)
Denning, D.E.: Cryptography and Data Security. Addison-Wesley, Reading (1982)
Dufay, G., Felty, A.P., Matwin, S.: Privacy-sensitive information flow with JML. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol. 3632, pp. 116–130. Springer, Heidelberg (2005)
Gries, D.: Data refinement and the tranform. In: Broy, M. (ed.) Program Design Calculi. International Summer School at Marktoberdorf. Springer, Heidelberg (1993)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 58–70 (2002)
Jacobs, B., Poll, E.: Java program verification at nijmegen: Developments and perspective. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 134–153. Springer, Heidelberg (2004)
Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 262–284. Springer, Heidelberg (2003)
Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Technical Report 424, Department of Computer Science, ETH Zurich (2004)
Myers, A.C.: JFlow: Practical mostly-static information flow control. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 228–241 (1999)
Naumann, J.D.A.: Verifying a secure information flow analyzer. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 211–226. Springer, Heidelberg (2005)
Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theoretical Computer Science (to appear, 2006)
Pottier, F., Simonet, V.: Information flow inference for ML. ACM Transactions on Programming Languages and Systems 25(1), 117–158 (2003)
Reynolds, J.C.: The Craft of Programming. Prentice-Hall, Englewood Cliffs (1981)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: IEEE Logic in Computer Science (LICS), pp. 55–74 (2002)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)
Sabelfeld, A., Sands, D.: A per model of secure information flow in sequential programs. Higher-order and Symbolic Computation 14(1), 59–91 (2001)
Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: IEEE Computer Security Foundations Workshop (CSFW) (2005)
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)
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)
Yang, H.: Relational separation logic. Theoretical Comput. Sci. (to appear, 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Naumann, D.A. (2006). From Coupling Relations to Mated Invariants for Checking Information Flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds) Computer Security – ESORICS 2006. ESORICS 2006. Lecture Notes in Computer Science, vol 4189. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11863908_18
Download citation
DOI: https://doi.org/10.1007/11863908_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44601-9
Online ISBN: 978-3-540-44605-7
eBook Packages: Computer ScienceComputer Science (R0)