Deniability

Description of the Case Study

[SSS20]. In a program, for every possible run \(\pi_{A}\) (e.g., potentially being observed by an adversary), there must exist \(2^N\) different runs, such that each agrees on \(\pi_{A}\) on the observable parts, but differ on secret values. While deniability is usually an example of quantitative hyperproperties [FHT18], here we demonstrate the case when the parameter is \(N = 1\), that is, an \(∀∃∃\) formula:

\[\varphi_{\text{den}} = \forall \pi_A. \exists \pi_B. \exists \pi_C. \Box \left( \left( \mathit{obs}_{\pi_A} \leftrightarrow \mathit{obs}_{\pi_B} \right) \land \left( \mathit{obs}_{\pi_A} \leftrightarrow \mathit{obs}_{\pi_C} \right) \land \left( \mathit{sec}_{\pi_B} \not\leftrightarrow \mathit{sec}_{\pi_C} \right) \right).\]

We evaluate this formula with an Wallet1 and Wallet2 models [BKR09] with a possible attack, where the attacker can speculate the total amount of an account (\(sec\)) by repeatedly withdrawing a fix amount (\(obs\)). The UNSAT outcome for bug-hunting by HyperQB gives a positive verdict (i.e., \(\mathcal{K} |=\varphi_{\text{den}}\))

Benchmarks

Case #8.1Case #8.2

The Model(s)

Deniability Small

--DENIABILITY
--(adopted from: Michael Backes, Boris Köpf, and Andrey Rybalchenko. Automatic discovery and quantification of information leaks. In 2009 30th IEEE Symposium on Security and Privacy)

MODULE main
 VAR
    init_balance: 0..10;
    debits_amount: 1..5;
    PC: 1..6;
    num_itr: 0..11;
    halt: boolean;
 ASSIGN
    -- Initial Conditions
    init(init_balance):= {0,1,2,3,4,5,6,7,8,9,10};
    init(debits_amount) := {1,2,3,4,5};
    init(num_itr):= 0;
    init(PC):= 1; -- but program counter starts at 1.
    init(halt) := FALSE;

    -- Transition Relations
    next(init_balance) :=
      case
        ((PC=3) & (init_balance - debits_amount > 0)): (init_balance - debits_amount);
        TRUE: init_balance;
      esac;

    next(debits_amount) :=
      case
        TRUE: debits_amount;
      esac;

    next(num_itr) :=
      case
        (PC=4): num_itr;
        TRUE: num_itr;
      esac;

    next(PC) :=
      case
        (PC=1): 2; -- num_itr = 0
        ((PC=2) & (init_balance>debits_amount)): 3; -- while (init_balance >= debits amount)
        ((PC=2) & (init_balance<=debits_amount)): 5;
        (PC=3): 4; -- init_balance -= debits_amount
        (PC=4): 2; -- num_itr += 1
        (PC=5): 6; -- Return num_itr += 1
        (PC=6): 6; -- (END)
        TRUE: PC;
      esac;

    next(halt) :=
      case
        (PC=6): TRUE;
        TRUE: halt;
      esac;

DEFINE

Formula

forall A. exists B. exists C.
G(
  (*debits_amount[A]=debits_amount[B]*)
  /\
  (*debits_amount[A]=debits_amount[C]*)
  /\
  ~(*init_balance[B]=init_balance[C]*)
)