There is a null tension in the programming languages world between dynamic and static typing.

If you program in a dynamically typed language like Scheme, you might get to run your code faster, but it might trigger dynamic type errors. Conversely, you can program in a statically typed language like Haskell or ML, and you'll spend more time fighting with the compiler to get the code to run, but you'll know that the program

will be free of type errors once it is accepted by the compiler. Now, of course, both disciplines have their relative advantages and disadvantages, which motivated the introduction of this notion of gradual typing. In gradually typed languages, statically typed code can seamlessly interact

with dynamically typed code, and we can rest assured that only the dynamically typed portions can be blamed for type errors. Originally, gradual typing was introduced for a simply typed languages, but the idea has been extended to cover richer typing disciplines,

encompassing features such as subtyping, polymorphism, and maybe even dependent types. Generally speaking, the richer a typing discipline is, the more interesting it is to have a gradual version of it, since it can lower the cost of adopting this language feature. The work that I'm presenting here today

is precisely about extending gradual typing to a language feature that has proven particularly tricky to you statically, which is information flow control, as you might find in languages such as GIF or FlowCaml, for instance. I'll start by covering some basics of information flow control

and explaining how people have tried to combine it with gradual typing. I'll then talk about difficulties that these earlier designs faced and show how we can manage to overcome these issues in this work. I'll briefly talk about GLIO, which is a gradual language that we designed

to demonstrate our solution and conclude with a few design perspectives on gradual typing for IFC. To discuss IFC, it is easier to start with taint tracking, which is a popular feature that you might find in other scripting languages like Ruby or Perl.

In these languages, values come with a taint bit that describes their secrecy, which is propagated on every operation on those values. For instance, if we take this function f and apply it to a secret Boolean, the result of the function is also marked as secret. Later on, we can test the secrecy bit of these results

to, for instance, prevent ourselves from inadvertently sending out secrets into an untrusted network connection, for instance. Now, full IFC is an extension of this idea for dealing with so-called implicit flows,

which are flows of information that happen through the control flow of the program. To see how this works, let us have a look at how this program here execute in several tracking disciplines. Accidentally, what this program does is to leak the input that it's fed into its output,

although admittedly in a somewhat convoluted way. However, if you trace exactly where these outputs are coming from, you will see that they don't come directly from the input of the program, but instead are propagated from constants that appear in the text of the program.

Now, the problem for taint tracking is that these constants are optimistically marked as public, which means that the results of the function are also public. Therefore, the results of the function fail to capture the dependency between them and the secrets

that were fed into the function. The reason why this leak was possible in this case is that there is an implicit flow of information from the secret X to the reference Y when you run this if statement. To prevent the leak, we need the way of tracking this dependency.

And this is what IFC does. By keeping a so-called PC label, which bounds the secrecy of values that influence the control flow of the program at every program point. In dynamic IFC, this PC label is part of the program's state and it's checked on every assignment.

We'll see later that this check leads to an error when we try to assign to Y here, preventing the leak that we saw. In static IFC, on the other hand, the PC label exists only at compile time. And leaks of the one we saw are detected before the program even runs.

Both variants of IFC enforce this property of non-interference, which says that the leakage of the program is limited just to one bit of information. Now, interestingly, it was static IFC that came first in the 90s. But many saw static IFC type systems

as too hard to program in, which has inspired the development of dynamic IFC about a decade later. Dynamic IFC languages have simpler type systems than static ones, but they can lead to runtime errors to prevent leakage,

which has motivated gradual IFC as a compromise between the two disciplines. Everything seemed to be going well in the gradual IFC world until two things happened. First, there was the introduction of the gradual guarantees of Jeremy Seek and collaborators,

which try to provide design guidelines for gradual languages. Now, the gradual guarantees in turn led to Mattias Storow and a few collaborators of his to explore more first principles approach to gradual IFC, relying on this abstracting gradual typing methodology.

In doing so, they revealed an important tension between the gradual guarantees and IFC. And to see what that is, I'm gonna start by clarifying what this gradual guarantee is. One of the aspects of the gradual guarantee is constraining how type annotations interact with the behavior of a program.

For instance, suppose that we have a dynamically typed program F and then we add some type annotations to make it more robust. How should this program behave? The so-called dynamic gradual guarantee says that there are two things that could happen in this scenario.

The first possibility is that the program returns exactly the same result as it did before. The second possibility is that the type annotation cannot be honored during execution. For instance, in this example, maybe one of the calls to F returned a string instead of returning an integer like its type reports.

And in this case, the program should return an error to signal that a type contract has been violated during execution. However, the dynamic gradual guarantee says that it cannot be the case that the program successfully terminates with a different result from what it gave before. Moreover, and this will be important

when discussing gradual IFC, if the unannotated program fails, then the annotated program must also fail. Now that we have a criterion from gradual languages, how do IFC languages fare? All the early designs in the space

violated the dynamic gradual guarantee, even though they managed to satisfy the soundness criterion of non-interference. This prompted Mattias Storro, Eric Tanter, and Ron Garcia to attempt a new design based on abstract and gradual typing. This AGT methodology allows you to derive gradual languages

from statically typed languages in a semi-automated way. And one of its interesting features is that it provides the dynamic gradual guarantee by construction. Toru and the others used AGT to define GSLRef,

which is a gradual IFC language with general references. And unfortunately, while this design did manage to satisfy the dynamic gradual guarantee by fiat, it ended up violating the soundness property of non-interference. The fix found by the authors was to tweak this initial design with a dynamic check for enforcing non-interference,

which unfortunately ended up breaking the dynamic gradual guarantee for reasons that we'll see in a second. Now this led the authors to speculate that perhaps there was something inherently incompatible between the two properties. But what we found in this work is that

this is not the case. Our GLIO language, which I'll present to you in a bit, does satisfy both non-interference and the dynamic gradual guarantee. The issue with the early designs was actually that they let the static secrecy annotations interfere with assignment checks used to prevent leakage.

To understand how this happened, let us revisit the previous example and review how dynamic IFC manages to enforce non-interference. Here we see the PC label state component, which tracks the secrecy of values

that have influenced control flow. It's initially set to public. Now suppose that we run this program on a secret Boolean X. This Boolean B here in the program is defined as public since it's set to a constant. Hence the references Y and Z, which are initialized with B,

are also marked as public. And then we reach this if statement. We branch on X, which causes the PC label to be bumped to secret. Now when we assign to Y, we trigger a so-called no sensitive upgrades check, which tries to ensure that the PC label

is less restricted than the label of the reference. The check fails here, signaling a potential leak, and the program terminates with an error. Now let us consider how this program would run in a gradual language. The language might let us to statically annotate

the secrecy of some values of this program, like B for instance. Now how should these annotations affect execution? Well, these earlier designs interpreted the annotations type level classification, which means that the label attached to B during execution

is also set to secret. This causes the labels of the reference to change and does the assignment check on Y to succeed, leading to the program successfully returning a result. This means that the dynamic gradual guarantee failed. We went from an annotated program that threw an error

to an annotated program that successfully terminates, which is precisely the opposite of what the dynamic gradual guarantee allows. Our solution to this issue is simple. You add label checks to honor static annotations, but you do not let them modify the label itself.

Let's see how this would work in our example program. The constant true is still labeled as public, but it needs to be assigned to a secret variable B here. To ensure that this is safe, we simply check that the label on the assigned value,

which is just public, is less restrictive than the label on B. Here the check succeeds, which allows execution to proceed normally. And what is important here is that the references that we allocate are now again labeled as public so that the assignment check that we perform on Y

now fails, causing the program to halt. Therefore, adding the type annotation did not remove the error, which means that the dynamic gradual guarantee was not violated. Now this solution can be readily adapted to previous gradual IFC languages,

but we decided to incorporate it in a novel language design called GLIO, which we think fits better with this style of enforcement. GLIO is an extension of LIO, which is a Haskell library for information flow control. There's been prior work in extending LIO

with gradual checks, which led to another Haskell library called HLIO. GLIO can be seen as an alternative bridge between LIO and SLIO, which is the fully statically typed fragment of this earlier HLIO system. To give you a taste of GLIO,

let us start with some typing rules. These rules that I'm showing here show how to check operations on references in the original LIO. As far as LIO goes, there are two interesting features here. First of all, LIO uses a monad to encapsulate IFC computations.

Second, to allocate a reference in LIO, we have to provide a term-level secrecy label. These labels in LIO are first-class citizens that can be created dynamically, passed to functions and so on, which allows us to determine a secrecy policy for a value based on runtime information, for instance.

In GLIO, these typing rules are refined with optional static label arguments. The annotations on the LIO monad, for instance, are bounds on the initial and final PC labels. And the annotations on reference types

describe the secrecy of the contents of these references. The labels and checks that appear in these rules reflect how these labels are manipulated at runtime. For instance, when we create and modify references, we use a type level analog of the NSU check

that we saw earlier. The rule for reading references shows another difference of LIO with respect to more traditional information flow control. LIO has a so-called coarse grain design where only some values carry labels.

The contents of references are protected by the label of the reference. But once we read the reference, the contents are only protected by the PC label. This is why the reference label is propagated to the final PC label in the GET rule, for instance. And finally, GLIO employs a notion of consistent subtyping

to allow annotated and unannotated code to interact. This relation allows us, for instance, to use a reference with unknown secrecy in a context that expects a reference with secret contents, statically speaking.

And at runtime, the program performs a check to ensure that the label of the left-hand side is compatible with the secrecy value of the right-hand side. For instance, that it's exactly secret, but not top secret or something more restrictive. Importantly, the cats induced by subtyping

never modify the labels, which is why GLIO manages to enforce the dynamic gradual guarantee. We have managed to prove both non-interference and the dynamic gradual guarantee for GLIO. And both of these results are formulated in a typical logical relation style.

For non-interference, for instance, the logical relation at function types guarantees that a program does not reveal secrets of public observability. Now, as usual, a challenge in proving these results is defining the logical relations because they have a circularity introduced

by higher order storage. We solved this issue by giving denotational semantics to our language and by reusing the framework of relational structures of Andy Pitz to define these relations. I'd like to end my talk with a few design perspectives.

GLIO supports a workflow where you start with some LIO program, incrementally add and static label annotations, and eventually you might end up with a fully annotated program in SLIO that is free of dynamic type and secrecy errors. The dynamic gradual guarantee that we proved

shows that this process is well behaved. The program does not change its behavior arbitrarily once you go from one side to the other. Unfortunately, most programs that we could benefit from information flow control are not written in LIO.

And to port them to GLIO, we first need to add in dynamic label annotations, for instance, when we're allocating references in the program. Now, this might be a little bit disappointing. Our reviewer, when we submitted this work to POPL last year, asked us, for instance, if there were any guarantees that we could provide for this migration process.

Since it's probably this migration process, it's the one that matters in practice. Unfortunately, there seems to be a fundamental obstacle to provide a full dynamic gradual guarantee for this entire process because of label introspection.

Suppose, for instance, that you have a program that allocates a new reference, but leaves its dynamic label unspecified. After allocating, the program checks if the label on the reference is exactly S. Now, imagine what should happen

if we add in a dynamic label annotation to this program, obtaining one of the programs on the right. If we want to obtain an analog of the dynamic gradual guarantee, these programs cannot do much. If this label of primitive, for instance, behaves like we might expect, then the two programs on the right will produce different results,

so there's no consistent outcome that is possible for the unannotated program. Similar issues have been observed for type introspection, and unfortunately, it's hard to have a practical IFC system that gives up on label introspection, meaning there are limits to how well-behaved this migration process can be.

On the other hand, this suggests that we can mitigate the issues with label annotations in GLIO by minimizing the need for them. I mentioned that LIO is a coarse-grained system where most values do not need label annotations. However, these label annotations

need to be provided explicitly by the programmer. Oh, and by the way, it might seem that coarse-grained systems like LIO are less expressive than more traditional fine-grained ones that we're seeing earlier, but it turns out that the two styles are equally powerful in terms of secrecy policies that you can express.

Now, if choosing labels explicitly leads to those migration problems, what if we let the language automatically choose labels for us? For instance, we could set the label for reference to be the same as the PC label at the moment of allocation, which might be a little bit unusual for IFC languages,

but I have the impression that it actually is a more faithful representation of how IFC operating systems work, for instance. So this concludes my talk. We've seen that, unlike what other people have suspected before us, the dynamic gradual guarantee can actually coexist with non-interference.

Could it also hint at better approaches for enforcing information flow control? Thank you.