-
Notifications
You must be signed in to change notification settings - Fork 343
GSoC 2020 Project Ideas
Please note that this list is not exclusive. If you have other ideas and topics related to JPF, please let us know on the JPF Google group. A possible proposal template can be found at the bottom of our GSoC page: JPF Google Summer of Code 2020.
Description:
jpf-core is essentially a JVM that currently fully supports only Java 8. The goal of this project is to make it up-to-date with new features of Java 11. The JPF source itself has already been made compatible with Java 11. Now, JPF should support new features of Java 11 bytecode. The key feature of Java 11 that is currently not supported are bootstrap methods that are generated at load time. They are used for things as common as string concatenation ("Hello, " + name). As of now, a few specialized cases are supported, but there are still many programs (and unit tests) that fail with Java 11. It is therefore very important for us that we support the general case of this feature. The current state can be seen by running the unit tests of branch java-10-gradle with Java 11.
This is a high-priority project, as support for Java 8 is limited to the near future. Note: You can apply to both projects (Java 11 or 12 support); in that case, please indicate that you would like to work on either one, and what your preference would be.
Difficulty: Hard
Required skills: Knowledge of Java bytecode
Preferred skills: Knowledge of bootstrap methods in Java bytecode
Related to the project above, there are also some internal APIs from Java 11 that no longer exist in Java 12 and later.
This requires redesigning and reimplementing part of the code, in order to take a different approach that no longer depends on functionality that was removed in Java 12. The code in question is easily found by trying to compile branch java-10-gradle with Java 12.
Note: You can apply to both projects (Java 11 or 12 support); in that case, please indicate that you would like to work on either one, and what your preference would be.
Difficulty: Medium
Required skills: Knowledge of Java internals
Description: Symbolic PathFinder is essentially a (symbolic) JVM that currently supports only Java 8. The goal of this project is to make it up-to-date with new features of Java 11. This is a high-priority project, as support for Java 8 is limited to the near future.
Description: The goal of this project is to (1) implement gradle support for Symbolic Pathfinder, (2) to update the extension template, including gradle support and updated documentation.
Description: Symbolic PathFinder incorporates String constraint solvers (ABC,Z3) to enable analysis of programs that process Strings. The project will involve careful testing and improving the infrastructure for String solving.
Description: A thesis project implemented Summaries of methods when executing in JPF. It includes a representation of the summaries that captures all side effects of the given procedure; and implements modifications of the program state.
The actual summary of a method will be computed during its first execution, and then reused within traversal of other state paths. Another possible feature is the support for externally defined summaries that would be useful for library methods.
Experiments have shown that without summarizing the effects of constructors, most methods cannot be summarized. This is caused by the construction of new objects or throwing an exception (which also create a new object). Summarizing the effect of constructors would therefore be a huge enhancement to this technique. Other enhancements may also be possible.
Difficulty: Medium
Required skills: Knowledge of Java bytecode
Preferred skills: Handling of weak references, garbage collection
Description: jpf-nas is an extension of JPF that provides support for model checking distributed multithreaded Java applications. It relies on the multiprocess support included in the jpf-core which provides basic functionality to verify the bytecode of distributed applications. jpf-nas supports interprocess communication via TCP sockets by modeling the Java networking package java.net. This tool can handle simple multi-client server applications. Some examples can be found in the jpf-nas distribution (at jpf-nas/src/examples/). The goal of this project is to extend the functionality of jpf-nas in various ways, such as extending the communication model supported by the tool towards an existing open source Java library/framework, called QuickServer, increasing the performance of the tool by improving the mechanism used to manage the state of communication objects, extending the tool with the cache-based approach used in net-iocache, etc.
Difficulty: Medium
Required skills: Knowledge of Java networking
Preferred skills: Knowledge of jpf-nas or net-iocache
Description: Automated program repair (APR) techniques often generate overfitting patches due to the reliance on test cases for patch generation and validation. In this project, we propose to overcome the overffiting issue in APR by leveraging developer-provided partial annotations to aid semantic reasoning. Developer annotations can come in different forms, e.g., JPF annotation. The advantage of developer annotations is two-fold. First, in addition to test cases, it helps augment the specifications of the program under analysis and thus provides more complete specifications. These annotations, despite being simple, can help significantly in semantic reasoning, e.g., null pointer analysis. Second, these annotations are not required to be complex so that to reduce the burden of manual effort by developers. For example, to reason about null pointer exception errors, developers are only required to add a few Nullable or Non-Nullable annotations to class fields or method parameters, etc. We will use JPF and SPF for symbolically reasoning about the semantics of programs under analysis and generating repairs. We will also use JPF-Annotation as a way for developers to provide annotations.
Description: SPF constraints need to be refactored to allow different kinds of constraints to be combined during the construction of a path condition. An example of how it should be after the refactoring is the Abstract Syntax Tree constructed by GREEN.
Difficulty: Medium
Required skills: Knowledge of object-oriented programming in Java, general knowledge of SMT-solvers
Preferred skills: Priori software development experience using SMT-solvers' APIs
Expected outcomes: More efficient and flexible constraint interface used to express a path constraints
Description: Hash-consing is a technique that reuses previously constructed expressions to avoid duplication during construction of larger expressions. It is a technique that has been extensively used for creating maximally-shared graphs (see Calysto by Babic et al.), reusing structurally equivalent expressions in KLEE (by Cadar et al.). Variants of this idea are also applied in other binary symbolic executors like FuzzBALL and built in to new binary analysis frameworks (see Jung et al). Symbolic PathFinder currently does not support hash-consing or sharing of subexpressions causing memory usage to blow-up in pathological examples. This project would be about implementing hash-consing or a variant of this idea in SPF. This would have a clear benefit in reducing SPF's memory usage.
Difficulty: Medium
Required skills: Knowledge of symbolic execution and what it is useful for
Preferred skills: Prior experience of developing or maintaining a symbolic execution tool
Expected outcomes: Clear reduction in memory usage of SPF when we run benchmarks. The idea of hash-consing is being adapted from the veritesting paper by Avgerinos et al.
Description: A symbolic executor explores feasible choices through a program. It can often be difficult to understand how a symbolic executor got to a particular program location in a given symbolic state. These difficulties arise from not being able to easily see all the previous choices the symbolic executor made to get to a certain point. To address this limitation, a symbolic executor can be asked to visually report its tree of exploration choices. An example of this is FuzzBALL's "-decision-tree-use-file" that reports FuzzBALL's tree of explored choices into a file that can be visualized. This project would be add a similar feature in SPF. Given a point of symbolic exploration, it would allow SPF to report its tree of explored ChoiceGenerator objects into a file that can be observed visually.
Difficulty: Easy
Required skills: Java programming
Preferred skills: Some knowledge of symbolic execution
Expected outcomes: Visualization of the choice generator tree when exploring a few benchmarks; implementation of a few ideas to improve the usability of such trees when generated from a symbolic execution run with complex software
Description: SPF has a large number of diverse configuration options. Enabling some features require combinations of options (such as incremental solving) whereas other options are backed by a broken implementation. For example, during the recently concluded SV-COMP 2020 competition, the Java Ranger authors (which also includes me) turned off symbolic string support, while the SPF team chose to leave this option on. For this project, we would examine all of SPF's options and construct test cases to combinatorially cover all of them. The outcome of this project would be a regression test suite that combinatorially covers all of SPF's options and provides clear documentation on which options don't work. If there is still time available during the summer, we would also attempt to fix SPF's broken symbolic string solving. There have been many recent advances in string solving and it would be valuable to have support for powerful string solvers such as z3str3. This project can also be combined with the improving string analysis project above.
Difficulty: Medium
Required skills: Java programming
Preferred skills: Some knowledge of SPF's configuration options
Expected outcomes: A clear list of SPF options that dont play well with each other; a list of test cases that tested the correct interactions between SPF options
Description: Path-merging has recently been implemented as an extension to the Symbolic PathFinder tool. However, path-merging is not always beneficial because it can contribute to making the contents of the stack and/or the heap symbolic. Later branching on these symbolic contents can cause further branching. This project is about developing a heuristic similar to the one proposed by Kuznetsov et al. for symbolic execution of Java bytecode.
Difficulty: Hard
Required skills: Knowledge of path-merging in symbolic execution; examples include dynamic state merging and/or veritesting
Preferred skills: Knowledge of SPF's internals when it comes to its execution of conditional branches; knowledge of Java Ranger would be further beneficial
Expected outcomes: a heuristic that improves SPF's performance when it uses path-merging but avoids path-merging when it doesn't seem beneficial; the targeted heuristic is of the kind proposed in the state merging paper above by Kuznetsov et al.
Description: Path-merging has recently been implemented as an extension to the Symbolic PathFinder tool. However, test generation with a path-merging symbolic executor is different because we would not want test generation to undo all the benefits of path-merging. Test generation should instead be targeted towards achieving coverage of some coverage criterion specified by the user. In this project, we will attempt to do test generation with a path-merging symbolic executor which will be Java Ranger. One example of test generation can be found in the test generation performed with veritesting by Avgerinos et al.
Difficulty: Hard
Required skills: Knowledge of path-merging in symbolic execution; examples include dynamic state merging and/or veritesting. This project would also involve knowledge of test criteria like MC/DC.
Preferred skills: Knowledge of SPF's internals when it comes to its execution of conditional branches; knowledge of Java Ranger would be further beneficial
Expected outcomes: a implementation that generates tests with a path-merging symbolic executor like Java Ranger
Description: Develop a fuzzer for Java that can be integrated with SPF (or another Java based symbolic execution engine). The idea would be that when fuzzing gets stuck and makes no progress that the symbolic analysis can create a new seed file to allow analysis to progress.
Description: This project explores the application of symbolic execution and related methods to the domain of neural networks. The goal of the project is to design and implement a family of integrated analyses that allow testing and debugging of neural networks. The project will build on recent advances in symbolic analysis of neural networks and utilize the SPF/JPF toolset.
Description: Develop a mechanism to allow the analysis of Ethereum Virtual Machine (EVM) bytecode by replacing the JVM bytecodes with EVM bytecodes within JPF. The second part of the project would be to extend the bytecodes further to allow symbolic execution as well.
Description: JDart is a dynamic symbolic execution for Java programs and is based on Java PathFinder (JPF). The tool executes Java programs with concrete and symbolic values at the same time and records symbolic constraints describing all the decisions along a particular path of the execution. These path constraints are then used to find new paths in the program. Concrete data values for exercising these paths are generated using a constraint solver. Recent development on JDart has focused on supporting more language features of Java (e.g., symbolic analysis of String variables) and on implementing taint analysis on top of concolic execution. As a consequence, JDart scored the third place in the Java track of SV-Comp 2020 and was able to beat the OWASP security benchmark. Source code of recent development can be found at https://github.com/tudo-aqua/jdart.
To further robustness of JDart, the tools needs a small overhaul of its architecture: the build system has to be updated to maven or gradle, dependencies should be handled by the build system, and proper unit tests should be executed by the build system. (A subset of) SV-Comp and OWASP benchmarks should become regression tests. To increase scalability, JDart should be make use of parallelization. Concolic execution lends itself to parallelization as individual executions are completely independent of one another (cf. works of white-box fuzzing). The architecture of JDart should be modularized with clear APIs between components as a basis for making JDart parallel. Google summer of code project could focus on a subset on these goals depending on skill set and interests of students.
Difficulty: Medium
Required skills: Java, maven/gradle, unit testing
Preferred skills: APIs, docker, multi-threading, distributed applications
Expected outcomes: An overhauled version of JDart should be made available under the Java PathFinder organization on github as one result of the Google summer of code project. When tackling scalability, results could be submitted to the JPF workshop.
Description: JPF requires test cases as a starting point to explore a system. It is therefore suitable to use test case generation to create test cases automatically. Modbat is an open-source tool for test case generation. For testing concurrent software, an obvious choice would be to combine Modbat (to generate tests) with JPF (to execute tests and find concurrency problems). This has been done once as a proof of concept but is not supported in the current version of Modbat. The main reason for this is that Modbat's reporting has to read and parse bytecode, which requires access to some native code that JPF does not support. The goal is to find all problems where Modbat requires native access, and to use jpf-nhandler to resolve as many of these cases as possible. Remaining cases can be handled with custom model/peer classes.
Difficulty: Easy
Required skills: Knowledge of Java Pathfinder
Preferred skills: Knowledge of test generation
Description: Habanero Java is a Java implementation of the Habanero Extreme-scale programming model for multithreaded applications. The model is based on X10 and supports fork/join semantics as well as futures, isolation, and phasers. The advantage of structured parallelism such as Habanero is that the language itself provides concurrency guarantees such as deadlock freedom and determinacy if and only the program is free of data-race. A data-race occurs when two or more threads of execution access the same memory location and at least one of those accesses is a write. An additional advantage of structured parallelism is that run-times and analysis can be optimized based on the language structure itself. Recent work adds to JPF the ability to model check Habanero Java programs using a verification specific runtime and an algorithm that constructs and analyzes a computation graph representing the happens-before relation of the program execution (1, 2. The analysis is predictive because it infers from the single observed schedule the presence or absence of data-race in other non-observed schedules and only needs to enumerate schedules around isolation. Enumeration schedules around isolation though is still expensive and leads to state explosion in JPF. The work in this project is to mitigate this state explosion in enumerating schedules around isolation by building a symbolic computation graph from the program execution that adds constraints on the graph edges indicating under what condition the edge is active, and then using an SMT solver to find a set of edges on which a data-race exists. A first step in the project is to add a dynamic partial order reduction to JPF that is able to inform the symbolic computation graph about dependencies.
Difficulty: Medium
Required skills: Java programming and knowledge of model checking
Expected outcomes: SMT solution to data-race that avoids state exploration
Please contact us by creating an issue. We are trying to fix the process below, which no longer works.
-
How to obtain and install JPF
- System requirements
- Downloading
- Creating a site properties file
- Building, testing, and running
- JPF plugins
-
Developer guide
- Top-level design
- Key mechanisms
- Extension mechanisms
- Common utilities
- Running JPF from within your application
- Writing JPF tests
- Coding conventions
- Hosting an Eclipse plugin update site