The Information Flow Calculus is unsound II

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

• Mantis: MT-1560

• Submitted on: 2015-08-04 by (at)mulbrich

• Updated: 2015-09-25

• Assigned to: (at)mkirsten

Description

Advanced control structures are not supported by the information flow engine for loops.

In addition to exceptions reported in #1535, return statements allow one to leak information undetected by the calculus.

break-statements have a similar potential. Due to some other bug with handling loop invariants (which actually should be another bug report ...), the proof could not be conducted however.

! THESE SOUNDNESS ISSUES ARE SEVERE. ! The information flow engine in KeY MUST be reconsidered in these respects. ! It is not in a state that would allow us to promote it publicly.

Steps to reproduce

Load the attached example Strange3
Strange5 contains the "break"-example

Additional Information

investigated together with Michael.

Due to bug #1559, we had to try this on KeY 2.4. But concepts have 
not been changed since.

Files

Strange3.java:

class Strange3 {

    /*@ requires true;
      @ determines \result \by l;
      (at)*/
    boolean m(boolean h, boolean l) {

        /*@ loop_invariant true;
          @ decreases 0;
          @ determines l \by \itself;
          (at)*/
        while(l) {
            return h;
        }

        return false;
    }

   // hidden for KeY
//   public static void main(String[] arg) {
//      Strange3 s = new Strange3();
//      
//      System.out.println("Running with h=true:");
//      try { System.out.println(s.m(true, true)); }
//      catch(Exception e) { e.printStackTrace(); }
//
//      System.out.println("Running with h=false:");
//      try { System.out.println(s.m(false, true)); }
//      catch(Exception e) { e.printStackTrace(); }
//  }


}

Strange5.java:

class Strange5 {

    /*@ requires true;
      @ determines \result \by \nothing;
      (at)*/
    int m(boolean h) {

        boolean l1 = true;
        boolean l2 = true;
        int l = 0;

        /*@ loop_invariant true;
          @ decreases l1 ? 1 : 0;
          @ determines l, l2, l1 \by \itself;
          (at)*/
        label1: while(l1) {
             /*@ loop_invariant true;
               @ decreases l2 ? 1 : 0;
               @ determines l2, l1, l \by \itself;
               (at)*/
            label2: while(l2) {
                if(h) break label1;
                l2 = false;
            }
            l = 1;
            l2 = false;
        }

        return l;
    }

   // hidden for KeY
//   public static void main(String[] arg) {
//      Strange3 s = new Strange3();
//      
//      System.out.println("Running with h=true:");
//      try { System.out.println(s.m(true, true)); }
//      catch(Exception e) { e.printStackTrace(); }
//
//      System.out.println("Running with h=false:");
//      try { System.out.println(s.m(false, true)); }
//      catch(Exception e) { e.printStackTrace(); }
//  }


}

Notes

(at)grahl at 2015-08-05

It seems that the quickest solution to achieve soundness would be to disable the invariant rule.

Associated Bugs

• Relates to MT-1535 with

History

• (at)mulbrich -- (NEW_BUG) 2015-08-04

• (at)mulbrich -- (FILE_ADDED) 2015-08-04

• (at)mulbrich -- (FILE_ADDED) 2015-08-04

• (at)mulbrich -- (BUG_ADD_RELATIONSHIP) 2015-08-04

• (at)grahl -- (BUGNOTE_ADDED) 2015-08-05

• (at)grahl -- (NORMAL_TYPE) 2015-08-18

• (at)grahl -- (NORMAL_TYPE) 2015-09-25

• (at)grahl -- (NORMAL_TYPE) 2015-09-25

• (at)grahl -- (BUG_ADD_RELATIONSHIP) 2015-10-01

Attributes

• Category: Calculus (Soundness)
• Status: ASSIGNED
• Severity: MAJOR
• OS:
• Target Version: 2.6
• Resolution: OPEN
• Priority: HIGH
• Reproducibility: ALWAYS
• Platform:
• Commit: f29c982fc6c75827991e94a2a905e3419d01d6ee
• Build:
• Tags []
• Labels: ~Bug ~HIGH

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:33:07.951Z
• updated_at: 2019-04-12T14:21:33.747Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0