Doi: 10.1145/2018396.2018418
technical Perspective
making untrusted code useful
By Butler Lampson
the foLLoWinG PAPer combines two
important themes in secure computing: assurance and information flow
control. Assurance is evidence that a
computer system is secure, that is,
obeys its security specification, usually called a security policy. A system’s
Trusted Computing Base (TCB) is all
the parts that must work for the system
to be secure. For high assurance, the
TCB needs to be small and the policy
simple. Flow control is one such policy;
it specifies how information is allowed
to move around in a system.
In the late 1960s the military began
to worry about a “multilevel” computer
system in which secrets leak from a
user process handling classified data.
It is impractical to require every application program to come from a trusted
source; databases, math libraries, and
many other essential tools are too big
and complicated to rebuild, or even
to audit. So the secret process might
contain a Trojan horse from the KGB,
which leaks the secrets to Moscow via
another, unclassified process.
Flow control solves this problem by
requiring that no action of a secret process can affect the state of an unclassified one. Formally, it models the system
as a state machine; the state is a set of
variables (including process state such
as the program counter), and every step
sets some variables to functions of others. So each step has the form
var1, … varn: = f1(args1), … , fn(argsn)
The only flows are from argsi to vari.
Each variable v has a label L(v). La-
bels form a lattice, a partial order in
which any two elements have a least
upper bound or max. The flow rule is
that information can only flow from
weaker (unclassified) labels to stronger
(secret) ones, so each step must satisfy
The flow rule is good because it
composes: if each step obeys the rule,
the whole computation does so. Hence
the label on every data item is at least
the max of the labels on everything that
affected it; the rule is end to end. It is
certainly simple, and assurance is just
evidence that each step obeys it.
maxv∈argsi L(v) L(vari)
security depends on
the simple flow control
policy and a small tcB.
References
1. Kaashoek, F. et al. application performance and
flexibility on exokernel systems. ACM Operating
Systems Review 31, 5, (dec. 1997), 52–65.
2. myers, a. and liskov, b. Protecting privacy using the
decentralized label model. Trans. Comput. Syst. 9, 4
(oct. 2000), 410–442.
3. Porter, d. et al. rethinking the library os from the
top down. ACM SIGPLAN Notices 46, 3 (mar. 2011),
291–304.
Typically a label is a set of atomic elements called categories, the ordering is
set inclusion, and max is set union.
Butler Lampson ( butler.lampson@microsoft.com) is a
technical Fellow at microsoft research and is a Fellow
of aCm.
