Verifiable functional purity in java

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verifiable functional purity in java

Full text

Pdf (251 KB)

Source

Conference on Computer and Communications Security archive
Proceedings of the 15th ACM conference on Computer and communications security table of contents

Alexandria, Virginia, USA

SESSION: Software security 2 table of contents

Pages 161-174

Year of Publication: 2008

ISBN:978-1-59593-810-7

Authors

Matthew Finifter	University of California, Berkeley, Berkeley, CA, USA
Adrian Mettler	University of California, Berkeley, Berkeley, CA, USA
Naveen Sastry	University of California, Berkeley, Berkeley, CA, USA
David Wagner	University of California, Berkeley, Berkeley, CA, USA

Sponsors

ACM: Association for Computing Machinery
SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 13, Downloads (12 Months): 213, Citation Count: 0

Additional Information:

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/1455770.1455793 What is a DOI?

Warning: The download time has expired please click on the item to try again.

ABSTRACT

Proving that particular methods within a code base are functionally pure--deterministic and side-effect free--would aid verification of security properties including function invertibility, reproducibility of computation, and safety of untrusted code execution. Until now it has not been possible to automatically prove a method is functionally pure within a high-level imperative language in wide use, such as Java. We discuss a technique to prove that methods are functionally pure by writing programs in a subset of Java called Joe-E; a static verifier ensures that programs fall within the subset. In Joe-E, pure methods can be trivially recognized from their method signature. To demonstrate the practicality of our approach, we refactor an AES library, an experimental voting machine implementation, and an HTML parser to use our techniques. We prove that their top-level methods are verifiably pure and show how this provides high-level security guarantees about these routines. Our approach to verifiable purity is an attractive way to permit functional-style reasoning about security properties while leveraging the familiarity, convenience, and legacy code of imperative languages.

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	Michael Backes , Markus Durmuth , Dominique Unruh, Information Flow in the Peer-Reviewing Process, Proceedings of the 2007 IEEE Symposium on Security and Privacy, p.187-191, May 20-23, 2007 [doi>10.1109/SP.2007.24]
	2	John Barnes, High Integrity Software: The SPARK Approach to Safety and Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
	3	M. Barnett, K.R. Leino, and W. Schulte. The Spec# programming system: An overview. In Proceedings of Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), 2004.
	4	Daniel J. Bernstein, Some thoughts on security after ten years of qmail 1.0, Proceedings of the 2007 ACM workshop on Computer security architecture, p.1-10, November 02-02, 2007, Fairfax, Virginia, USA [doi>10.1145/1314466.1314467]
	5	W. Bright. D language 2.0. http://www.digitalmars.com/d/2.0/.
	6	L. Brown. AEScalc. http://www.unsw.adfa.edu.au/~lpb/src/AEScalc/AEScalc.jar.
	7	Lilian Burdy , Yoonsik Cheon , David R. Cok , Michael D. Ernst , Joseph R. Kiniry , Gary T. Leavens , K. Rustan M. Leino , Erik Poll, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.3, p.212-232, June 2005 [doi>10.1007/s10009-004-0167-4]
	8	Y. Cheon and G. Leavens. A runtime assertion checker for the Java Modeling Language, 2002.
	9	T. Close and S. Butler. Waterken server. http://waterken.sourceforge.net/.
	10	Norman Hardy, KeyKOS architecture, ACM SIGOPS Operating Systems Review, v.19 n.4, p.8-25, October 1985 [doi>10.1145/858336.858337]
	11	HTML4 Test Suite. http://www.w3.org/MarkUp/Test/HTML401/current/.
	12	R. Ierusalimschy and N. de La Rocque Rodriguez. Side-effect free functions in object-oriented languages. Comput. Lang., 21(3/4):129--146, 1995.
	13	M. Frans Kaashoek , Dawson R. Engler , Gregory R. Ganger , Hector M. Briceño , Russell Hunt , David Mazières , Thomas Pinckney , Robert Grimm , John Jannotti , Kenneth Mackenzie, Application performance and flexibility on exokernel systems, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.52-65, October 05-08, 1997, Saint Malo, France
	14	B. W. Lampson , J. J. Horning , R. L. London , J. G. Mitchell , G. J. Popek, Report on the programming language Euclid, ACM SIGPLAN Notices, v.12 n.2, p.1-79, February 1977 [doi>10.1145/954666.971189]
	15	G. Leavens and Y. Cheon. Design by contract with JML, 2003.
	16	A. Mettler and D. Wagner. The Joe-E language specification, version 1.0. Technical Report UCB/EECS-2008-91, EECS Department, University of California, Berkeley, August 7, 2008.
	17	Bertrand Meyer, Eiffel: the language, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
	18	Mark Samuel Miller , Jonathan S. Shapiro, Robust composition: towards a unified approach to access control and concurrency control, Johns Hopkins University, Baltimore, MD, 2006
	19	Andrew C. Myers , Barbara Liskov, A decentralized model for information flow control, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.129-142, October 05-08, 1997, Saint Malo, France
	20	D. Oswald, S. Raha, I. Macfarlane, and D. Walters. HTMLParser 1.6. http://htmlparser.sourceforge.net/.
	21	Atanas Rountev, Precise Identification of Side-Effect-Free Methods in Java, Proceedings of the 20th IEEE International Conference on Software Maintenance, p.82-91, September 11-14, 2004
	22	Algis Rudys , Dan S. Wallach, Termination in language-based systems, ACM Transactions on Information and System Security (TISSEC), v.5 n.2, p.138-168, May 2002 [doi>10.1145/505586.505589]
	23	A. Salcianu and M.C. Rinard. Purity and side effect analysis for java programs. In VMCAI, pages 199--215, 2005.
	24	Verifying Security Properties in Electronic Voting Machines. PhD thesis, University of California at Berkeley, 2007.
	25	F. Sauer. Eclipse metrics plugin 1.3.6. http://metrics.sourceforge.net/.
	26	Matthew S. Tschantz , Michael D. Ernst, Javari: adding reference immutability to Java, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	27	Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
	28	K.-P. Yee and M. Miller. Auditors: An extensible, dynamic code verification mechanism, 2003. http://www.erights.org/elang/kernel/auditors/index.html.