Security-Aware Program Transformations

  • Massimo Bartoletti
  • Pierpaolo Degano
  • Gian Luigi Ferrari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2841)


Stack inspection is a basic mechanism for implementing language based security. Stack inspection is time consuming and may prevent from code optimization. A static analysis is presented that safely approximates the access rights granted at run-rime. Stack inspection optimizations are then possible, along with program transformations.


Access Control Security Policy Operational Semantic Access Control Policy Program Transformation 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Burrows, M., Lampson, B., Plotkin, G.: A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems 4(15), 706–734 (1993)CrossRefGoogle Scholar
  2. 2.
    Bartoletti, M., Degano, P., Ferrari, G.: Stack inspection and program transformations (2003),
  3. 3.
    Bartoletti, M., Degano, P., Ferrari, G.: Static analysis for eager stack inspection. In: Workshop on Formal Techniques for Java-like Programs, FTfJP 2003 (2003)Google Scholar
  4. 4.
    Besson, F., Jensen, T., Le Métayer, D., Thorn, T.: Model checking security properties of control flow graphs. Journal of computer security 9, 217–250 (2001)Google Scholar
  5. 5.
    Choi, J.-D., Grove, D., Hind, M., Sarkar, V.: Efficient and precise modeling of exceptions for the analysis of Java programs. In: Workshop on Program Analysis For Software Tools and Engineering (1999)Google Scholar
  6. 6.
    Clemens, J., Felleisen, M.: A tail-recursive semantics for stack inspections. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 22–37. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Fournet, C., Gordon, A.D.: Stack inspection: theory and variants. ACM Transactions on Programming Languages and Systems (TOPLAS) 25(3), 360–399 (2003)CrossRefGoogle Scholar
  8. 8.
    Gong, L.: Inside Java 2 platform security: architecture, API design, and implementation. Addison-Wesley, Reading (1999)Google Scholar
  9. 9.
    Gorla, D., Pugliese, R.: Resource access and mobility control with dynamic privileges acquisition. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Grove, D., Chambers, C.: A framework for call graph construction algorithms. ACM Transactions on Programming Languages and Systems (TOPLAS) 23(6), 685–746 (2001)CrossRefGoogle Scholar
  11. 11.
    Kaser, O., Ramakrishnan, C.R.: Evaluating inlining techniques. Computer Languages 24(2), 55–72 (1998)zbMATHCrossRefGoogle Scholar
  12. 12.
    Koved, L., Pistoia, M., Kershenbaum, A.: Access rights analysis for Java. In: Proc. of the 17th ACM conference on Object-oriented programming, systems, languages, and applications (OOPSLA 2002), ACM Press, New York (2002)Google Scholar
  13. 13.
    Lai, C., Gong, L., Koved, L., Nadalin, A., Schemers, R.: User authentication and authorization in the Java platform. In: 15th Annual Computer Security Application Reference, IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  14. 14.
    Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. International Journal of Information Security (2003)Google Scholar
  15. 15.
    Microsoft Corp. .NET Framework Developer’s Guide: Securing ApplicationsGoogle Scholar
  16. 16.
    Nielson, F., Nielson, H.R., Hankin, C.L.: Principles of Program Analysis. Springer, Heidelberg (1999)zbMATHGoogle Scholar
  17. 17.
    Pottier, F., Skalka, C., Smith, S.: A systematic approach to static access control. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 30. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    Sinha, S., Harrold, M.J.: Analysis and testing of programs with exception handling constructs. Software Engineering 26(9), 849–871 (2000)CrossRefGoogle Scholar
  19. 19.
    Souter, A., Pollack, L.: Incremental call graph reanalysis for object-oriented software maintenance. In: IEEE International Conference on Software Maintenance (November 2001)Google Scholar
  20. 20.
    Sundaresan, V., Hendren, L., Razafimahefa, C., Vallée-Rai, R., Lam, P., Gagnon, E., Godin, C.: Practical virtual method call resolution for Java. In: Proc. of the 2000 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA 2000). SIGPLAN Notices, vol. 35(10), ACM Press, New York (2000)Google Scholar
  21. 21.
    Tip, F., Palsberg, J.: Scalable propagation-based call graph construction algorithms. In: Proc. of the 2000 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications, OOPSLA 2000 (2000)Google Scholar
  22. 22.
    Wallach, D.S., Appel, A.W., Felten, E.W.: SAFKASI: a security mechanism for language-based systems. ACM TOSEM 9(4), 341–378 (2001)CrossRefGoogle Scholar
  23. 23.
    Wille, C.: Presenting C\(\sharp\). SAMS Publishing, USA (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Massimo Bartoletti
    • 1
  • Pierpaolo Degano
    • 1
  • Gian Luigi Ferrari
    • 1
  1. 1.Dipartimento di InformaticaUniversità di PisaItaly

Personalised recommendations