Avik's talk on Dynamic Labels and Static Types for Protection in an Operating System
Luca de Alfaro
Avik Chaudhuri
E2, Rm 399, Tue May 1, 2:15pm
Label-based protection mechanisms aim to prevent undesirable flows
across labeled protection boundaries. Such mechanisms and their
security properties are the subject of much active research. Despite
their conceptual simplicity and intuitive appeal, however, these
mechanisms seldom find their way into commercial systems, partly
because their security properties often require conditions that are
difficult to meet in practice. We study protection provided by a
commercial operating system by combining such runtime mechanisms with
static discipline. The runtime mechanisms complement conventional
mandatory access controls with some non-standard features for
flexibility in practice; these features open the door for
vulnerabilities that are eliminated by static discipline.
Specifically, we design a calculus that can express dynamic creation
and relabeling of threads and locations, packing and execution of
binaries, and other usual operating system constructs. We then design
a type system for this calculus that guarantees protection of trusted
code from arbitrary untrusted environments. The calculus and type
system closely follow the label-based protection mechanisms and so-
called best programming practices in the Microsoft Windows Vista
operating system.