research-article

Verifiable functional purity in java

Authors:

Matthew Finifter,

Adrian Mettler,

Naveen Sastry,

David WagnerAuthors Info & Claims

CCS '08: Proceedings of the 15th ACM conference on Computer and communications security

Pages 161 - 174

https://doi.org/10.1145/1455770.1455793

Published: 27 October 2008 Publication History

Get Access

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

[1]

M. Backes, M. Dürmuth, and D. Unruh. Information flow in the peer-reviewing process (extended abstract). In IEEE Symposium on Security and Privacy, Proceedings of SSP'07, pages 187--191, May 2007.

Digital Library

Google Scholar

[2]

J. Barnes. High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2003.

Digital Library

Google Scholar

[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.

Digital Library

Google Scholar

[4]

D.J. Bernstein. Some thoughts on security after ten years of qmail 1.0. In CSAW '07: Proceedings of the 2007 ACM workshop on Computer security architecture, pages 1--10, New York, NY, USA, 2007. ACM.

Digital Library

Google Scholar

[5]

W. Bright. D language 2.0. http://www.digitalmars.com/d/2.0/.

Google Scholar

[6]

L. Brown. AEScalc. http://www.unsw.adfa.edu.au/~lpb/src/AEScalc/AEScalc.jar.

Google Scholar

[7]

L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. Leavens, K.R. Leino, and E. Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT), 7(3):212--232, June 2005.

Digital Library

Google Scholar

[8]

Y. Cheon and G. Leavens. A runtime assertion checker for the Java Modeling Language, 2002.

Google Scholar

[9]

T. Close and S. Butler. Waterken server. http://waterken.sourceforge.net/.

Google Scholar

[10]

N. Hardy. Keykos architecture. SIGOPS Oper. Syst. Rev., 19(4):8--25, 1985.

Digital Library

Google Scholar

[11]

HTML4 Test Suite. http://www.w3.org/MarkUp/Test/HTML401/current/.

Google Scholar

[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.

Digital Library

Google Scholar

[13]

M.F. Kaashoek, D.R. Engler, G.R. Ganger, n. Hector M. Brice, R. Hunt, D. Mazières, T. Pinckney, R. Grimm, J. Jannotti, and K. Mackenzie. Application performance and flexibility on exokernel systems. In SOSP '97: Proceedings of the sixteenth ACM symposium on Operating systems principles, pages 52--65, New York, NY, USA, 1997. ACM.

Digital Library

Google Scholar

[14]

B.W. Lampson, J.J. Horning, R.L. London, J.G. Mitchell, J.G. Mitchell, G.J. Popek, and G.J. Popek. Report on the programming language Euclid. SIGPLAN Not., 12(2):1--79, 1977.

Digital Library

Google Scholar

[15]

G. Leavens and Y. Cheon. Design by contract with JML, 2003.

Google Scholar

[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.

Google Scholar

[17]

B. Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, Englewood Cliffs, NJ, USA,

Digital Library

Google Scholar

[18]

M.S. Miller. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, Baltimore, Maryland, USA, May 2006.

Digital Library

Google Scholar

[19]

A.C. Myers and B. Liskov. A decentralized model for information flow control. In Symposium on Operating Systems Principles, pages 129--142, 1997.

Digital Library

Google Scholar

[20]

D. Oswald, S. Raha, I. Macfarlane, and D. Walters. HTMLParser 1.6. http://htmlparser.sourceforge.net/.

Google Scholar

[21]

Precise identification of side-effect-free methods in java. In ICSM '04: Proceedings of the 20th IEEE International Conference on Software Maintenance, pages 82--91, Washington, DC, USA, 2004. IEEE Computer Society.

Digital Library

Google Scholar

[22]

A. Rudys and D.S. Wallach. Termination in language-based systems. ACM Transactions on Information and System Security, 5(2), May 2002.

Digital Library

Google Scholar

[23]

A. Salcianu and M.C. Rinard. Purity and side effect analysis for java programs. In VMCAI, pages 199--215, 2005.

Digital Library

Google Scholar

[24]

Verifying Security Properties in Electronic Voting Machines. PhD thesis, University of California at Berkeley, 2007.

Google Scholar

[25]

F. Sauer. Eclipse metrics plugin 1.3.6. http://metrics.sourceforge.net/.

Google Scholar

[26]

M.S. Tschantz and M.D. Ernst. Javari: Adding reference immutability to Java. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2005), pages 211--230, San Diego, CA, USA, October 18--20, 2005.

Digital Library

Google Scholar

[27]

P. Wadler. The essence of functional programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1--14, Albequerque, New Mexico, 1992.

Digital Library

Google Scholar

[28]

K.-P. Yee and M. Miller. Auditors: An extensible, dynamic code verification mechanism, 2003. http://www.erights.org/elang/kernel/auditors/index.html.

Google Scholar

Cited By

View all

Zuilhof Bvan Hees RGrelck C(2023)Code Quality Metrics for Functional Features in Modern Object-Oriented LanguagesComposability, Comprehensibility and Correctness of Working Software10.1007/978-3-031-42833-3_10(358-374)Online publication date: 18-Oct-2023
https://doi.org/10.1007/978-3-031-42833-3_10
Koppmann MKudera CPucher MMerzdovnik G(2022)Utilizing Object Capabilities to Improve Web Application SecurityApplied Cybersecurity & Internet Governance10.5604/01.3001.0016.08231:1(1-18)Online publication date: 16-Nov-2022
https://doi.org/10.5604/01.3001.0016.0823
Webster NServetto MHomer M(2022)Using Functional Reactive Programming to Define Safe Actor SystemsProceedings of the 24th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3611096.3611098(4-10)Online publication date: 7-Jun-2022
https://dl.acm.org/doi/10.1145/3611096.3611098
Show More Cited By

Index Terms

Verifiable functional purity in java

Recommendations

Verifiable Functional Encryption
Proceedings, Part II, of the 22nd International Conference on Advances in Cryptology --- ASIACRYPT 2016 - Volume 10032

In light of security challenges that have emerged in a world with complex networks and cloud computing, the notion of functional encryption has recently emerged. In this work, we show that in several applications of functional encryption even those ...
Publicly verifiable ciphertexts
Advances in Security for Communication Networks

In many applications where encrypted traffic flows from an open public domain to a protected private domain there exists a gateway that bridges these two worlds, faithfully forwarding all incoming traffic to the receiver. We observe that the notion of ...
More Efficient Verifiable Functional Encryption
Provable and Practical Security
Abstract
Functional encryption (FE for short) can be used to calculate a function output of a message when given the corresponding function key, without revealing other information about the message. However, the original FE does not guarantee the ...

Reviews

Reviewer: Raghvinder S Sangwan

Functional purity is an important concept in functional programming languages. This paper explores functional purity in the context of Java. Imperative languages such as Java generally lack the notion of functional purity; to realize this concept, the authors use a restricted subset of Java-Joe-E-along with a static verifier. Having the ability to prove functional purity can provide an elegant way to reason about security properties, such as reproducibility, invertibility, noninterference, and containment of untrusted code, in parts of a system where this quality is highly desirable. Finifter et al. provide a nice background on the concept of functional purity and security properties of pure functions. In order to be pure, the functions must satisfy two critical properties: they cannot have side effects-their execution cannot have any visible effect other than generating a result-and they must be deterministic-their "behavior must depend only on the arguments provided" to them. Verifying functional purity is generally difficult. The authors introduce the concept of deterministic object-capability languages, in which a programmer can look at a function's type signature to tell whether it is pure. The only restriction in these languages is that the parameter types of a pure function must be immutable. Joe-E, a subset of Java, is a deterministic object-capability language. Using Joe-E, Finifter et al. demonstrate the benefits of modular reasoning about purity, such as refactoring blocks of legacy code to attain useful security and reliability guarantees. Functionally pure parts of a system are reproducible-since the determinism of pure functions "makes explicit the inputs a computation may depend" on, it allows replicated parts of a "system to transparently fail over to a backup that is receiving the same stream of input events." Functionally pure parts are invertible-for matched pairs of algorithms where one is an inverse of the other, determinism ensures that this inverse relationship holds at all times. Purity provides "a way to execute untrusted code safely"-simply verify the purity of the untrusted code and only execute it if it's pure. Functional purity has several additional benefits. The self-contained nature of pure functions makes them easy to understand, thread-safe, capable of asynchronous execution, and easy to replace at runtime. This capability is, therefore, a good addition to an imperative programming language. The elegance of the paper resides in providing a formalism for verifying critical security properties of a codebase that is based on two simple properties-the functions in this codebase should be deterministic and free of side effects. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CCS '08: Proceedings of the 15th ACM conference on Computer and communications security

October 2008

590 pages

ISBN:9781595938107

DOI:10.1145/1455770

General Chair:
Peng Ning
North Carolina State University, USA
,
Program Chairs:
Paul Syverson
Naval Research Laboratory, USA
,
Somesh Jha
University of Wisconsin, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 October 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS08

Sponsor:

CCS08: 15th ACM Conference on Computer and Communications Security 2008

October 27 - 31, 2008

Virginia, Alexandria, USA

Acceptance Rates

CCS '08 Paper Acceptance Rate 51 of 280 submissions, 18%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

33
Total Citations
View Citations
707
Total Downloads

Downloads (Last 12 months)19
Downloads (Last 6 weeks)1

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zuilhof Bvan Hees RGrelck C(2023)Code Quality Metrics for Functional Features in Modern Object-Oriented LanguagesComposability, Comprehensibility and Correctness of Working Software10.1007/978-3-031-42833-3_10(358-374)Online publication date: 18-Oct-2023
https://doi.org/10.1007/978-3-031-42833-3_10
Koppmann MKudera CPucher MMerzdovnik G(2022)Utilizing Object Capabilities to Improve Web Application SecurityApplied Cybersecurity & Internet Governance10.5604/01.3001.0016.08231:1(1-18)Online publication date: 16-Nov-2022
https://doi.org/10.5604/01.3001.0016.0823
Webster NServetto MHomer M(2022)Using Functional Reactive Programming to Define Safe Actor SystemsProceedings of the 24th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3611096.3611098(4-10)Online publication date: 7-Jun-2022
https://dl.acm.org/doi/10.1145/3611096.3611098
Banerjee SClapp LSridharan MDumas MPfahl DApel SRusso A(2019)NullAway: practical type-based null safety for JavaProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338919(740-750)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338919
Helm DKübler FEichberg MReif MMezini MHuchard MKästner CFraser G(2018)A unified lattice model and framework for purity analysesProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238226(340-350)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3238147.3238226
Eichberg MKübler FHelm DReif MSalvaneschi GMezini MDolby JHalfond WMishra A(2018)Lattice based modularization of static analysesCompanion Proceedings for the ISSTA/ECOOP 2018 Workshops10.1145/3236454.3236509(113-118)Online publication date: 16-Jul-2018
https://dl.acm.org/doi/10.1145/3236454.3236509
Allamanis MBarr EDevanbu PSutton C(2018)A Survey of Machine Learning for Big Code and NaturalnessACM Computing Surveys10.1145/321269551:4(1-37)Online publication date: 31-Jul-2018
https://dl.acm.org/doi/10.1145/3212695
Gorshkova ENovikov BShukla M(2017)A Fine-Grained Access Control Model and ImplementationProceedings of the 18th International Conference on Computer Systems and Technologies10.1145/3134302.3134310(187-194)Online publication date: 23-Jun-2017
https://dl.acm.org/doi/10.1145/3134302.3134310
Chrząszcz JSchubert AVanhoof WPientka B(2017)Function definitions for compound values in object-oriented languagesProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming10.1145/3131851.3131860(61-72)Online publication date: 9-Oct-2017
https://dl.acm.org/doi/10.1145/3131851.3131860
Holland BSanthanam GKothari S(2017)Transferring State-of-the-Art Immutability Analyses: Experimentation Toolbox and Accuracy Benchmark2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2017.55(484-491)Online publication date: Mar-2017
https://doi.org/10.1109/ICST.2017.55
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Verifiable Functional Encryption

Publicly verifiable ciphertexts

More Efficient Verifiable Functional Encryption

Reviews

Access critical reviews of Computing literature here