-
Notifications
You must be signed in to change notification settings - Fork 32
A Quick Introduction to Jeeves
The Jeeves language is embedded in Python, which means that we have developed Jeeves as a Python library. We've done this by creating special objects corresponding to faceted values and overloading Python operators to handle computations on these objects. Since Python doesn't allow overloading of everything, we have implemented an @jeeves macro that rewrites classes and functions to use the appropriate Jeeves library functions.
For further reference, check out the Jeeves API documentation.
To access functions to create labels, sensitive values, and policies, you must import the Jeeves library.
import JeevesLib
Jeeves has its own functions to handle assignments, conditionals, and more. To help the programmer write code that looks like Python code but uses the Jeeves semantics, we have a the @jeeves macro.
from sourcetrans.macro_module import macros, jeeves
The Jeeves source transformation uses the MacroPy module, which requires the module macropy.activate to be imported before any other modules. A way to do ensure this happens at the beginning is to add import macropy.activate to the beginning of your __init__.py file and then import X for all modules X that use the @jeeves macro.
The Jeeves libraries manages different views of sensitive values and is responsible for producing appropriate values for the results. In Jeeves terms, a faceted value is a sensitive value containing two views, a high-confidentiality and a low-confidentiality view. Faceted values are guarded by labels, which are either high or low and determine which facet flows to the viewer. Programmer-specified policies determine the label values; these policies are functions that describe whether a viewer has access. Computations on faceted values produce new faceted values, so all computations interacting with outside world (such as print) need to concretize values. Concretization occurs with respect to a specific viewer and uses the policies to assign label values in order to project out a result adhering to the policies. The Jeeves library has functionality for creating labels, creating faceted values, associating labels with policies, and concretizing faceted values.
We call mkLabel to make a label and restrict to make a policy:
x = JeevesLib.mkLabel()
JeevesLib.restrict(x, lambda _: False)
The restrict function takes the label x and a function that takes an output channel and returns whether x may be high with respect to that output channel. The call to restrict above returns False no matter the output channel. No matter what output channel argument we supply when we we call the library's concretize function, we will get that x is low (False):
assertFalse(JeevesLib.concretize(x, None))
We can make sensitive values with these labels:
xS = JeevesLib.mkSensitive(x, 42, 0)
Here, xS is a sensitive value guarded by label x where 42 is the high-confidentiality facet and 0 is the low-confidentiality facet. Because, as we showed, x is always low, xS always concretizes to 0.
We can write a less trivial policy as follows:
x = JeevesLib.mkLabel()
JeevesLib.restrict(x, lambda y: y == 2)
value = JeevesLib.mkSensitive(x, 42, 41)
The policy says that if the output channel is equal to 2, then the label x may be high. Thus the concretization of value will only be 42 if the output channel argument is 2:
assertEquals(JeevesLib.concretize(1, value), 41)
assertEquals(JeevesLib.concretize(2, value), 42)
assertEquals(JeevesLib.concretize(3, value), 41)
Contexts may also depend on sensitive values. Consider what happens in the following code:
x = JeevesLib.mkLabel()
JeevesLib.restrict(x, lambda ctxt : ctxt == 42)
value = JeevesLib.mkSensitive(x, 42, 20)
self.assertEquals(JeevesLib.concretize(value, value), 42)
In this code, we create a label and store it in x. We attach a policy to x that the context must be equal to 42. We then create a sensitive value that x is either equal to 42 or 20, depending on the value of x.
Something interesting happens when we use value as the context for viewing value. We create a circular dependency between value and the policy on label x. As a result, the policy allows multiple outcomes: either x is low and value is 20 or x is high and value is 42. In these cases, the Jeeves runtime allows the label to be high, and thus JeevesLib.concretize(value, value) yields 42.
The @jeeves macro rewrites functions to use the Jeeves versions of conditionals, assignments, and function calls.
You may look at our gallery to see how we use Jeeves for larger programs. The @jeeves macro also works for classes.