Team for Research in
Ubiquitous Secure Technology

Citation
Matthew Finifter, Adrian Mettler, Naveen Sastry, David Wagner. "Verifiable Functional Purity in Java". Talk or presentation, 12, November, 2008.

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.

Electronic downloads

• 23%20-%20Wagner.pdf · application/pdf · 546 kbytes

• HTML

  Matthew Finifter, Adrian Mettler, Naveen Sastry, David
  Wagner. <a
  href="http://www.truststc.org/pubs/494.html"
  ><i>Verifiable Functional Purity in
  Java</i></a>, Talk or presentation,  12,
  November, 2008.

• Plain text

  Matthew Finifter, Adrian Mettler, Naveen Sastry, David
  Wagner. "Verifiable Functional Purity in Java".
  Talk or presentation,  12, November, 2008.

• BibTeX

  @presentation{FinifterMettlerSastryWagner08_VerifiableFunctionalPurityInJava,
      author = {Matthew Finifter and Adrian Mettler and Naveen
                Sastry and David Wagner},
      title = {Verifiable Functional Purity in Java},
      day = {12},
      month = {November},
      year = {2008},
      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. },
      URL = {http://www.truststc.org/pubs/494.html}
  }
  

Posted by Jessica Gamble on 23 Jan 2009.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.