Come scrivere monitor a runtime e oracoli di test

Questa guida mostra due modi di usare a runtime una specifica Lean dimostrata, quando il codice da verificare non è Lean:

• Un monitor a runtime riceve gli eventi di un sistema in esecuzione, uno alla volta. È dimostrato che accetta esattamente le tracce di eventi che un protocollo consente, quindi ogni violazione che segnala è reale.
• Un oracolo di test è un’implementazione di riferimento dimostrata. Il codice scritto a mano, in qualsiasi linguaggio, viene verificato rispetto a esso invece di essere accettato sulla fiducia.

L’esempio di riferimento è lungo-rs/examples/oracle-monitor, una politica di controllo degli accessi con un protocollo di sessione.

Scrivi il protocollo

Un protocollo (Lungo.Trace.Protocol ε) è l’insieme delle tracce di eventi a cui un componente può partecipare, chiuso rispetto ai prefissi. Il suo lato eseguibile è un reducer (Lungo.Trace.Reducer ε σ): uno stato iniziale e un passo che accetta un evento, dando lo stato successivo, oppure lo rifiuta.

import Lungo

namespace Access

open Lungo Lungo.Trace

inductive Event where
  | signIn (user role : String)
  | access (user action : String)
  | signOut (user : String)

/-- Who is signed in, with their role. -/
structure Session where
  users : List (String × String)

/-- The session after `e`; `none` when `e` breaks the protocol. -/
def next (policy : List Rule) (s : Session) (e : Event) : Option Session := ...

/-- No one signed in: the session a host starts monitoring from. -/
def start : Session := ⟨[]⟩

/-- The session protocol under `policy`. -/
@[lungo_spec "lungo.protocol"]
noncomputable def Sessions (policy : List Rule) : Protocol Event :=
  (Reducer.mk start (next policy)).protocol

Un protocollo è un oggetto logico, non codice da eseguire, quindi Sessions è noncomputable. lungo non lo esporta mai, e @[lungo_spec] lo registra come specifica che i claim possono citare.

Costruisci il monitor

Un monitor (Lungo.Monitor ε σ) ha uno stato iniziale start e un passo step : σ → ε → Except String σ. Un passo dà lo stato successivo, oppure il motivo per cui l’evento è una violazione. Monitor.run elabora un’intera traccia, Monitor.Accepts m t dice che m accetta la traccia t dal suo stato iniziale, e Monitor.Sound m p dice che m accetta esattamente le tracce che il protocollo p consente.

Costruisci i monitor con questi combinatori. Ognuno ha il proprio teorema di correttezza:

L’esempio monitora il proprio reducer:

/-- Why `e` breaks the protocol in session `s`. -/
def reason (s : Session) (e : Event) : String := ...

private def monitor (policy : List Rule) : Monitor Event Session :=
  Monitor.ofReducer ⟨start, next policy⟩ reason

/-- The session after `e`, or the violation it is. -/
def observe (policy : List Rule) (s : Session) (e : Event) : Except String Session :=
  (monitor policy).step s e

L’host ha bisogno dello stato iniziale e del passo come funzioni, quindi gli export sono start e observe. Il valore Monitor in sé non serve fuori da Lean, quindi è private.

Afferma che è corretto

Enuncia il claim sulle funzioni esportate, con la relazione lungo.monitors:

@[lungo_claim "lungo.monitors" subject start observe spec Sessions]
theorem observe_sound (policy : List Rule) :
    (Monitor.mk start (observe policy)).Sound (Sessions policy) :=
  Monitor.ofReducer_sound (Reducer.mk start (next policy)) reason

Un claim lungo.monitors deve enunciare Lungo.Monitor.Sound m p, con m che menziona ogni soggetto. lungo verifica questa forma quando l’attributo viene applicato, e di nuovo quando legge i record. Perché la build fallisca se il claim viene rimosso o si basa su sorry, richiedilo:

# lungo.toml
[assurance]
require-claims = ["Access.observe"]

(Builder::require_claims("Access.observe") in build.rs.)

Passagli gli eventi dall’host

L’host conserva la sessione e chiama observe con ogni evento. Che cosa fare di una violazione (registrarla, rifiutare la richiesta, avvisare qualcuno) lo decide l’host; la dimostrazione garantisce soltanto che si tratta di una violazione.

Rust

let mut session = access::start();
for event in events {
    match access::observe(policy.clone(), session.clone(), event) {
        Ok(next) => session = next,
        Err(reason) => eprintln!("violation: {reason}"),
    }
}

Python

session = access.start()
for event in events:  # access.EventSignIn("ada", "editor"), access.EventAccess("ada", "write"), …
    verdict = access.observe(policy, session, event)
    if isinstance(verdict, lungo_py.Ok):
        session = verdict.value
    else:
        log.warning("violation: %s", verdict.error)

Go

session, err := access.Start()
if err != nil {
	return err
}
for _, e := range events { // access.EventSignIn{User: "ada", Role: "editor"}, …
	verdict, err := access.Observe(policy, session, e)
	if err != nil {
		return err
	}
	if verdict.Ok {
		session = verdict.Value
	} else {
		log.Printf("violation: %s", verdict.Error)
	}
}

TypeScript

let session = p.start();
for (const e of events) { // { kind: "signIn", user: "ada", role: "editor" }, …
  const verdict = p.observe(policy, session, e);
  if (verdict.ok) session = verdict.value;
  else console.warn(`violation: ${verdict.error}`);
}

Swift

var session = try start()
for e in events { // .signIn(user: "ada", role: "editor"), …
    switch try observe(policy, session, e) {
    case .ok(let next): session = next
    case .error(let reason): print("violation: \(reason)")
    }
}

C

access_start e access_observe restituiscono la sessione e il valore Except. Leggi quest’ultimo con lungo_value_is_ok e lungo_value_get_except.

Usa una funzione dimostrata come oracolo di test

Un oracolo è una specifica che si può eseguire. Nell’esempio, evaluate decide una richiesta rispetto a una politica, ed è dimostrato che decide esattamente la relazione Permits:

@[lungo_spec "lungo.relation"]
def Permits (policy : List Rule) (r : Request) : Prop :=
  (∃ rule ∈ policy, rule.covers r = true ∧ rule.effect = .allow) ∧
    ∀ rule ∈ policy, rule.covers r = true → rule.effect ≠ .deny

@[lungo_role "lungo.oracle"]
def evaluate (policy : List Rule) (r : Request) : Bool := ...

@[lungo_claim "lungo.decides" subject evaluate spec Permits]
theorem evaluate_decides (policy : List Rule) (r : Request) :
    evaluate policy r = true ↔ Permits policy r := ...

@[lungo_role "lungo.oracle"] registra lo scopo dell’export. Il ruolo compare nella voce dell’export in assurance.json e nella sua rappresentazione in ogni linguaggio, per esempio __meta::declaration("Access.evaluate").unwrap().assurance.roles in Rust.

Il codice di produzione che deve essere veloce, come un valutatore indicizzato per ruolo e azione, è scritto a mano e verificato rispetto all’oracolo su input generati:

for seed in 0..300 {
    let rules = policy(seed, (seed % 8) as usize);
    let index = Index::new(&rules);
    let lean = List::from(rules);
    for role in ROLES {
        for action in ACTIONS {
            let oracle = access::evaluate(lean.clone(), Request { role: role.into(), action: action.into() });
            assert_eq!(index.permits(role, action), oracle, "seed {seed}: {role} {action}");
        }
    }
}

Il test Python dell’esempio fa lo stesso con un valutatore Python. Un valutatore che ignora le regole di divieto fallisce il test entro pochi seed. Poiché è dimostrato che l’oracolo decide Permits, concordare con esso significa concordare con la specifica su ogni input verificato, non con un’altra implementazione che potrebbe avere lo stesso difetto.

Vedi anche

• Come dichiarare claim sugli export
• La libreria Lean di lungo: Lungo.Trace e Lungo.Monitor