Investigating the Benets of Ownership in Static Information Flow Security
Authors
Lepka, Nikolaj ; Rasmussen, Morten Meyer
Term
4. term
Education
Publication year
2019
Abstract
This thesis investigates whether Rust-style ownership can strengthen static information flow security in languages with side effects, and how a security monad can complement ownership to reduce unintended leaks of secret data. We first design a small While language with formal syntax, semantics, and a type system, then extend it with an ownership model featuring moves, references, and explicit scoping, and finally introduce a security monad that encapsulates computations involving sensitive information, yielding SecWhile. Using illustrative examples (e.g., input validation and access control) and the accompanying rules, we discuss how ownership limits aliasing and lifetimes to lower leakage risk, and where ownership alone is insufficient. In those cases, monadic encapsulation of secrets and side effects can make accidental exposure harder. The work relates to prior efforts on taint analysis and a security library, and aims to show that combining ownership with a security monad provides clearer static guarantees about information flow. The included pages focus on language construction, examples, and formal rules; definitive empirical results beyond these discussions are not presented in the excerpt.
Denne afhandling undersøger, om Rust-inspireret ownership kan styrke statisk informationsflow-sikkerhed i sprog med sideeffekter, og hvordan en sikkerhedsmonade kan supplere ownership for at mindske utilsigtede lækager af hemmelige data. Vi udvikler først et lille While-sprog med formel syntaks, semantik og typesystem, udvider det dernæst med et ownership‑system med flytning, referencer og eksplicitte scopes, og introducerer til sidst en sikkerhedsmonade, der kapsler beregninger med følsomme oplysninger, hvilket resulterer i SecWhile. Gennem illustrative eksempler (fx validering af brugerinput og adgange) og de tilhørende regler diskuterer vi, hvordan ownership kan begrænse aliasering og levetid på data og dermed reducere risikoen for lækage, samt hvor det ikke er tilstrækkeligt. I de tilfælde kan en monadisk indkapsling af hemmeligheder og sideeffekter gøre utilsigtet eksponering vanskeligere. Arbejdet relaterer til tidligere arbejde med taintanalyse og en sikkerhedsbibliotekstilgang og søger at vise, at kombinationen af ownership og en sikkerhedsmonade giver klarere, statiske garantier for informationsflow. De første kapitler fokuserer på opbygningen af sproget, eksempler og de formelle regler; egentlige empiriske resultater ud over disse diskussioner er ikke præsenteret i det medtagne uddrag.
[This apstract has been generated with the help of AI directly from the project full text]