Modal logic is a fascinating field which has been applied to computer science in all sorts of weird ways. In this post I'll talk about an interpretation of modal logic that I've been exploring which gives type-theoretic interpretations to crashing and security.
This post assumes a familiarity with logic, and a very vague familiarity with monads, comonads, and the Curry-Howard correspondance. Also, I need to say from the start that this post is not very rigorous; it's meant as interesting food for thought and intuition.
Modal logic is a version of logic that has two new and fascinating operators, Possibly and Necessarily. These operators work exactly as you'd expect, but it's hard to say exactly what it is that we expect, so I'll simplify the idea. Consider the python program below:
# this is equivalent to print(input() + 4)
# but the variables make it easier to talk about
x = input()
y = 2 + 2 # always evaluates to 4
z = y + x # depends on user input
print(z)
When a program is run, it has some set of inputs that change how the program progresses to completion. In this case, it's the value assigned to x. For a given run of the program, it only has one concrete input, and only unfolds in one way. If you enter 3, the program calculates and prints 7. But there are other ways it could have gone, if the original input were different. It wouldn't have printed 7 if the input were, say, 5. And there are some parts of each run of the program that are the same no matter what the inputs are, like the value of y. Framed in modal logic, we'll say that z is possibly 7, and y is necessarily 4. That's the understanding of possibility and necessity we'll use for this post. A vocabulary for talking about different runs of a given program. Regular propositions are for the "current run," necessary ones are true in all runs, and possible ones are true in some runs, which could be the current one but might not be.
In logic, "\(P\) is possible" is written \(\Diamond P\) and "\(P\) is necessary" is written \(\Box P\).
First of all, it's worth taking a moment to appreciate the beauty of modal logic. Possibility and necessity are dual in the same way conjunction and disjunction are, or universal and existential quantification are. That is, take some proposition \(P\). \(\neg (\Diamond (\neg P))\), or "it is not possible that \(P\) is false," is equivalent to \(\Box P\), or "\(P\) is necessary." \(\neg (\Box (\neg P))\), or "it is not necessary that \(P\) is false," is equivalent to \(\Diamond P\), or "\(P\) is possible." That is, negating the inputs and outputs of one gets you the other, just like conjunction/disjunction and just like existential/universal quantification.
They're also dual in a sort of category-theory way: possibility is a monad and necessity is a comonad. Showing why is a nice demonstration of the modalities, so here it is: for any proposition \(P\),
You can see in these rules the monadic "return" and "join" operations and comonadic "extract" and "duplicate" operations. It's also worth going through them and intuitively checking if they make sense.
If you're familiar with language-based security theory, you might immediately see a use for this. LBS is largely built around a concept called noninterference), the property that secret inputs don't interfere with less-secret outputs. It's a hyperproperty, meaning that it's talking about all possible runs of the program instead of just a few particular ones. Sound familiar? In our modal vocabulary we might say that public outputs are necessary with respect to secret inputs; they aren't affected in any run of the program by those inputs.
This is a little bit different from how LBS is usually studied. To oversimplify, there's usually a Secret monad that ensures the values it holds can only affect other Secret values. In the modal language, however, we're talking about a Public comonad that makes sure the held value only depends on Public values. This flipping of perspective has been studied a bit, most notably by Choudhury. He takes inspiration from a system by Davies (that is explicitly inspired by necessity in modal logic) that is used to determine which expressions in a language don't depend on user input, and can therefore be evaluated at compiletime as an optimization. This is like noticing that y is necessarily 4 in the python code above, and removing the addition. Choudhury extends this idea for language-based security, combining it with the Secret monad I just mentioned.
Consider for a moment what it is that an assert statement does in a program. Hopefully it does nothing! It has some proposition that it expects to be true in the current run of the program, and it crashes if it doesn't. We can describe this naturally in our modal vocabulary: it takes a proposition that's possibly true (true in some runs of the program) and "proves" that it's true in the current run by crashing if it's not: \(\Diamond P\implies P\). This is a weird sort of implication because it's not generally true: not all things that are possibly true are actually true. It's like an "extract" operation for monads: it doesn't generally exist. (Side note: Rust's unwrap operation for the Result monad comes to mind.) Therefore it's an implication that you don't want to be applying unless you really think it's true for the proposition in question.
We talked a lot about duality in this post so far, so just for some informal fun, what would the dual of an assertion be? If an assertion is an implication \(\Diamond P\implies P\) then its dual would be an implication \(P\implies\Box P\), which also doesn't exist in general. What does it mean? If \(P\) is true in this run then it's true in every other run. This is obviously not true in general but we can imagine that it works like assertions, simply crashing the program when it's false.
This is a weird operation: take some fact about the current run of the program, and crash the program if it's not true in every other run of the program. Is there anything like this in computer science? There actually is, surprisingly enough, and big corporations like Amazon are using it to make a ton of money. It's called dynamic taint tracking. The idea is you "taint" certain inputs at runtime which may give sensitive information, then you taint every value that is derived from the inputs, then if a tainted value is about to be printed in a public way, the program crashes. This can easily be seen in terms of the Public comonad I mentioned earlier: dynamic taint tracking takes a value and coerces it to be Public, and thus publicly viewable, crashing if the value depends on sensitive information. That is, the program crashes if the value isn't necessary with respect to the secret inputs.
That's all I have to say about this stuff for now but I hope to keep exploring modal logic as a language for security and crashing. I care a lot about crashing because I like the crash-only software philosophy a lot, and microreboot architectures, but I'm a type theorist and logician primarily. I have a crash-based project I'm working on that I'll hopefully post about soon. Also, if you're interested in how comonads are useful I've got to link this. I hope this was interesting!
© 2024 Ryan Brewer.