Systematically explore bit-flip faults in user-specified variables in Java programs.

[y553546436]

Systematically explore bit-flip faults in user-specified variables in Java programs.

Computer hardware is susceptible to errors. For example, radiation may induce error to the hardware and some bit might be flipped. It is important to improve the resiliency of software against hardware errors. One way to evaluate the resiliency of software against hardware errors is by fault injection. This JPF extension aims to systematically inject and explore bit-flip faults in the user specified variables in Java programs.
This website summarizes the contributions of this extension.

What it does

This extension can systematically inject and explore bit-flip faults in the user specified variables in Java programs. The variable to flip can be method parameters, fields, and local variables, and it can be any of the 8 primitive data types. You can specify the variable(s) to flip in three different ways: (1) directly calling the Verify.getBitFlip API in the code, (2) adding @BitFlip annotation to the variables, and (3) specifying in the command line arguments without changing the application code.

How to use it

Suppose you have this simple program that does nothing but prints 0 by invoking a method called foo:

package simple.example;

public class SimpleExample {
     public static void foo(int bar) {
         System.out.println(bar);
     }
     public static void main(String[] args) {
         foo(0);
     }
}

Now you want to see what will happen if there is some error in the argument passing that causes a bit flip in argument bar. Since bar is of type int, there are 32 cases of which bit is flipped, and you want to see how the program reacts to all of them. You can three options of doing that:

1. Call the Verify.getBitFlip API. This approach is straightforward and easy to control. You just need to add one line at the beginning of the method foo (of course you should first import gov.nasa.jpf.vm.Verify):

   bar = Verify.getBitFlip(bar, 1)

   The second parameter of getBitFlip method specifies the number of bits to flip in the variable, which is usually 1, but we support up to 7 bits to flip. The first argument can be again, any of the 8 primitive types. Now run this program in JPF, expectedly you will get the following output:

   1
   2
   4
   ...
   1073741824
   -2147483648
   

   The output shows that the JPF explores all the 32 cases of one bit flip in bar.

2. Add @BitFlip annotation to the variable. This is even simpler than calling the getBitFlip API. You just need to annotate bar like this:

   public static void foo(@BitFlip int bar)

   and then run the program in JPF with this command line argument +listener=gov.nasa.jpf.listener.BitFlipListener. You will get the same output as we get for the API option.

   To explain a bit, this extension injects bit flips to annotated parameters when the argument values are passed, and to annotated fields and local variables when they are written. To support that, we need a JPF listener that checks the annotations of the target variables of each instruction, and that is what the command line argument above is for.

   You can also configure the number of bits to flip in the variable by annotate it with @BitFlip(k) where k is the number, and by default 1.

3. Specify the variable in the command line argument to the JPF. If you don't want any change to your source code, then this is the best option. You can directly run the program in JPF with the following arguments passed to the JPF:

   +listener=gov.nasa.jpf.listener.BitFlipListener +bitflip.params=foobar +bitflip.foobar.method=simple.example.SimpleExample.foo(int) +bitflip.foobar.name=bar

   The BitFlipListener will read the command line arguments and add the specified variables to the watch list, and before a store instruction or invocation instruction, it will check the watch list for variables to flip. The name foobar is a configuration name for a parameter bit flip, and the following two arguments specify the method and parameter name of foobar. Note that you can also configure the number of bits to flip by passing another argument +bitflip.foobar.nbit=k, and if not specified, k is by defaut one.

More Examples

For more detail, the regression test class gov.nasa.jpf.test.mc.data.BitFlipTest documents most of the use senarios in 16 regression tests, from simple usage as shown above, to more complex usage like combining the annotations and the command line arguments.

We also have a GitHub repository to show how this extension could be used to evaluate error detection algorithms' resiliency against bit flip faults. Specifically, it contains the implementation of the Cyclic redundancy check (CRC) and International Standard Book Number (ISBN) algorithms where you can try out this extension.

[cyrille-artho]

Thank you very much! Merged. The CI issue is documented in issue #294 and does not seem to be related to your code.