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.