CSCI 1730 · Fall 2026
3 IFC Design
3.1 What is This Assignment’s Purpose?
An information-flow language enforces whatever policy it is given. It stops flows forbidden by the policy and permits one allowed by it. The language itsef doesn’t not take any positions on these data; they are all determined by the policy. (This is just like type-checking, where the checker has no opinions; it just enforces whatever types you declared.) Thus, policy authoring requires care, and this assignment gets you to start working on that.
3.2 Terminology
Information flow control policies can be expressed at different levels of abstraction. They can refer to a particular person or particular datum;While it is conventional to speak of “people”, entities can also be inanimate. For instance, a policy may refer to computer programs. or they can refer to groups of people (roles) or groups of data. A label names a kind of data, and the labels must be arranged in a lattice: label A below label B means that data at A may be used in a document at B. Read another way, it says that whoever may read B may read A. Every role gets a clearance, which is one label; the role may read everything at or below it. Several roles may share a clearance, and there may be nobody with a particular clearance label.
When a document is assembled from data at two labels, it gets the permissions of the least label above both, which is referred to as their join. If the two labels are comparable, that is just the higher one. If they are not, the lattice has to contain a label that is above both and below every other label above both, and whoever is cleared at that label may read the document. A document built from two kinds of data therefore has a label you may not have chosen, and readers you may not have had in mind.
3.3 The Sample Domain
You are the security engineer for a small company that sells a hosted software product to other businesses. It has five roles: Support, who answer customers’ tickets; Engineering, who build the product; Sales, who negotiate contracts, each at its own price; HR, who set salaries; and the Executives, who make decisions about business and about employees. Follow these definitions even if you have worked somewhere organized differently.
There are four kinds of data besides what is on the public web site: tickets (what a customer wrote, with the screenshots of their own data that they attached), the source code, contracts, and salaries. The table below lays out what the company requires. M means the role must be able to read that kind of data; X means it must not; a blank cell is not decided.
| Public |
| Tickets |
| Source code |
| Contracts |
| Salaries | |
Support |
| M |
| M |
| X |
|
| X | |
Engineering |
| M |
|
| M |
| X |
| X | |
Sales |
| M |
|
| X |
| M |
| X | |
HR |
| M |
| X |
| X |
|
| M | |
Executives |
| M |
|
|
| M |
| M |
Two documents are built from two kinds of data each, and the company has requirements for them too:
An account review: one customer’s contract, with their ticket history. Sales and the Executives must be able to read it; Engineering must not.
A commission report: each salesperson’s commission, computed from the contracts they closed and their salary. HR and the Executives must be able to read it; Sales must not.
3.4 Assignment
Design a lattice, and give each role a clearance within it, such that they meet every requirement above.
The blank cells are left to you to make decisions about. You need not fill every one; fill the ones you think matter, with an M or an X, and justify each one you fill. The tricky part of doing this is the following. You might think you are granting or blocking a permission for one thing, but you may have inadvertently affected some other entity as well. The challenge of policy design is thinking through all the consequences of your decisions.
For each of the two composite documents, say which label it gets in your lattice and who can read it there. If the first lattice you draw gives one of them readers the requirements forbid, or denies it readers they require, you have a choice to make: add a label, move a clearance, or argue that the document should really be two documents at two labels. Say which you did and why.
digraph { rankdir=BT; Public -> Tickets; Public -> Code; Tickets -> Account; } |
3.5 What To Hand In
Assemble a single document with carefully marked sections (labeled separator pages can sometimes help). It must contain: The lattice, the clearances, the table with the cells you filled marked, the labels of the two composite documents, and your justifications. Make sure you write this in Google Docs.