GSoC/GCI Archive
GSoC/GCI Archive
Google Summer of Code 2012

The Java Pathfinder Team

Web Page: http://babelfish.arc.nasa.gov/trac/jpf/wiki/events/soc2012

Mailing List: http://groups.google.com/group/java-pathfinder

The Java PathFinder project (JPF) was initially conceived and developed at NASA Ames Research Center in 1999. JPF was open sourced in April 2005 as one of the first ongoing NASA development projects ever. JPF is a highly extensible Java Virtual Machine (JVM) written in Java itself, and is used to create a variety of verification tools ranging from concurrency software model checkers to test case generators using symbolic execution. JPF is a research platform and a production tool at the same time. Although JPF has serious contributions from companies and government agencies, our main user community is academic - there are ongoing collaborations with more than 20 universities world-wide. The JPF team for GSoC 2012 is led by the NASA Ames Research Center, but includes mentors from NCSU, University of Texas, Brigham Young University and the universities of Stellenbosch SA, Tokyo JP, and Prague CZ.

JPF is designed to be extensible. There are well defined extension mechanisms, directory structures and build procedures, which keep the core relatively stable and provide suitable, well separated testbeds for new ideas and alternative implementations. As a consequence we host a number of such extension projects on our own, public JPF server, together with a Wiki that is the one-stop for learning about, obtaining and contributing to JPF.

JPF has been used for a variety of application domains and research topics such as verification of multi-threaded applications, graphical user interfaces, networking, and distributed applications. In addition to its continued presence in academia, JPF has matured enough to support verification of production code and frameworks such as Android. JPF is constantly being extended with support for verification of new types of properties for new types of application domains.

Projects

  • Abstract Model Checking Abstract Pathfinder is an extension for Java PathFinder, which aims to introduce data abstraction. Abstract Pathfinder supports various abstractions for numeric data like Signs, Evenness, Interval and Range, which can be arbitrarily combined together.
  • Conformance Checker The Java Path Finder uses a set of so called model classes in alternative to the standard library classes. These classes are expected to show the same behaviour of their standard library counterpart, where the 'behaviour' is represented by the public and protected members a class has. To prevent bugs, it is important that this behaviour is exactly the same of the standard library counterpart and an automated tool is needed to ensure this conformance.
  • Dimensional Analysis of Physical Units The project is aiming to create a lightweight, easy-to-use extension of the Java PathFinder project that would carry out a dimensional analysis of units used in scientific computation. One of the objectives is for the solution to be applicable on legacy code, so the changes done to the code need to be as minimal as possible. The analysis would be performed during the testing phase, keeping only the floating-point arithmetic in the final binary executable.
  • Human Automation Interaction Patterns The main objective of the project is to extend the jpf-hmi project in order to support human automation interaction patterns and verification of their properties by the Java Path Finder model checker.
  • jpf-android: analysing Android applications. This project will extend Java Pathfinder to allow the verification of Android applications.
  • jpf-qif : Quantitative Information Flow Analysis for Java Bytecode Computer systems in the real world are never 100% secure, so we need to measure how secure they are. As a simple example, suppose an attacker tries to guess a password: if his guess is correct, he can obtain all the information; otherwise he can still learn that the password is not the same as the previous try, so his search space is narrowed. In either the cases, the password checking program does leak some information. The aim of this project is to use Java PathFinder to quantify leakage of confidential information in Java programs.
  • Model Checking Android Applications This project would involve extending the Java Path Finder (JPF) software model checker to handle Android service applications. More at: https://gitorious.org/jpf-android-services
  • Sanitizer validation using symbolic execution and library cross-checking The goal of this project is to analyze sanitization libraries in seek of vulnerabilities. More specifically, we want to find inputs that reveal vulnerabilities in existing sanitization functions. Our contribution is twofold: (1) we want to find spec-violating inputs for the sanitization function and (2) report vulnerabilities not covered by the current library.
  • Security policy verification via information flow analysis Data (information) flow plays an important part in software security. Many security properties rely on the possibility to follow data flow throughout the program. The most popular security policy for information flow is non-interference, which consists in assigning secrecy levels to the data and forbids flows from high secrecy level data to the low secrecy level data.
  • Semantic Porting Analysis based on JPF Regression DiSE and DSE To introduce similar features or bug fixes developers often port code from one program context to another. Ad hoc porting can produce various side effects if the source and target contexts differ. As ported edits are similar to reference edits, a syntactic program differencing tool cannot identify such semantic discrepancies. In this project we propose to develop a semantic porting analysis tool using the JPF framework. Given a pair of source and target edits as input our tool will generate test cases to manifest differences in the input-output behavior of the source and target contexts.
  • Trace Server Trace Server is used for storing, querying, analyzing and printing collected trace information. Postmortem analyzers can be used to find out about defects.This year's work will be a continuation of GSoC 2010, by implementing new functionality, as well as improving current performance. The plan is to develop new storage, DSL for querying the database, new analyzers, new user interface, use Scala to increase performance and reduce complexity of code.