Extending Lagois Connections for Secure Information Flow to n Organizations
Author
Ståhl, Casper
Term
4. term
Education
Publication year
2025
Abstract
Dette speciale udvider rammeværket for Lagois-forbindelser til sikker informationsstrøm fra to organisationer til vilkårlige netværk af organisationer. Motiveret af præcisionstab ved kædede udvidelser og sikkerhed, der kun er garanteret for endepunkter, modellerer vi organisationer som gittere med parvise Lagois-forbindelser og løfter sikkerhedsbegrebet til netværksniveau via en induceret tværorganisatorisk flowrelation. Vi giver flere ækvivalente definitioner af netværkssikkerhed, beskriver beslutningsprocedurer der typisk har kubisk tidskompleksitet, og udvikler bevisværktøjer, herunder et induktionsprincip for afledte selvforbindelser. Vi identificerer topologier, der altid er sikre: netværk med skov-topologi, netværk der opfører sig som skove, og skove af sikre delnetværk; centrale resultater for de to første er mekanisk bevist i Coq. Vi kobler den statiske ramme til en småskridts operationel model med sammenflettet eksekvering og synkron kommunikation og definerer (fremdriftsinsensitiv) ikke-interferens parameteriseret ved en angribers placering og observationskraft. Vi leverer ikke en håndhævelsesmekanisme eller et lydsthedsresultat, men formoder at begge er opnåelige. Rammeværket er generelt og kan, under besluttelig identifikation af organisationer, udvides til uendelige netværk over partielle ordener; flere resultater er uafhængige af de konvergensaksiomer, der ofte antages for Lagois-forbindelser.
This thesis extends the framework of Lagois connections for secure information flow from two organizations to arbitrary networks. Motivated by loss of label precision in chained extensions and security guarantees stated only for endpoints, we model organizations as lattices with pairwise Lagois connections and lift security to the network level via an induced cross-organization flow relation. We provide several equivalent definitions of network security, give decision procedures that are generally cubic in the size of the network, and develop proof tools, including an induction principle on derived self-connections. We identify topologies that are always secure: networks with forest topology, networks that behave as forests, and forests of secure subnetworks; key results for the first two are mechanically proved in the Coq proof assistant. We connect the static framework to a small-step operational model with interleaved execution and synchronized communication and define (progress-insensitive) noninterference parameterized by an attacker’s location and observational power. We do not provide an enforcement mechanism or a soundness result, but conjecture both are attainable. The framework is general and, under decidable identification of organizations, extends to infinite networks over partial orders; several results do not depend on the convergence axioms often assumed for Lagois connections.
[This summary has been generated with the help of AI directly from the project (PDF)]
Documents