I am a PhD student in the Information Security division at Chalmers University of Technology supervised by Alejandro Russo. My research focuses on programming languages and security.
Oct. 2021 
Pure InformationFlow Control with Effects Made Simple
(unpublished)
Informationflow control (IFC) is a promising technology to protect data confidentiality. The foundational work on the Dependency Core Calculus (DCC) positions monads as a suitable abstraction for enforcing IFC. Pure functional languages with effects, like Haskell, can provide IFC as a library (MAC, LIO etc.), a minor task compared to implementing compilers for IFC from scratch. Previous works on IFC as a library introduce ad hoc primitives to type programs whose effects do not depend on the sensitive data in context. In this work, we start afresh and ask ourselves: what would we need to extend an effectfree language for IFC (e.g., DCC) with secure effects? The answer turns out to be elegant and simple. In a pure language with effects there is a natural place where information flows from sensitive data to effects need to be restricted, and when effects are tracked in a more finegrained fashion than Haskell's IO monad (e.g., with a graded monad) then a single primitive is enough to allow the secure flows! To support our insight, we present and prove secure several IFC enforcement mechanisms based on extensions of the Sealing Calculus (SC) with effects using a graded monad. Effects that depend on sensitive data are secured through a novel primitive distr. All of our security guarantees are mechanized in the Agda proof assistant. Moreover, we provide an implementation of these mechanisms as a new Haskell library for IFC. 
Oct. 2021 
Normalization for Fitchstyle Modal Calculi
(unpublished)
Fitchstyle modal lambda calculi enable programming with necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator that is denoted by a lock. The addition of locks simplifies the formulation of typing rules for calculi that incorporate different modal axioms, but each variant demands different, tedious and seemingly ad hoc syntactic lemmas to prove normalization. In this work, we take a semantic approach to normalization, called normalization by evaluation (NbE), by leveraging the possibleworld semantics of Fitchstyle calculi to yield a more modular approach to normalization. We show that NbE models can be constructed for calculi that incorporate the K, T and 4 axioms of modal logic, as suitable instantiations of the possibleworld semantics. In addition to existing results that handle 𝛽equivalence, our normalization result also considers 𝜂equivalence for these calculi. Our key results have been mechanized in the proof assistant Agda. Finally, we showcase several consequences of normalization for proving metatheoretic properties of Fitchstyle calculi as well as programminglanguage applications based on different interpretations of the necessity modality. 
CSF 2020 
Securing Asynchronous Exceptions
33rd IEEE Computer Security Foundations Symposium
Languagebased informationflow control techniques often rely on special purpose (often ad hoc) primitives to deal with different sources of covert channels (e.g., caches, the scheduler, or garbage collector) that originate in the runtime system, beyond the scope of language constructs. Since these piecemeal solutions may not compose securely, there is a need for a unified mechanism to control covert channels. As a first step towards this goal, we argue for the design of a general interface that allows programs to safely interact with the runtime system and the computing resources of the system. To coordinate the communication between programs and the runtime systems, we propose the use of asynchronous exceptions (interrupts), which, to the best of our knowledge, have not been considered before in the context of IFC languages. Since asynchronous exceptions can be raised at any point during execution—often due to the occurrence of an external event—threads must temporarily mask them out when manipulating locks and shared data structures to avoid deadlocks and breaking program invariants. Crucially, the naive combination of asynchronous exceptions with existing features of IFC languages (e.g., concurrency and synchronization variables) may open up new possibilities of information leakage. In this paper, we present MAC_{async} , a concurrent (statically enforced) language for informationflow control that, as a novelty, includes asynchronous exceptions. We show how asynchronous exceptions easily enable (out of the box) useful programming patterns like speculative execution and some degree of resource management. We prove that programs in MAC_{async} satisfy progresssensitive noninterference and mechanize our formal claims in the Agda proof assistant. 
PLAS 2019 
Simple Noninterference by Normalization
14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security
Informationflow control (IFC) languages ensure programs preserve the confidentiality of sensitive data. Noninterference, the desired security property of such languages, states that public outputs of programs must not depend on sensitive inputs. In this paper, we show that noninterference can be proved using normalization. Unlike arbitrary terms, normal forms of programs are wellprincipled and obey useful syntactic propertieshence enabling a simpler proof of noninterference. Since our proof is syntaxdirected, it offers an appealing alternative to traditional semantic based techniques to prove noninterference. In particular, we prove noninterference for a static IFC calculus, based on Haskell's seclib library, using normalization. Our proof follows by straightforward induction on the structure of normal forms. We implement normalization using normalization by evaluation and prove that the generated normal forms preserve semantics. Our results have been verified in the Agda proof assistant. 
TyDe 2018 
From Algebra to Abstract Machine: A Verified Generic Construction
3rd ACM SIGPLAN International Workshop on TypeDriven Development
Many functions over algebraic datatypes can be expressed in terms of a fold. Doing so, however, has one notable drawback: folds are not tailrecursive. As a result, a function defined in terms of a fold may raise a stack overflow when executed. This paper defines a datatype generic, tailrecursive higherorder function that is guaranteed to produce the same result as the fold. Doing so combines the compositional nature of folds and the performance benefits of a handwritten tailrecursive function in a single setting. 
NWPT 2021 
InformationFlow Control and Effects
32nd Nordic Workshop on Programming Theory

TYPES 2021 
Semantic Analysis of Normalization by Evaluation for FitchStyle Modal Lambda Calculi
27th International Conference on Types for Proofs and Programs
Fitchstyle modal lambda calculi provide a solution to programming necessity modalities (denoted by a □) in a typed lambda calculus by extending the typing context with a delimiting operator (denoted by a 🔒). In this work, we perform a semantic analysis of normalization by evaluation (NbE) for Fitchstyle modal lambda calculi by beginning with the calculus λ_{IK}—a system for the most basic modal logic IK (for "intuitionistic" and "Kripke")—as our object of study. We construct an NbE model for λ_{IK}, and show that it is an instance of the possibleworlds semantics for IK. The presented NbE procedure has been formalized in the proof assistant Agda. 
MSc. Thesis 
Verified TailRecursive Folds through Dissection
Master in Computing Science, Utrecht University
The functional programming paradigm advocates a style of programming based on higherorder functions over inductively defined datatypes. A fold, which captures their common pattern of recursion, is the prototypical example of such a function. However, its use comes at a price. The definition of a fold is not tailrecursive which means that the size of the stack during execution grows proportionally to the size of the input. McBride has proposed a method called dissection, to transform a fold into its tailrecursive counterpart. Nevertheless, it is not clear why the resulting function terminates, nor it is clear that the transformation preserves the fold’s semantics. In this thesis, we formalize the construction of such tailrecursive function and prove that it is both terminating and equivalent to the fold. In addition, using McBride’s dissection, we generalize the tailrecursive function to work on any algebra over any regular datatype. 