Carlos Tomé Cortiñas

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 Information-Flow Control with Effects Made Simple
Carlos Tomé Cortiñas and Alejandro Russo

Information-flow 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 effect-free 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 fine-grained 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 Fitch-style Modal Calculi
Nachiappan Valliappan, Fabian Ruch and Carlos Tomé Cortiñas

Fitch-style 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 possible-world semantics of Fitch-style 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 possible-world 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 meta-theoretic properties of Fitch-style calculi as well as programming-language applications based on different interpretations of the necessity modality.


CSF 2020
Securing Asynchronous Exceptions
Carlos Tomé Cortiñas, Marco Vassena and Alejandro Russo
33rd IEEE Computer Security Foundations Symposium

Language-based information-flow 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 MACasync , a concurrent (statically enforced) language for information-flow 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 MACasync satisfy progress-sensitive non-interference and mechanize our formal claims in the Agda proof assistant.

PLAS 2019
Simple Noninterference by Normalization
Carlos Tomé Cortiñas and Nachiappan Valliappan
14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security

Information-flow 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 well-principled and obey useful syntactic properties-hence enabling a simpler proof of noninterference. Since our proof is syntax-directed, 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
Carlos Tomé Cortiñas and Wouter Swierstra
3rd ACM SIGPLAN International Workshop on Type-Driven Development

Many functions over algebraic datatypes can be expressed in terms of a fold. Doing so, however, has one notable drawback: folds are not tail-recursive. As a result, a function defined in terms of a fold may raise a stack overflow when executed. This paper defines a datatype generic, tail-recursive higher-order 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 hand-written tail-recursive function in a single setting.


NWPT 2021
Information-Flow Control and Effects
Carlos Tomé Cortiñas and Fabian Ruch
32nd Nordic Workshop on Programming Theory
TYPES 2021
Semantic Analysis of Normalization by Evaluation for Fitch-Style Modal Lambda Calculi
Nachiappan Valliappan, Fabian Ruch and Carlos Tomé Cortiñas
27th International Conference on Types for Proofs and Programs

Fitch-style 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 Fitch-style 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 possible-worlds semantics for IK. The presented NbE procedure has been formalized in the proof assistant Agda.


MSc. Thesis
Verified Tail-Recursive Folds through Dissection
Carlos Tomé Cortiñas
Master in Computing Science, Utrecht University

The functional programming paradigm advocates a style of programming based on higher-order 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 tail-recursive 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 tail-recursive 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 tail-recursive function and prove that it is both terminating and equivalent to the fold. In addition, using McBride’s dissection, we generalize the tail-recursive function to work on any algebra over any regular datatype.