Speculative Execution Defenses (NuSMV)

Description of the Case Study

Speculative execution can transiently execute instructions whose effects should be discarded, potentially exposing secrets via microarchitectural channels. The benchmark suite models seven optimisation stages, each provided with a non-speculative (_nse) and speculative (_se) version. The systems consist of two cooperating processes that manipulate shared arrays and update a public register var_Y. The HyperLTL property demands that the public output remains zero even when speculation occurs, capturing the absence of observable leakage.

The NuSMV model(s)

Version 1Version 2Version 3Version 4Version 5Version 6Version 7

Non-speculativeSpeculative

MODULE main
VAR
    offset   : 0..2;
    var_Y    : 0..7;
    var_size : 0..4;

    ----------------------------------------------------------------
    -- Flattened proc1: program(0, var_Y, var_size, offset)
    ----------------------------------------------------------------
    proc1_line           : 0..8;

    proc1_arrA_pos0      : 0..4;
    proc1_arrA_pos1      : 0..4;
    proc1_arrA_pos2      : 0..4;
    proc1_arrA_pos3      : 0..4;
    proc1_arrA_pos4      : 0..4;

    proc1_arrB_pos0      : 0..4;
    proc1_arrB_pos1      : 0..4;
    proc1_arrB_pos2      : 0..4;
    proc1_arrB_pos3      : 0..4;
    proc1_arrB_pos4      : 0..4;

    proc1_var_temp_proc1 : 0..4;

    proc1_var_X          : boolean;
    proc1_var_Z          : 0..4;
    proc1_var_W          : 0..4;
    proc1_var_temp_proc2 : 0..4;

    proc1_halt           : boolean;

    ----------------------------------------------------------------
    -- Flattened proc2: program(3, var_Y, var_size, offset)
    ----------------------------------------------------------------
    proc2_line           : 0..8;

    proc2_arrA_pos0      : 0..4;
    proc2_arrA_pos1      : 0..4;
    proc2_arrA_pos2      : 0..4;
    proc2_arrA_pos3      : 0..4;
    proc2_arrA_pos4      : 0..4;

    proc2_arrB_pos0      : 0..4;
    proc2_arrB_pos1      : 0..4;
    proc2_arrB_pos2      : 0..4;
    proc2_arrB_pos3      : 0..4;
    proc2_arrB_pos4      : 0..4;

    proc2_var_temp_proc1 : 0..4;

    proc2_var_X          : boolean;
    proc2_var_Z          : 0..4;
    proc2_var_W          : 0..4;
    proc2_var_temp_proc2 : 0..4;

    proc2_halt           : boolean;

ASSIGN
    ----------------------------------------------------------------
    -- Globals
    ----------------------------------------------------------------
    init(offset) := 0;
    next(offset) := offset;

    next(var_Y) := var_Y;

    init(var_size) := 4;
    next(var_size) := var_size;

    ----------------------------------------------------------------
    -- ========== proc1 ==========
    ----------------------------------------------------------------
    init(proc1_halt) := FALSE;
    next(proc1_halt) :=
        case
            (proc1_line = 2 | proc1_line = 8) : TRUE;
            TRUE : FALSE;
        esac;

    init(proc1_var_temp_proc1) := 0;
    next(proc1_var_temp_proc1) :=
        case
            (proc1_line = 1 & ((var_Y + offset) = 0)) : proc1_arrB_pos0;
            (proc1_line = 1 & ((var_Y + offset) = 1)) : proc1_arrB_pos1;
            (proc1_line = 1 & ((var_Y + offset) = 2)) : proc1_arrB_pos2;
            (proc1_line = 1 & ((var_Y + offset) = 3)) : proc1_arrB_pos3;
            (proc1_line = 1 & ((var_Y + offset) = 4)) : proc1_arrB_pos4;
            TRUE : proc1_var_temp_proc1;
        esac;

    init(proc1_line) := 0;  -- initline for proc1
    next(proc1_line) :=
        case
            -- program1
            (proc1_line = 0 & (var_Y >= var_size)) : 2;
            (proc1_line = 0 & (var_Y <  var_size)) : 1;
            (proc1_line = 1) : 2;
            (proc1_line = 2) : 2;

            -- program2
            (proc1_line = 3) : 4;
            (proc1_line = 4 & (!proc1_var_X)) : 8;
            (proc1_line = 4 &   proc1_var_X)  : 5;
            (proc1_line = 5) : 6;
            (proc1_line = 6) : 7;
            (proc1_line = 7) : 8;
            (proc1_line = 8) : 8;

            TRUE : proc1_line;
        esac;

    init(proc1_var_X) := FALSE;
    next(proc1_var_X) :=
        case
            (proc1_line = 3) : (var_Y < var_size);
            TRUE : proc1_var_X;
        esac;

    init(proc1_var_Z) := 0;
    next(proc1_var_Z) :=
        case
            -- load z
            ((proc1_line = 5) & (var_Y = 0)) : proc1_arrA_pos0;
            ((proc1_line = 5) & (var_Y = 1)) : proc1_arrA_pos1;
            ((proc1_line = 5) & (var_Y = 2)) : proc1_arrA_pos2;
            ((proc1_line = 5) & (var_Y = 3)) : proc1_arrA_pos3;
            ((proc1_line = 5) & (var_Y = 4)) : proc1_arrA_pos4;
            -- shift pointer
            ((proc1_line = 6) & (proc1_var_Z < 3) & (offset = 0)) : proc1_var_Z + 0;
            ((proc1_line = 6) & (proc1_var_Z < 3) & (offset = 1)) : proc1_var_Z + 1;
            ((proc1_line = 6) & (proc1_var_Z < 3) & (offset = 2)) : proc1_var_Z + 2;
            ((proc1_line = 6) & (proc1_var_Z >= 3)) : 4;
            TRUE : proc1_var_Z;
        esac;

    init(proc1_var_W) := 0;
    next(proc1_var_W) :=
        case
            ((proc1_line = 7) & (proc1_var_Z = 0)) : proc1_arrB_pos0;
            ((proc1_line = 7) & (proc1_var_Z = 1)) : proc1_arrB_pos1;
            ((proc1_line = 7) & (proc1_var_Z = 2)) : proc1_arrB_pos2;
            ((proc1_line = 7) & (proc1_var_Z = 3)) : proc1_arrB_pos3;
            ((proc1_line = 7) & (proc1_var_Z = 4)) : proc1_arrB_pos4;
            TRUE : proc1_var_W;
        esac;

    init(proc1_var_temp_proc2) := 0;
    next(proc1_var_temp_proc2) :=
        case
            (proc1_line = 8) : proc1_var_W;
            TRUE : proc1_var_temp_proc2;
        esac;

    -- static arrays
    init(proc1_arrA_pos0) := 0; next(proc1_arrA_pos0) := proc1_arrA_pos0;
    init(proc1_arrA_pos1) := 1; next(proc1_arrA_pos1) := proc1_arrA_pos1;
    init(proc1_arrA_pos2) := 2; next(proc1_arrA_pos2) := proc1_arrA_pos2;
    init(proc1_arrA_pos3) := 3; next(proc1_arrA_pos3) := proc1_arrA_pos3;
    init(proc1_arrA_pos4) := 4; next(proc1_arrA_pos4) := proc1_arrA_pos4;

    init(proc1_arrB_pos0) := 0; next(proc1_arrB_pos0) := proc1_arrB_pos0;
    init(proc1_arrB_pos1) := 1; next(proc1_arrB_pos1) := proc1_arrB_pos1;
    init(proc1_arrB_pos2) := 2; next(proc1_arrB_pos2) := proc1_arrB_pos2;
    init(proc1_arrB_pos3) := 3; next(proc1_arrB_pos3) := proc1_arrB_pos3;
    init(proc1_arrB_pos4) := 4; next(proc1_arrB_pos4) := proc1_arrB_pos4;

    ----------------------------------------------------------------
    -- ========== proc2 ==========
    ----------------------------------------------------------------
    init(proc2_halt) := FALSE;
    next(proc2_halt) :=
        case
            (proc2_line = 2 | proc2_line = 8) : TRUE;
            TRUE : FALSE;
        esac;

    init(proc2_var_temp_proc1) := 0;
    next(proc2_var_temp_proc1) :=
        case
            (proc2_line = 1 & ((var_Y + offset) = 0)) : proc2_arrB_pos0;
            (proc2_line = 1 & ((var_Y + offset) = 1)) : proc2_arrB_pos1;
            (proc2_line = 1 & ((var_Y + offset) = 2)) : proc2_arrB_pos2;
            (proc2_line = 1 & ((var_Y + offset) = 3)) : proc2_arrB_pos3;
            (proc2_line = 1 & ((var_Y + offset) = 4)) : proc2_arrB_pos4;
            TRUE : proc2_var_temp_proc1;
        esac;

    init(proc2_line) := 3;  -- initline for proc2
    next(proc2_line) :=
        case
            -- program1
            (proc2_line = 0 & (var_Y >= var_size)) : 2;
            (proc2_line = 0 & (var_Y <  var_size)) : 1;
            (proc2_line = 1) : 2;
            (proc2_line = 2) : 2;

            -- program2
            (proc2_line = 3) : 4;
            (proc2_line = 4 & (!proc2_var_X)) : 8;
            (proc2_line = 4 &   proc2_var_X)  : 5;
            (proc2_line = 5) : 6;
            (proc2_line = 6) : 7;
            (proc2_line = 7) : 8;
            (proc2_line = 8) : 8;

            TRUE : proc2_line;
        esac;

    init(proc2_var_X) := FALSE;
    next(proc2_var_X) :=
        case
            (proc2_line = 3) : (var_Y < var_size);
            TRUE : proc2_var_X;
        esac;

    init(proc2_var_Z) := 0;
    next(proc2_var_Z) :=
        case
            -- load z
            ((proc2_line = 5) & (var_Y = 0)) : proc2_arrA_pos0;
            ((proc2_line = 5) & (var_Y = 1)) : proc2_arrA_pos1;
            ((proc2_line = 5) & (var_Y = 2)) : proc2_arrA_pos2;
            ((proc2_line = 5) & (var_Y = 3)) : proc2_arrA_pos3;
            ((proc2_line = 5) & (var_Y = 4)) : proc2_arrA_pos4;
            -- shift pointer
            ((proc2_line = 6) & (proc2_var_Z < 3) & (offset = 0)) : proc2_var_Z + 0;
            ((proc2_line = 6) & (proc2_var_Z < 3) & (offset = 1)) : proc2_var_Z + 1;
            ((proc2_line = 6) & (proc2_var_Z < 3) & (offset = 2)) : proc2_var_Z + 2;
            ((proc2_line = 6) & (proc2_var_Z >= 3)) : 4;
            TRUE : proc2_var_Z;
        esac;

    init(proc2_var_W) := 0;
    next(proc2_var_W) :=
        case
            ((proc2_line = 7) & (proc2_var_Z = 0)) : proc2_arrB_pos0;
            ((proc2_line = 7) & (proc2_var_Z = 1)) : proc2_arrB_pos1;
            ((proc2_line = 7) & (proc2_var_Z = 2)) : proc2_arrB_pos2;
            ((proc2_line = 7) & (proc2_var_Z = 3)) : proc2_arrB_pos3;
            ((proc2_line = 7) & (proc2_var_Z = 4)) : proc2_arrB_pos4;
            TRUE : proc2_var_W;
        esac;

    init(proc2_var_temp_proc2) := 0;
    next(proc2_var_temp_proc2) :=
        case
            (proc2_line = 8) : proc2_var_W;
            TRUE : proc2_var_temp_proc2;
        esac;

    -- static arrays
    init(proc2_arrA_pos0) := 0; next(proc2_arrA_pos0) := proc2_arrA_pos0;
    init(proc2_arrA_pos1) := 1; next(proc2_arrA_pos1) := proc2_arrA_pos1;
    init(proc2_arrA_pos2) := 2; next(proc2_arrA_pos2) := proc2_arrA_pos2;
    init(proc2_arrA_pos3) := 3; next(proc2_arrA_pos3) := proc2_arrA_pos3;
    init(proc2_arrA_pos4) := 4; next(proc2_arrA_pos4) := proc2_arrA_pos4;

    init(proc2_arrB_pos0) := 0; next(proc2_arrB_pos0) := proc2_arrB_pos0;
    init(proc2_arrB_pos1) := 1; next(proc2_arrB_pos1) := proc2_arrB_pos1;
    init(proc2_arrB_pos2) := 2; next(proc2_arrB_pos2) := proc2_arrB_pos2;
    init(proc2_arrB_pos3) := 3; next(proc2_arrB_pos3) := proc2_arrB_pos3;
    init(proc2_arrB_pos4) := 4; next(proc2_arrB_pos4) := proc2_arrB_pos4;


DEFINE
    -- halting condition
    halt := ((proc1_line=8) & (proc2_line=8));

The HyperLTL formula

The property asserts that for every trace there exists a witness whose public output var_Y stays at zero in lockstep. All secure non-speculative variants satisfy the property, while speculative versions that leak data violate it.

\[\begin{split}\begin{aligned} \varphi_{\text{se}} = {} & \forall \pi_A . \exists \pi_B . \exists t . \\ & \Box\big( var\_Y_{\pi_A}[t] = 0 \land var\_Y_{\pi_B}[t] = 0 \big) \end{aligned}\end{split}\]

Speculative Safety

Forall A . Exists B . E t .
G((var_Y[A][t] = 0) & (var_Y[B][t] = 0))