Automated Analysis of Java Methods for Confidentiality

  • Pavol Černý
  • Rajeev Alur
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


We address the problem of analyzing programs such as J2ME midlets for mobile devices, where a central correctness requirement concerns confidentiality of data that the user wants to keep secret. Existing software model checking tools analyze individual program executions, and are not applicable to checking confidentiality properties that require reasoning about equivalence among executions. We develop an automated analysis technique for such properties. We show that both over- and under- approximation is needed for sound analysis. Given a program and a confidentiality requirement, our technique produces a formula that is satisfiable if the requirement holds. We evaluate the approach by analyzing bytecode of a set of Java (J2ME) methods.


Equivalence Capture Loop Unrollings Weak Precondition Phone Book Existential Formula 
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.


  1. 1.
    JavaTM ME Developer’s Library 2.0,
  2. 2.
    WALA - Watson libraries for analyses,
  3. 3.
    JSR 118 Expert Group. Mobile Information Device Profile for J2ME 2.1 (2007)Google Scholar
  4. 4.
    Alur, R., Černý, P., Chaudhuri, S.: Model checking on trees with path equivalences. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 664–678. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Alur, R., Černý, P., Zdancewic, S.: Preserving secrecy under refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 107–118. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Amtoft, T., Banerjee, A.: Verification condition generation for conditional information flow. In: Proc. of FMSE 2007, pp. 2–11 (2007)Google Scholar
  7. 7.
    Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: Proc. POPL 2002, pp. 1–3 (2002)Google Scholar
  8. 8.
    Bryans, J., Koutny, M., Mazaré, L., Ryan, P.: Opacity generalised to transition systems. Int. J. Inf. Sec. 7(6), 421–435 (2008)CrossRefGoogle Scholar
  9. 9.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL 1977, Los Angeles, California, pp. 238–252 (1977)Google Scholar
  10. 10.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. of POPL 1978, pp. 84–97 (1978)Google Scholar
  11. 11.
    Dam, M.: Decidability and proof systems for language-based noninterference relations. In: POPL 2006, pp. 67–78 (2006)Google Scholar
  12. 12.
    Dam, M., Giambiagi, P.: Confidentiality for mobile code: The case of a simple payment protocol. In: Proc. of CSFW 2000, pp. 233–244 (2000)Google Scholar
  13. 13.
    Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253–291 (1997)CrossRefGoogle Scholar
  14. 14.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  16. 16.
    Gray, J.: Probabilistic interference. In: Proc. of SP 1990, pp. 170–179 (1990)Google Scholar
  17. 17.
    Gulavani, B., Rajamani, S.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 474–488. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Halpern, J., O’Neill, K.: Secrecy in multiagent systems. In: Proc. of CSFW 2002, pp. 32–46 (2002)Google Scholar
  19. 19.
    Hammer, C., Krinke, J., Nodes, F.: Intransitive noninterference in dependence graphs. In: Proc. of ISoLA 2006, pp. 136–145 (2006)Google Scholar
  20. 20.
    Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19, 31–100 (2006)CrossRefzbMATHGoogle Scholar
  22. 22.
    Myers, A.: JFlow: Practical mostly-static information flow control. In: Proc. of POPL 1999, pp. 228–241 (1999)Google Scholar
  23. 23.
    O’Connor, J.: Attack surface analysis of Blackberry devices. White Paper: Symantec security response (2007)Google Scholar
  24. 24.
    Popeea, C., Chin, W.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331–345. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  25. 25.
    Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)CrossRefGoogle Scholar
  26. 26.
    Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: CSFW 2005, pp. 255–269 (2005)Google Scholar
  27. 27.
    Sankaranarayanan, S., Ivancic, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 3–17. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  28. 28.
    Schneider, F. (ed.): Trust in Cyberspace. National Academy Press (1999)Google Scholar
  29. 29.
    Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. ACM Trans. Softw. Eng. Methodol. 15(4), 410–457 (2006)CrossRefGoogle Scholar
  30. 30.
    van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. Electr. Notes Theor. Comput. Sci. 168, 61–75 (2007)CrossRefGoogle Scholar
  31. 31.
    Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. Journal of Computer Security 7(1) (1999)Google Scholar
  32. 32.
    Winskel, G.: The formal semantics of programming languages: An Introduction. MIT Press, Cambridge (1993)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Pavol Černý
    • 1
  • Rajeev Alur
    • 1
  1. 1.University of PennsylvaniaUSA

Personalised recommendations