To Secure a Flow
From Specification to Enforcement of Information Flow Control
Tid: Ti 2025-03-11 kl 09.00
Plats: Kollegiesalen, Brinellvägen 8, Stockholm
Språk: Engelska
Ämnesområde: Datalogi
Respondent: Amir M. Ahmadian , Teoretisk datalogi, TCS, Language-Based Security
Opponent: Professor Limin Jia, Carnegie Mellon University, Pittsburgh, PA, US
Handledare: Associate Professor Musard Balliu, Teoretisk datalogi, TCS; Professor Dilian Gurov, Teoretisk datalogi, TCS
QC 20250214
Abstract
Användningen av mjukvara har blivit alltmer utbredd och påverkar i stort sett alla aspekter av våra dagliga liv. I detta sammanhang är det viktigare än någonsin att säkerställa säkerheten i mjukvarusystem, eftersom sårbarheter kan leda till betydande sociala och ekonomiska konsekvenser. Informationsflödeskontroll är ett forskningsområde som fokuserar på att utveckla metoder och tekniker för att tillhandahålla starka säkerhetsgarantier mot mjukvaruattacker och sårbarheter. Informationsflödeskontroll uppnår detta genom att spåra hur information flödar i ett program och säkerställa att känslig data inte når obehöriga utdata. Denna process kan vara utmanande eftersom den kräver en exakt definition av mjukvarusystemets säkerhetspolicy och utveckling av mekanismer för att upprätthålla policyn mot olika typer av angripare med varierande förmågor.
I denna avhandling undersöker vi språkbaserade tillvägagångssätt för att upprätthålla informationsflödeskontroll i mjukvarusystem, med fokus på att definiera lämpliga säkerhetspolicies, angriparmodeller och mekanismer för verkställande för att proaktivt säkra moderna mjukvarusystem. Avhandlingen bidrar till den aktuella forskningen inom informationsflödesäkerhet på flera sätt, både teoretiska och praktiska, genom att undersöka fyra centrala forskningsfrågor: att definiera icke-triviala säkerhetspolicies för verkliga scenarier, att utveckla relevanta angriparmodeller, att skapa mekanismer för att upprätthålla villkor för informationsflödesäkerhet samt att tillämpa språkbaserade tekniker på verkliga programmeringsspråk. När det gäller policy-specifikation presenterar vi ett kunskapsbaserat säkerhetsramverk som kan uttrycka många varianter av dynamiska policies samt Determinacy Quantale, en ny semantisk modell för att uttrycka disjunktiva policies i databasstödda program, med särskilt fokus på intressekonfliktklasser. Vi undersöker angriparens roll i att definiera säkerhetsvillkor, särskilt två typer av aktiva angripare och tre typer av passiva angripare med olika grad av förmågor. Vi undersöker mekanismer för efterlevnad, såsom säkerhetstypsystem och symbolisk exekvering, som utvecklats för att statiskt upprätthålla olika informationsflödessäkerhetspolicies. Slutligen, för att demonstrera användbarheten av språkbaserade metoder i verkliga program, implementerar och utvärderar vi de föreslagna mekanismerna på språk Java och P4.