As a full disclaimer, the vast majority of work for these labs was done by the professor for 15-316 Software Foundations of Security and Privacy, Matt Fredrikson. As a TA, I helped a little bit with coming up with the ideas for the labs and also a little with basic file/object structure and autograders.

So, while I can’t really even claim 20% credit for these, I’m still really proud that I had any part in them that all and think they are super neat labs to work through. Also, they’re open source so you can follow along at home too!

Lab 1: Analyzing Safety

This lab is all about instrumenting code and then proving properties about the original code through the instrumented version. You may be wondering what any of these words mean so let’s go through an example.

Tinyscript

Here is some code:

x := i;
while x < (i-i)-1 do
    x := x + 1
done

You may notice that the syntax is similar to, but not exactly the same as, any language you’ve ever seen¹. This is because it is a language you have never seen. For simplicity, this course uses a fairly small language we call Tinyscript with simple and intuitive and easy-to-specify semantics. Full syntax tree and interpreter can be found in the repository.

Safety Properties

Anyways back to safety: a safety property is class² of traces that can be defined by excluding all failing traces³ with just a finite prefix. That is, as soon as you see “something unsafe”, you know the safety property has been violated.

Unfortunately, you can’t neatly divide programs into “satisfies a safety property” and “doesn’t satisfy a safety property” since that would require solving the halting problem⁴. Plus, with our arbitrary-precision variables, you can’t brute-force every input combination to see if the safety property is violated (or the program doesn’t halt in a reasonable amount of time). So, what can you do?

Dynamic Logic

There is a formula called a box modality, which we denote as $[\alpha]P$ where $\alpha$ is a program, and $P$ is a boolean predicate, which is itself a predicate saying “for all runs of $\alpha$, $P$ will hold in the terminating state”.

Turns out, there are rules on how to simplify this when given a specific $\alpha$ and $P$! I’ll spare you most of the details (take the class or read the code to see how it’s done), but I should note one, which is the rule for loops:

$[\texttt{while}(Q)\ \texttt{do}\ \alpha\ \texttt{done}]P \leftrightarrow [\texttt{if}(Q)\ \texttt{then}\ \alpha\ \texttt{else}\ \texttt{pass}\ \texttt{endif};\texttt{while}(Q)\ \texttt{do}\ \alpha\ \texttt{done}]P$

yeah um there’s a bit of infinite recursion here. One way to handle this is by giving up and pursuing a different area of computer science, since this is again equivalent to the halting problem. Another way is to unroll the loop for “enough iterations” and call it a day. We take the latter approach.

With all these rules to turn box modalities into regular formulae, we can just plug that resulting formula into Z3 and bask in the glory of modern computation. Hooray for automated theorem provers!

Program Instrumentation

So now we have a tool to help us reason about a condition at the end of a program, but safety properties can be violated at any time in our program. How can we reconcile this? Simple: we rewrite the program so that any operation that could violate the property sets a marker that cannot be changed afterwards.

Here is how we would do that for the previously-shown program, for the safety property x > 0:

#violated := 0;
x := i;
if !(x > 0) then #violated := 1 else pass endif;
while x < (i-i)-1 do
    x := x + 1;
    if !(x > 0) then #violated := 1 else pass endif
done

We’ve instrumented every assignment to x with a check afterwards to make sure that it’s value doesn’t dip below zero.

By the magic of “it’s really easy to recur over syntax trees”, doing this instrumentation automatically is fairly simple if you’re clever. With this method, proving the safety property becomes equivalent to proving $[f(\alpha)](\texttt{\#violated} = 0)$ (where $f$ is the instrumentation function), which we have the tools for!

All the problems in the lab (bounded execution, no unused variables, taint analysis w/o implicit flows) are meant to be solved using this strategy. If you have some time and are curious about this, definitely check it out! It’s free online and the writeup there is much better than what I could explain here.