Compiler Optimisations: Security-Preserving Refinement (NuSMV)

Description of the Case Study

We study three compiler optimisation patterns and analyse whether they preserve the security guarantees of the original program. Each optimisation transforms a loop-based routine into a more efficient variant: Loop Peeling (LP) moves one iteration outside the loop, Expression Folding Loop Peeling (EFLP) normalises arithmetic expressions, and Dead Branch Elimination (DBE) removes infeasible public branches. For every pair, the source model captures the original program and the target model implements the optimised version. The HyperLTL specification requires that public outputs remain indistinguishable across both programs, ensuring that the transformation does not introduce information leaks.

The NuSMV model(s)

LP Original — SourceLP Original — TargetLP Nondet — SourceLP Nondet — TargetLP Nondet — Incorrect TargetLP Loop — SourceLP Loop — TargetLP Loop — Incorrect TargetEFLP — SourceEFLP — TargetEFLP Nondet — SourceEFLP Nondet — TargetDBE — SourceDBE — TargetDBE Nondet — SourceDBE Nondet — TargetDBE Nondet — Incorrect Target

 MODULE main
 VAR
    step: 0..9;
    int_x: 0..15;
    int_k: 0..3;
    in_secret: 0..3;
    out_public: 0..3;

  ASSIGN

    -- D = 32
    -- L0:
    -- L1: x = 0
    -- L2: k = 0
    -- L3: while (k < 3) {
    -- L4: if (k == 0) {
    -- L5:  x := in_secretput();}
    -- L6: else {x := x + x;}
    -- L7: k := k + 1;
    -- L8: out_publicput(x % k);
    -- L9: END
  init(step):= 0;
  next(step):=
    case
      (step=0): {1};
      (step=1): {2};
      (step=2): {3};
      ((step=3) &  (int_k<3)): {4};
      ((step=3) & !(int_k<3)): {9};
      ((step=4) &  (int_k=0)): {5};
      ((step=4) & !(int_k=0)): {6};
      (step=5): {7};
      (step=6): {7};
      (step=7): {8};
      (step=8): {3};
      (step=9): {9};
      TRUE: step;
    esac;

  init(int_x) := 0;
  next(int_x) :=
    case
      -- ((int_x+int_x)>15): 15;
      (int_x > 7): 15;
      (step=5) : in_secret;
      (step=6) : (int_x + int_x);
      TRUE: int_x;
    esac;

  init(int_k) := 0;
  next(int_k) :=
    case
      (int_k=3): 3;
      (step=7) : int_k + 1;
      TRUE: int_k;
    esac;

  init(out_public) := 0;
  next(out_public) :=
    case
      ((step=8)& !(int_k=0)): (int_x mod int_k);
      TRUE: out_public;
    esac;

  init(in_secret) := {0, 1, 2, 3};
  next(in_secret) := in_secret;

  DEFINE
  halt := (step=9);

The HyperLTL formula

All three optimisations reuse the same observational determinism property: any two traces of the source must match the public outputs of a witness trace, reflecting that the optimised program does not expose new public information.

\[\begin{split}\begin{aligned} \varphi_{\text{opt}} = {} & \forall \pi_A . \forall \pi_B . \exists \pi_C . \\ & \Box\Big( out\_public_{\pi_A} = out\_public_{\pi_C} \land out\_public_{\pi_B} = out\_public_{\pi_C} \Big) \end{aligned}\end{split}\]

LPLP NondetLP LoopsLP Loops w/ BugEFLPEFLP NondetDBEDBE NondetDBE Nondet w/ Bug

Forall A . Forall B . E t . G(((out_public[A][t] = 0) & (out_public[B][t] = 0)) | ((out_public[A][t] = 1) & (out_public[B][t] = 1)) | ((out_public[A][t] = 2) & (out_public[B][t] = 2)) | ((out_public[A][t] = 3) & (out_public[B][t] = 3)))