Apply patches for #295 to explore bit-flip manipulation and #297 and #299 to fix and refactor the Verify class (#403)

Co-authored-by: varad64 <[email protected]>

Author: varad64

src/annotations/gov/nasa/jpf/annotation/BitFlip.java

@@ -0,0 +1,17 @@
+package gov.nasa.jpf.annotation;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * @author Pu Yi <[email protected]>
+ *
+ * An annotation used to specify fields/parameters to perform bit flipping exploration
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ ElementType.PARAMETER, ElementType.FIELD, ElementType.LOCAL_VARIABLE })
+public @interface BitFlip {
+  int value() default 1;
+}

src/main/fault/injection/examples/APISimpleExample.java

@@ -0,0 +1,12 @@
+package fault.injection.examples;
+
+import gov.nasa.jpf.vm.Verify;
+
+/*
+ * Use getBitFlip API to inject a bit flip to a variable
+ */
+public class APISimpleExample {
+    public static void main(String[] args) {
+        System.out.println(Verify.getBitFlip((byte)0, 2));
+    }
+}

src/main/fault/injection/examples/AnnotationSimpleExample.java

@@ -0,0 +1,16 @@
+package fault.injection.examples;
+
+import gov.nasa.jpf.vm.Verify;
+import gov.nasa.jpf.annotation.BitFlip;
+
+/*
+ * Use @BitFlip annotation to inject a bit flip to an argument
+ */
+public class AnnotationSimpleExample {
+    public static void foo(@BitFlip byte bar) {
+        System.out.println(bar);
+    }
+    public static void main(String[] args) {
+        foo((byte)0);
+    }
+}

src/main/fault/injection/examples/BCDEncodedISBN.java

@@ -0,0 +1,77 @@
+package fault.injection.examples;
+
+import gov.nasa.jpf.vm.Verify;
+
+/*
+ * International Standard Book Number (ISBN) error detection
+ * BCD variant
+ */
+public class BCDEncodedISBN {
+
+    // get the i-th (indexed from 0) decimal number
+    static int getNumber (long digits, int i) {
+        return (int) ((digits >> (i << 2)) & 15);
+    }
+
+    // calculate the check digit for ISBN-10 based on the first 9 digits
+    public static int calculate10 (long digits) {
+        int s = 0, t = 0;
+        for (int i = 0; i < 9; ++i) {
+            int digit = getNumber(digits, i);
+            t += digit;
+            s += t;
+        }
+        return (11 - (s + t) % 11) % 11;
+    }
+
+    // ISBN-10 check
+    public static boolean check10 (long digits) {
+        // invalid if more than 10 decimal numbers
+        if ((digits >> 40) != 0)
+            return false;
+        for (int i = 0; i < 10; ++i) {
+            if (getNumber(digits, i) > 10 || (getNumber(digits, i) == 10 && i != 9))
+                return false;
+        }
+        return getNumber(digits, 9) == calculate10(digits);
+    }
+
+    // calculate the check digit for ISBN-13 based on the first 12 digits
+    public static int calculate13 (long digits) {
+        int s = 0, t = 1;
+        for (int i = 0; i < 12; ++i) {
+            s += getNumber(digits, i) * t;
+            t = 4 - t;
+        }
+        return (10 - s % 10) % 10;
+    }
+
+    // ISBN-13 check
+    public static boolean check13 (long digits) {
+        // invalid if more than 13 decimal numbers
+        if ((digits >> 52) != 0)
+            return false;
+        for (int i = 0; i < 13; ++i) {
+            if (getNumber(digits, i) < 0 || getNumber(digits, i) > 9)
+                return false;
+        }
+        return getNumber(digits, 12) == calculate13(digits);
+    }
+
+    // given the first 9 digits, generate the 10th, and check that one bit flip will always be detected
+    public static void main (String[] args) {
+        assert (args[0].length() == 9);
+        long digits = 0;
+        for (int i = 0; i < 9; ++i) {
+            char c = args[0].charAt(i);
+            assert (c >= '0' && c <= '9');
+            digits |= ((long) (c - '0')) << (i << 2);
+        }
+        digits |= ((long) calculate10(digits)) << (9 << 2);
+        assert (check10(digits));
+        digits = Verify.getBitFlip(digits, 2, 40);
+        if (check10(digits)) {
+            System.out.println("Masked case: " + digits);
+        }
+    }
+}

src/main/fault/injection/examples/CRC.java

@@ -0,0 +1,53 @@
+package fault.injection.examples;
+
+/*
+ * Cyclic redundancy check algorithm
+ * Assume the CRC algorithm is performed in GF(2)
+ */
+public class CRC {
+
+    int n; // divisor's length
+    int[] d; // the divisor
+
+    CRC (String divisor) {
+        n = divisor.length();
+        d = new int[n];
+        for (int i = 0; i < n; ++i) {
+            assert (divisor.charAt(i) == '0' || divisor.charAt(i) == '1');
+            d[i] = divisor.charAt(n-1-i) - '0';
+        }
+    }
+
+    // calculate the remainder of the given bit string
+    public String remainder (String s) {
+        // convert string to int array
+        String padded = new String(s);
+        for (int i = 0; i < n-1; ++i)
+            padded += "0";
+        int len = padded.length();
+        int[] r = new int[len];
+        for (int i = 0; i < len; ++i)
+            r[i] = padded.charAt(len-1-i) - '0';
+        for (int i = len-1; i >= n-1; --i) {
+            if (r[i] == 1) {
+                for (int j = 0; j < n; ++j)
+                    r[i-j] ^= d[n-1-j];
+            }
+        }
+        String res = "";
+        for (int i = n-2; i >= 0; --i)
+            res += r[i];
+        return res;
+    }
+
+    // check the data integrity
+    public boolean check (String s, String r) {
+        if (s == null)
+            return false;
+        for (char c : s.toCharArray()) {
+            if (c != '0' && c != '1')
+                return false;
+        }
+        return remainder(s).equals(r);
+    }
+}

src/main/fault/injection/examples/CheckISBN.java

@@ -0,0 +1,46 @@
+package fault.injection.examples;
+
+/*
+ * International Standard Book Number (ISBN) error detection
+ */
+public class CheckISBN {
+    // calculate the check digit for ISBN-10 based on the first 9 digits
+    public static int calculate10 (int[] digits) {
+        int s = 0, t = 0;
+        for (int i = 0; i < 9; ++i) {
+            t += digits[i];
+            s += t;
+        }
+        return (11 - (s + t) % 11) % 11;
+    }
+    // ISBN-10 check
+    public static boolean check10 (int[] digits) {
+        if (digits == null || digits.length != 10)
+            return false;
+        for (int i = 0; i < 10; ++i) {
+            if (digits[i] < 0 || digits[i] > 10 || (digits[i] == 10 && i != 9))
+                return false;
+        }
+        return digits[9] == calculate10(digits);
+    }
+
+    // calculate the check digit for ISBN-13 based on the first 12 digits
+    public static int calculate13 (int[] digits) {
+        int s = 0, t = 1;
+        for (int i = 0; i < 12; ++i) {
+            s += digits[i] * t;
+            t = 4 - t;
+        }
+        return (10 - s % 10) % 10;
+    }
+    // ISBN-13 check
+    public static boolean check13 (int[] digits) {
+        if (digits == null || digits.length != 13)
+            return false;
+        for (int i = 0; i < 13; ++i) {
+            if (digits[i] < 0 || digits[i] > 9)
+                return false;
+        }
+        return digits[12] == calculate13(digits);
+    }
+}

src/main/fault/injection/examples/LongEncodedCRC.java

@@ -0,0 +1,63 @@
+package fault.injection.examples;
+
+import gov.nasa.jpf.vm.Verify;
+
+/*
+ * Cyclic redundancy check algorithm
+ * Assume the CRC algorithm is performed in GF(2)
+ * Assume the data length is less than 64 bits, and encode them in a variable of type long
+ */
+public class LongEncodedCRC {
+
+    int n; // divisor's length
+    long d; // the divisor
+
+    LongEncodedCRC (String divisor) {
+        n = divisor.length();
+        d = 0;
+        for (int i = 0; i < n; ++i) {
+            assert (divisor.charAt(i) == '0' || divisor.charAt(i) == '1');
+            d |= ((long) (divisor.charAt(n-1-i) - '0')) << i;
+        }
+    }
+
+    LongEncodedCRC (long _d) {
+        d = _d;
+        assert (d != 0);
+        for (int i = 0; i < 64; ++i)
+            if ((d >> i & 1) == 1) {
+                n = i;
+            }
+    }
+
+    // calculate the remainder of the given bit string
+    public long remainder (int len, long s) {
+        long r = s << (n-1);
+        len += n-1;
+        for (int i = len-1; i >= n-1; --i) {
+            if ((r >> i & 1) == 1) {
+                r ^= d << (i-n+1);
+            }
+        }
+        return r;
+    }
+
+    // check the data integrity
+    public boolean check (int len, long dataWithCheckBits) {
+        long data = dataWithCheckBits >> (n-1);
+        long checkBits = dataWithCheckBits & ((1 << (n-1)) - 1);
+        return remainder(len, data) == checkBits;
+    }
+
+    // check that bit flips in the data can be detected
+    public static void main (String[] args) {
+        LongEncodedCRC crc = new LongEncodedCRC("1011");
+        int len = 14;
+        long dataWithCheckBits = 0b11010011101100100l;
+        assert (crc.check(len, dataWithCheckBits));
+        long flippedData = Verify.getBitFlip(dataWithCheckBits, 2, 17);
+        if (crc.check(len, flippedData)) {
+            System.out.println("Masked case: " + flippedData);
+        }
+    }
+}