Generalized Non-interference: Banking Audit Logs (NuSMV)

Description of the Case Study

Generalized non-interference [GM82] requires that observables remain insensitive to confidential choices. We study three NuSMV models of an online banking login workflow, each refining the instrumentation of the authentication stack. The property of interest—Always-Equivalent Evidence (AEE)—states that, for any two executions, there must exist a third execution whose return code matches one run while its audit trail mirrors the other. This captures the idea that public transaction logs should not reveal which credentials were accepted. HyperQB, under halting pessimistic semantics, reports SAT for all three models: the witness pairs a successful login trace with one that records a failed attempt. Because every version writes the outcome directly into loginfo, no execution can combine the success code from one run with the failure log from another, demonstrating a persistent violation of AEE even after successive simplifications of the system model.

The NuSMV model(s)

MODULE main
VAR 
    password : 0..2; -- (none = 0, userPassword = 1, adminPassword = 2, badPassword = 3)
    username : 0..2; -- (none = 0, user = 0, devadmin = 1)
    matchedUserPassword : 0..1; -- 
    matchedAdminPassword : 0..1; -- 
    loginfo : 0..2; -- (none = 0, success = 1, failure = 2)
    result : 0..2; -- (none = 0, 1 = login, badLogin = 2, 3 = No connection)
    httpclient : 0..2; -- (unset = 0, userlogin = 1, devlogin = 2)
    serverport : 0..1; -- (unset = 0, set = 1)
    serverip : 0..1; -- (unset = 0, set = 1)
    creds : 0..2; -- (nothing = 0, user = 1, dev = 2)
    startactivity : 0..2; -- (none = 0, userLoginSequence = 1; AdminLoginSequence = 1)
    date : 0..11; -- Due to the over-simplified hq property, loginfo has to have everything the same so extra features like date violate it

ASSIGN
    -- Starting values
    init(password) := {0, 2}; -- none
    init(username) := {0, 1, 2}; --
    init(matchedUserPassword) := {0, 1};
    init(matchedAdminPassword) := {0, 1};
    init(serverip) := 1; -- set 
    init(serverport) := 1; -- set 
    init(loginfo) := 0; -- empty
    init(result) := 0; -- unknown
    init(startactivity) := 0; -- none
    init(httpclient) := 0; --nada
    init(creds) := 0; --
    init(date) := {0,1,2,3,4,5,6,7,8,9,10,11};
 
    --Define Statics
    next(date) := date;
    next(password) := password;
    next(username) := username;
    next(matchedUserPassword) := matchedUserPassword;
    next(matchedAdminPassword) := matchedAdminPassword;
    next(serverip) := serverip;
    next(serverport) := serverport;

    --Transition Rules
    next(httpclient) := 
    case
        ((serverip = 1) & (serverport = 1)) : username;
        TRUE : 0;
    esac;

    next(result) := 
    case
        (httpclient = 0) : result;
        (((password = matchedUserPassword) & (httpclient = 1)) | ((password = matchedAdminPassword) & (httpclient = 2))) : 1;
        TRUE : 2;
    esac;

    next(loginfo) := 
    case
        (result = 0) : loginfo;
        TRUE : result;
    esac;

    next(creds) := 
    case
        ((password = matchedAdminPassword) & (httpclient = 2)) : 2; --Give Admin Creds
        ((password = matchedUserPassword) & (httpclient = 1)) : 1; --Give User Creds
        TRUE : 0;
    esac;

    next(startactivity) := 
    case
        (creds = 0): 0;
        (creds = 1): 1;
        (creds = 2): 2;
        TRUE: startactivity;
    esac;


DEFINE
    halt := ((result = 1) | (result = 2));

The HyperLTL formula(s)

The AEE hyperproperty formalises the decoupling between observable results and audit evidence. For any traces \(\pi_A\) and \(\pi_B\), HyperQB must witness a third trace \(\pi_C\) that always agrees with \(\pi_A\) on the return code result while reproducing the loginfo sequence of \(\pi_B\). If no such \(\pi_C\) exists, the audit log leaks information about which credentials succeeded.

\[\varphi_{\text{GMNI}} = \forall \pi_A . \forall \pi_B . \exists \pi_C . \Box(\mathit{result}_{\pi_A} = \mathit{result}_{\pi_C}) \land \Box(\mathit{loginfo}_{\pi_B} = \mathit{loginfo}_{\pi_C})\]
Forall A . Forall B . Exists C . 
G(result[A] = result[C]) & G(loginfo[B] = loginfo[C])

References