A Type System for Purpose Limitation

Abstract

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.