Enforcing resource bounds via static verification of dynamic checks

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Enforcing resource bounds via static verification of dynamic checks

Full text

Pdf (425 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 29 , Issue 5 (August 2007) table of contents
Special Issue ESOP'05

Article No. 28

Year of Publication: 2007

ISSN:0164-0925

Authors

Ajay Chander	DoCoMo Labs USA, Palo Alto, CA
David Espinosa	DoCoMo Labs USA, Palo Alto, CA
Nayeem Islam	DoCoMo Labs USA, Palo Alto, CA
Peter Lee	Carnegie Mellon University, Pittsburgh, PA
George C. Necula	University of California, Berkeley, CA

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 56, Citation Count: 1

Additional Information:

abstract references cited by 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/1275497.1275503 What is a DOI?

ABSTRACT

We show how to limit a program's resource usage in an efficient way, using a novel combination of dynamic checks and static analysis. Usually, dynamic checking is inefficient due to the overhead of checks, while static analysis is difficult and rejects many safe programs. We propose a hybrid approach that solves these problems. We split each resource-consuming operation into two parts. The first is a dynamic check, called reserve. The second is the actual operation, called consume, which does not perform any dynamic checks. The programmer is then free to hoist and combine reserve operations. Combining reserve operations reduces their overhead, while hoisting reserve operations ensures that the program does not run out of resources at an inconvenient time. A static verifier ensures that the program reserves resources before it consumes them. This verification is both easier and more flexible than an a priori static verification of resource usage. We present a sound and efficient static verifier based on Hoare logic and linear inequalities. As an example, we present a version of tar written in Java.

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	Chander, A., Espinosa, D., Islam, N., Lee, P., and Necula, G. 2005. JVer: A Java verifier. In Proceedings of the Conference on Computer Aided Verification (Edinburgh, Scotland).
	2	Chander, A., Mitchell, J., and Shin, I. 2001. Mobile code security by Java bytecode instrumentation. In Proceedings of the DARPA Information Survivability Confernce and Exposition.
	3	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]
	4	Karl Crary , Stephnie Weirich, Resource bound certification, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.184-198, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325716]
	5	Grzegorz Czajkowski , Thorsten von Eicken, JRes: a resource accounting interface for Java, Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.21-35, October 18-22, 1998, Vancouver, British Columbia, Canada
	6	Detlefs, D., Nelson, G., and Saxe, J. 2003. Simplify: A theorem prover for program checking. Tech. Rep. HPL-2003-148, HP Laboratories. July.
	7	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	8	Endres, T. 2003. Java tar 2.5. http://www.trustice.com.
	9	Ú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]
	10	Evans, D. and Twyman, A. 1999. Flexible policy-directed code safety. In Proceedings of the IEEE Symposium on Security and Privacy (Oakland, CA).
	11	Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
	12	Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
	13	Li Gong, Inside Java 2 platform security architecture, API design, and implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
	14	Rajiv Gupta, Optimizing array bound checks using flow analysis, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.135-150, March–Dec. 1993 [doi>10.1145/176454.176507]
	15	Martin Hofmann , Steffen Jost, Static prediction of heap space usage for first-order functional programs, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.185-197, January 15-17, 2003, New Orleans, Louisiana, USA
	16	Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
	17	Kim, M., Kannan, S., Lee, I., and Sokolsky, O. 2001. Java-MaC: A run-time assurance tool for Java programs. Electron. Not. Theor. Comput. Sci. 55, 2.
	18	John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
	19	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]
	20	George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
	21	George C. Necula , S. P. Rahul, Oracle-based checking of untrusted software, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.142-154, January 2001, London, United Kingdom
	22	Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
	23	Pandey, R. and Hashii, B. 2000. Providing fine-grained access control for Java programs via binary editing. Concurrency: Pract. Exper. 12, 1405--1430.
	24	Patel, P. and Lepreau, J. 2003. Hybrid resource control of active extensions. In Proceedings of the IEEE Conference on Open Architectures and Network Programming (San Francisco, CA).
	25	Natarajan Shankar , Harald Rueß, Combining Shostak Theories, Proceedings of the 13th International Conference on Rewriting Techniques and Applications, p.1-18, July 22-24, 2002
	26	Robert E. Shostak, Deciding Combinations of Theories, Journal of the ACM (JACM), v.31 n.1, p.1-12, Jan. 1984 [doi>10.1145/2422.322411]
	27	Joseph C. Vanderwaart , Karl Crary, Automated and certified conformance to responsiveness policies, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.79-90, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040302]
	28	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]