Local policies for resource usage analysis

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Local policies for resource usage analysis

Full text

Pdf (563 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 31 , Issue 6 (August 2009) table of contents

Article No. 23

Year of Publication: 2009

ISSN:0164-0925

Authors

Massimo Bartoletti	Università degli Studi di Cagliari, and Università di Pisa, Pisa, Italy
Pierpaolo Degano	Università di Pisa, Pisa, Italy
Gian-Luigi Ferrari	Università di Pisa, Pisa, Italy
Roberto Zunino	Università degli Studi di Trento, Povo, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 38, Downloads (12 Months): 97, Citation Count: 0

Additional Information:

appendices and supplements abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1552309.1552313 What is a DOI?

APPENDICES and SUPPLEMENTS

Bartoletti Appendix

Online appendix to local policies for resource usage analysis. The appendix supports the information on article 23.

ABSTRACT

An extension of the λ-calculus is proposed, to study resource usage analysis and verification. It features usage policies with a possibly nested, local scope, and dynamic creation of resources. We define a type and effect system that, given a program, extracts a history expression, that is, a sound overapproximation to the set of histories obtainable at runtime. After a suitable transformation, history expressions are model-checked for validity. A program is resource-safe if its history expression is verified valid: If such, no runtime monitor is needed to safely drive its executions.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Bartoletti, M. 2009. Usage automata. In Proceedings of the Workshop on Issues in the Theory of Security. Lecture Notes in Computer Science, vol. 5511. Springer, Berlin, 52--69.
	2	Bartoletti, M., Costa, G., Degano, P., Martinelli, F., and Zunino, R. 2009. Securing Java with local policies. J. Object Technol. 8, 4, 5--32.
	3	Massimo Bartoletti , Pierpaolo Degano , Gian Luigi Ferrari, Stack inspection and secure program transformations, International Journal of Information Security, v.2 n.3, p.187-217, August 2004 [doi>10.1007/s10207-004-0038-8]
	4	Bartoletti, M., Degano, P., and Ferrari, G.-L. 2005a. Checking risky events is enough for local policies. In Proceedings of the 9th Italian Conference on Theoretical Computer Science (ICTCS). Lecture Notes in Computer Science, vol. 3701. Springer, Berlin, 97--112.
	5	Massimo Bartoletti , Pierpaolo Degano , Gian Luigi Ferrari, Enforcing Secure Service Composition, Proceedings of the 18th IEEE workshop on Computer Security Foundations, p.211-223, June 20-22, 2005 [doi>10.1109/CSFW.2005.17]
	6	Bartoletti, M., Degano, P., and Ferrari, G.-L. 2005c. History-based access control with local policies. In Proceedings of the 8th Foundations of Software Science and Computational Structures (FOSSACS). Lecture Notes in Computer Science, vol. 3441. Springer, Berlin, 316--332.
	7	Massimo Bartoletti , Pierpaolo Degano , Gian Luigi Ferrari, Types and Effects for Secure Service Orchestration, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.57-69, July 05-07, 2006 [doi>10.1109/CSFW.2006.31]
	8	Bartoletti, M., Degano, P., Ferrari, G.-L., and Zunino, R. 2007. Types and effects for resource usage analysis. In Proceedings of the 10th Foundations of Software Science and Computational Structures (FOSSACS'07). Lecture Notes in Computer Science, vol. 4423. Springer, Berlin, 32--47.
	9	Massimo Bartoletti , Pierpaolo Degano , Gian Luigi Ferrari , Roberto Zunino, Model Checking Usage Policies, Trustworthy Global Computing: 4th International Symposium, TGC 2008, Barcelona, Spain, November 3-4, 2008, Revised Selected Papers, Springer-Verlag, Berlin, Heidelberg, 2009 [doi>10.1007/978-3-642-00945-7_2]
	10	Bartoletti, M. and Zunino, R. 2008. LocUsT: A tool for checking usage policies. Tech. rep. TR-08-07, Dipartimento Informatica, Universita Pisa. http://compass2.di.unipi.it/TR/Files/TR-08-07.pdf.gz.
	11	Bauer, L., Ligatti, J., and Walker, D. 2002. More enforceable security policies. In Proceedings of the Workshop on Foundations of Computer Security (FCS).
	12	Lujo Bauer , Jay Ligatti , David Walker, Composing security policies with polymer, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
	13	Bergstra, J. A. and Klop, J. W. 1985. Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37, 77--121.
	14	Frédéric Besson , Thomas De Grenier DeLatour , Thomas Jensen, Interfaces for stack inspection, Journal of Functional Programming, v.15 n.2, p.179-217, March 2005 [doi>10.1017/S0956796804005465]
	15	Frédéric Besson , Thomas Jensen , Daniel Le Métayer , Tommy Thorn, Model checking security properties of control flow graphs, Journal of Computer Security, v.9 n.3, p.217-250, January 2001
	16	Julian C. Bradfield, On the Expressivity of the Modal Mu-Calculus, Proceedings of the 13th Annual Symposium on Theoretical Aspects of Computer Science, p.479-490, February 22-24, 1996
	17	Sagar Chaki , Sriram K. Rajamani , Jakob Rehof, Types as models: model checking message-passing programs, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.45-57, January 16-18, 2002, Portland, Oregon
	18	Christensen, S. 1993. Decidability and decomposition in process algebras. Ph.D. thesis, Edinburgh University.
	19	Thomas Colcombet , Pascal Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325703]
	20	Mads Dam, On the decidability of process equivalences for the &pgr;-calculus, Theoretical Computer Science, v.183 n.2, p.215-228, Sept. 15, 1997 [doi>10.1016/S0304-3975(96)00325-8]
	21	Úlfar Erlingsson , Fred B. Schneider, SASI enforcement of security policies: a retrospective, Proceedings of the 1999 workshop on New security paradigms, p.87-95, September 22-24, 1999, Caledon Hills, Ontario, Canada [doi>10.1145/335169.335201]
	22	Javier Esparza, On the Decidability of Model Checking for Several µ-calculi and Petri Nets, Proceedings of the 19th International Colloquium on Trees in Algebra and Programming, p.115-129, April 11-13, 1994
	23	Fong, P. W. 2004. Access control by tracking shallow execution history. In Proceedings of the IEEE Symposium on Security and Privacy (S&P'04). IEEE Computer Society, Los Alamitos, 43--55.
	24	Cédric Fournet , Andrew D. Gordon, Stack inspection: Theory and variants, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.3, p.360-399, May 2003 [doi>10.1145/641909.641912]
	25	Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Computability classes for enforcement mechanisms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.1, p.175-205, January 2006 [doi>10.1145/1111596.1111601]
	26	Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.331-342, January 16-18, 2002, Portland, Oregon
	27	Futoshi Iwama , Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis for a functional language with exceptions, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina [doi>10.1145/1111542.1111550]
	28	Naoki Kobayashi, Time regions and effects for resource usage analysis, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
	29	Kozen, D. 1983. Results on the propositional μ-calculus. Theor. Comput. Sci. 27, 333--354.
	30	Marriott, K., Stuckey, P. J., and Sulzmann, M. 2003. Resource usage verification. In Proceedings of the 1st Asian Symposium on Programming Languages and Systems (APLAS'03). Lecture Notes in Computer Science, vol. 2895. Springer, Berlin, 212--229.
	31	Mayr, R. 1998. Decidability and complexity of model-checking problems for infinite-state systems. Ph.D. thesis, Technischen Universität München.
	32	Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, II, Information and Computation, v.100 n.1, p.41-77, Sept. 1992 [doi>10.1016/0890-5401(92)90009-5]
	33	George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
	34	Hanne Riis Nielson , Flemming Nielson, Higher-order concurrent programs with finite communication topology (extended abstract), Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.84-97, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.174538]
	35	Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
	36	Christian Skalka, Trace effects and object orientation, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.139-150, July 11-13, 2005, Lisbon, Portugal [doi>10.1145/1069774.1069787]
	37	Skalka, C. and Smith, S. 2004. History effects and verification. In Proceedings of the 2nd Asian Symposium on Programming Languages and Systems (APLAS'04). Lecture Notes in Computer Science, vol. 3302. Springer, Berlin, 107--128.
	38	Christian Skalka , Scott Smith , David Van horn, Types and trace effects of higher order programs, Journal of Functional Programming, v.18 n.2, p.179-249, March 2008 [doi>10.1017/S0956796807006466]
	39	Talpin, J.-P. and Jouvelot, P. 1992. Polymorphic type, region and effect inference. J. Functional Program. 2, 3, 245--271.
	40	Tan, G., Ou, X., and Walker, D. 2003. Resource usage analysis via scoped methods. In Proceedings of the Foundations of Object-Oriented Languages.
	41	Peter Thiemann, Program specialization for execution monitoring, Journal of Functional Programming, v.13 n.3, p.573-600, May 2003 [doi>10.1017/S0956796802004586]
	42	David Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.254-267, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325728]
	43	Dan S. Wallach , Andrew W. Appel , Edward W. Felten, SAFKASI: a security mechanism for language-based systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.341-378, Oct. 2000 [doi>10.1145/363516.363520]
	44	Wang, J., Takata, Y., and Seki, H. 2006. HBAC: A model for history-based access control and its model-checking. In Proceedings of the 11th European Symposium on Research in Computer Security (ESORICS'06). Lecture Notes in Computer Science, vol. 4189. Springer, Berlin, 263--278.