Systematic Bit-Flip Fault Injection and Exploration using Java PathFinder

This is a Google Summber of Code (GSoC) project on extending the Java PathFinder project (JPF). The project is done by Pu (Luke) Yi, under the supervison of Profs. Cyrille Artho and Pavel Parízek. The project code is publicly available at this PR.

Project Overview

The project uses Java PathFinder to systematically inject and explore bit-flip faults in the user specified variables in Java programs. The project supports injecting bit flips to (1) static and instance fields, (2) method arguments, and (3) local variables, whose type can be all primitive data types. The number of bits to flip in a variable is also configurable. The users can use three different ways to specify the variables: (1) directly calling the getBitFlip API in the application code, (2) adding @BitFlip annotation to the variables, and (3) specifying in the command line arguments without changing the application code.

Detailed Information

Implementation

  1. getBitFlip API (code). The users can invoke getBitFlip(v, k) in the program to get the value of v with k bits flipped, and the JPF will explore all $\binom{n}{k}$ possible flipping positions, where $n$ is the length of variable v.

    To provide such an API for all primitive data types, we first implement for long type, and for the other types, we first cast them to long, perform the bit flip, and then cast them back. The key challenge is to register only one choice generator even when k>0, because it confuses the JPF to register several choice generators at the same application code point. We resolve this issue by registering only one IntIntervalGenerator that produces an integer in range $[0,\binom{n}{k})$, and then decode the integer using binomial coefficients to get a set of $k$ bits to flip (code).

  2. @BitFlip Annotation (annotation class). The users can add @BitFlip(k) annotations to fields, parameters, or local variables in the code, where k is the number of bits to flip for the variable and by default 1. For the annotated parameters, the JPF will inject the bit flip when the method is invoked. For the annotated fields and local variables, the JPF will inject the bit flip when they are written.

    The implementation is based on the JPF listener and modifying the operand stack. We implemented the BitFlipListener which before a store instruction is executed, checks the annotations of the target fields (code) and local variables (code), and before an invocation instruction is executed, checks the parameter annotations (code). If the @BitFlip annotation is identified, the BitFlipListener registers a Choice Generator to the current system state in a similar way we do for getBitFlip API, and re-execute the instruction to start the exploration. To inject bit flips to the variables, we inject bit flips to the values in the operand stack that are to be assigned to them.

  3. Command Line argument support. If the users do not want to change the source code, they can use command line arguments (or alternatively the configuration file) to specify the variables to inject bit flips.

    The constructor method of the BitFlipListener reads the command line arguments and adds the specified variables to a watch list (code). Then before a store or invocation instruction is executed, the BitFlipListener checks the watch list besides the annotations. As a common practice, if the @BitFlip annotation and the command line specification are both present for a variable, we let the command line arguments surpress the annotations.

Testing and Examples

  1. JPF tests. We write a JPF test class BitFlipTest, which contains 16 regression tests that checks the bit flip injection mechanism and also documents the basic usage.
  2. We also created a repository to show the usage of our tool for Cyclic redundancy check (CRC) and International Standard Book Number (ISBN) algorithms. You can use our tool to see how resilient these algorithms are against bit flip fault.

Future Plan

It would be worthwhile to try out Symbolic PathFinder (SPF) to see how symbolic execution can help speed up the exploration of all possible bit flips.