Concurrent Leakage Variants (NuSMV)
===================================

Description of the Case Study
-----------------------------

The concurrent leakage suite models how different schedulers and input manipulations influence information flow between three
processes that communicate via shared Boolean registers ``x`` and ``y``. The attacker observes the outputs generated by the
second process. We analyse three variants: a baseline with two processes, a three-process refinement that preserves security,
and a buggy three-process model where the third process forces low inputs to leak the secret. All instances are encoded as
flattened NuSMV models that explicitly capture the scheduler and loop counters.

The NuSMV model(s)
------------------

.. tabs::

    .. tab:: Two processes (secure)

        .. literalinclude :: ../benchmarks_ui/nusmv/security/concleak/concleaks_2procs.smv
            :language: smv

    .. tab:: Three processes (secure)

        .. literalinclude :: ../benchmarks_ui/nusmv/security/concleak/concleaks_3procs.smv
            :language: smv

    .. tab:: Three processes (buggy)

        .. literalinclude :: ../benchmarks_ui/nusmv/security/concleak/concleaks_3procs_bug.smv
            :language: smv

The HyperLTL formula
--------------------

All variants are checked against the same observational determinism property. As long as the high and low inputs agree across
traces, the observable events ``obs_X_is_zero``, ``obs_X_is_one``, ``obs_Y_is_zero``, and ``obs_Y_is_one`` must coincide. The buggy
model violates this requirement because the forced low input reveals the secret.

.. math::

   \begin{aligned}
   \varphi_{\text{conc}} = {} & \forall \pi_A . \exists \pi_B . \forall t_1 . \exists t_2 . \\
   & \Big(
        \Box\big(in\_HIGH_{\pi_A}[t_1] = in\_HIGH_{\pi_B}[t_1]\big)
        \land
        \Box\big(in\_LOW_{\pi_A}[t_1] = in\_LOW_{\pi_B}[t_1]\big)
     \Big) \\
   & \rightarrow
     \Box\Big(
        obs\_X\_is\_zero_{\pi_A}[t_2] = obs\_X\_is\_zero_{\pi_B}[t_2]
        \land
        obs\_X\_is\_one_{\pi_A}[t_2] = obs\_X\_is\_one_{\pi_B}[t_2] \\
   & \qquad\qquad\qquad\land
        obs\_Y\_is\_zero_{\pi_A}[t_2] = obs\_Y\_is\_zero_{\pi_B}[t_2]
        \land
        obs\_Y\_is\_one_{\pi_A}[t_2] = obs\_Y\_is\_one_{\pi_B}[t_2]
     \Big)
   \end{aligned}

.. tabs::

    .. tab:: Observational Determinism

        .. literalinclude :: ../benchmarks_ui/nusmv/security/concleak/od.hq
            :language: hq