The use of software has become increasingly prevalent, affecting nearly every aspect of our daily lives.  In this landscape, ensuring the security of software systems is more critical than ever, as vulnerabilities can lead to significant social and financial consequences.  Information flow control is a research area focused on developing methods and techniques to provide strong security guarantees against software attacks and vulnerabilities.  Information flow control achieves this by tracking how information flows within a program, ensuring that sensitive data does not reach unauthorized outputs.  This process can be challenging as it requires precisely defining the software system's security policy and developing mechanisms to enforce that policy against different types of attackers with varying capabilities.  

In this thesis, we examine language-based approaches to enforcing information flow control in software systems, with a focus on defining appropriate security policies, attacker models, and enforcement mechanisms to proactively secure modern software systems.  The thesis contributes to the state of the art of information flow security in several directions, both theoretical and practical, by investigating four key research questions: defining non-trivial security policies for real-world scenarios, developing appropriate attacker models, creating mechanisms to enforce information flow security conditions, and applying language-based techniques to real-world programming languages.  On the policy specification side, we provide a knowledge-based security framework capable of expressing many variants of dynamic policies as well as the Determinacy Quantale, a new semantic model for expressing disjunctive policies in database-backed programs, focusing on the conflict-of-interest classes.  We examine the role of attackers in defining security conditions, specifically two types of active attackers and three types of passive attackers with various degrees of capabilities.  Moreover, we investigate enforcement mechanisms, such as security type systems and symbolic execution, developed to statically enforce various information flow security policies.  Finally, to demonstrate the applicability of language-based approaches in real-world programs, we implement and evaluate the proposed enforcement mechanisms in the programming languages Java and P4.

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.