Access Hoare Logic

1. Il Problema: I Limiti della Logica di Hoare per la Sicurezza degli Accessi

La logica di Hoare classica è lo standard per la verifica della correttezza dei programmi, basandosi su triple $\{P\}C\{Q\}$. In questo contesto, la precondizione $P$ è una condizione sufficiente: se il programma parte da uno stato che soddisfa $P$ e termina, allora lo stato finale soddisferà $Q$.

Tuttavia, gli autori identificano un limite fondamentale nell'applicare questo approccio alla sicurezza degli accessi (access security), come il controllo degli accessi, l'autenticazione e la gestione delle chiavi digitali (es. chiavi elettroniche per hotel, script di Bitcoin, smart contract).

• La natura del problema: Per la sicurezza degli accessi, non basta sapere che un accesso può essere concesso se certe condizioni sono vere; è necessario garantire che l'accesso venga concesso solo ed esclusivamente se quelle condizioni sono state soddisfatte.
• La direzione inversa: Mentre la logica di Hoare standard va dalle precondizioni alle postcondizioni (direzione in avanti), la sicurezza degli accessi richiede di ragionare a ritroso: se l'accesso è stato concesso (postcondizione $Q$ vera), è necessario che le condizioni di sicurezza iniziali (precondizione $P$) fossero vere.
• Il fallimento dell'approccio standard: In logica di Hoare, una precondizione falsa ($False$) è sempre valida (poiché implica qualsiasi cosa), il che non ha senso per la sicurezza. Nella logica degli accessi, la precondizione deve essere una condizione necessaria, rendendo $True$ la precondizione "più debole" valida in certi contesti, invertendo la logica di implicazione.

2. Metodologia: La Logica di Hoare per gli Accessi (Access Hoare Logic - aHl)

Gli autori propongono un nuovo formalismo chiamato Access Hoare Logic (aHl), basato su triple di accesso denotate come $\langle P \rangle C \langle Q \rangle$.

Definizione Semantica

La triple $\langle P \rangle C \langle Q \rangle$ è valida se e solo se:
$$\forall s, s' [s \xrightarrow{C} s' \land Q(s') \rightarrow P(s)]$$
Ciò significa: se l'esecuzione del programma $C$ parte dallo stato $s$, termina in uno stato $s'$ che soddisfa la postcondizione $Q$, allora lo stato iniziale $s$ deve aver soddisfatto la precondizione $P$. $P$ è una condizione necessaria per $Q$.

Il Calcolo (Rules)

Gli autori definiscono un calcolo diretto per aHl, evitando di ridurlo semplicemente alla logica di Hoare tramite negazione (che introdurrebbe complessità sintattiche e problemi con la logica intuizionistica). Le regole principali includono:

• Assegnazione: $\langle P[E/V] \rangle V := E \langle P \rangle$ (analoga a Hoare, ma applicata al flusso inverso).
• Composizione: Se $\langle P \rangle S \langle R \rangle$ e $\langle R \rangle T \langle Q \rangle$, allora $\langle P \rangle S;T \langle Q \rangle$.
• Condizionale: Le regole per if-then-else sono modificate per gestire le implicazioni inverse. Ad esempio, per il ramo then, si richiede $\langle B \rightarrow P \rangle S \langle Q \rangle$.
• Ciclo While: La regola richiede che l'invariante sia mantenuto in modo che, se il ciclo termina (quando $\neg B$ è vero), l'invariante implichi la precondizione necessaria.

Relazione con la Logica di Hoare Standard

Viene stabilito un legame fondamentale tra le due logiche:

• La precondizione più debole (weakest pre-condition) per una triple di Hoare corrisponde alla precondizione più forte (strongest pre-condition) per una triple di accesso, a patto che il programma termini.
• Formalmente: $P_s(C, Q) = P_w(C, Q) \cap \{s \mid C \text{ termina su } s\}$.
• Per programmi totali (che terminano sempre), le precondizioni più deboli di Hoare e le più forti di aHl coincidono.

3. Contributi Chiave

1. Definizione Formale di aHl: Introduzione di un calcolo completo e sonoro per ragionare sulla sicurezza degli accessi come condizione necessaria, non solo sufficiente.
2. Dimostrazione di Correttezza e Completezza:
   • Soundness (Correttezza): Qualsiasi triple provabile in aHl è semanticamente valida.
   • Completeness (Completezza): Qualsiasi triple semanticamente valida è provabile in aHl. La prova è costruita direttamente tramite induzione strutturale sul programma, utilizzando il concetto di precondizione più forte ($P_s$).
3. Distinzione dalla "Incorrectness Logic": Gli autori chiariscono la differenza fondamentale tra aHl e la logica di incorrectness (che usa under-approximations per trovare bug). Mentre la logica di incorrectness lavora su trasformatori in avanti (forward transformers) per trovare stati finali raggiungibili da stati iniziali "cattivi", aHl lavora su trasformatori all'indietro (backwards transformers) per garantire che stati finali "sicuri" provengano solo da stati iniziali "sicuri".
4. Applicazione alla Logica Intuizionistica: Viene notato che, a differenza della riduzione tramite negazione che richiederebbe logica classica, la maggior parte delle prove in aHl può essere condotta in logica intuizionistica, rendendola compatibile con dimostratori di teoremi come Coq/Rocq.

4. Risultati ed Esempi Applicativi

Gli autori dimostrano l'utilità di aHl attraverso tre casi di studio, formalizzati e verificati:

1. Chiavi Elettroniche per Hotel:
   • Analizza un sistema dove una carta contiene due chiavi ($ck1, ck2$) e la serratura ha una chiave interna ($dk$).
   • Dimostra che una specifica implementazione del codice (P1) è sicura (l'accesso è concesso solo se la chiave è valida), mentre una versione ambigua (P2) non lo è, poiché P2 concede l'accesso indipendentemente dalla chiave in alcuni rami, violando la necessità della precondizione.
2. Bitcoin e Smart Contracts:
   • Analizza lo script di blocco scriptPubKeyP2PKH.
   • Formalizza la sicurezza come: se la transazione termina con successo (stack top = true), allora è necessario che la firma e l'indirizzo forniti corrispondano a quelli registrati.
   • Traduce lo stack-based Bitcoin script in un linguaggio imperativo (while) e dimostra la validità della triple di accesso.
3. Controllo Accessi con Liste (While Loops):
   • Un programma che cerca una chiave in una lista.
   • Dimostra come costruire un'invariante di ciclo appropriata che garantisca che acc = true (accesso concesso) solo se la chiave era effettivamente presente nella lista iniziale.

5. Significato e Implicazioni

• Nuovo Paradigma di Verifica: Il paper stabilisce che la sicurezza degli accessi non è un sottoprodotto della correttezza funzionale, ma richiede un formalismo specifico che inverta la direzione del ragionamento logico.
• Impatto su Blockchain e Sicurezza: Fornisce un fondamento teorico rigoroso per la verifica di smart contract e sistemi crittografici, dove l'accesso alle risorse digitali deve essere garantito come condizione necessaria e non solo sufficiente.
• Strumenti di Verifica: Suggerisce che strumenti esistenti (come SPARK o Dafny) potrebbero essere estesi o adattati per supportare aHl, permettendo di verificare proprietà di sicurezza che attualmente sfuggono alla logica di Hoare standard.
• Brevetto: Gli autori menzionano di aver depositato un brevetto basato su questo lavoro per la generazione di condizioni di verifica per la sicurezza degli accessi, indicando un potenziale impatto industriale immediato.

In sintesi, questo lavoro colma un divario teorico fondamentale, offrendo un linguaggio formale per garantire che i sistemi informatici non concedano mai accessi non autorizzati, trasformando la sicurezza da una proprietà "se... allora..." a una proprietà "solo se... allora...".