A Type System for Purpose Limitation
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2022
Författare
Wang, Chengyuan
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
Purpose Limitation is a GDPR [1] principle that restricts software to only collect and process personal data for specified purposes to which the user consented. However, there are few works that implement automatic purpose limitation check in software. Fortunately, there is a similar policy called confidentiality with lots of previous works. In practice, to ensure this principle, the policy checks are usually implemented by an Information-Flow Control (IFC) framework. This technique restricts how data flows within the software to prevent policy violations. Previously, Stefan et al. have done a series of works to use IFC to ensure confidentiality and present a concrete implementation as a Haskell Library [2, 3]. In this project, we present a static IFC system as a type system which checks the purpose limitation statically. Additionally, we embed this type system into Haskell and formalize it in Agda. The former implementation presents a concrete example of how our type system would behave in an industrial language, while the latter proves our type
system’s correctness.
Beskrivning
Ämne/nyckelord
Type system , Security & Privacy , Information-flow control , Noninterference