2010 IEEE Symposium on Security and Privacy Proceedings issue:2010 pages:109-124
IEEE Symposium on Security and Privacy 2010 edition:31 location:Oakland, California, US date:16-19 May 2010
A program is defined to be non-interferent if its outputs cannot be
influenced by inputs at a higher security level than their own.
Various researchers have demonstrated how this property (or closely
related properties) can be achieved through information flow analysis,
using either a static analysis (with a type system or otherwise), or
using a dynamic monitoring system.
We propose an alternative approach, based on a technique we call
secure multi-execution. The main idea is to execute a program
multiple times, once for each security level, using special rules for
I/O operations. Outputs are only produced in the execution linked to
their security level. Inputs are replaced by default inputs except in
executions linked to their security level or higher. Input side
effects are supported by making higher-security-level executions reuse
inputs obtained in lower-security-level threads.
We show that this approach is interesting from both a theoretical
and practical viewpoint. Theoretically, we prove for a simple
deterministic language with I/O operations, that this approach
guarantees complete soundness (even for the timing and termination
covert channels), as well as good precision (identical I/O for
terminating runs of termination-sensitively non-interferent
On the practical side, we present an experiment implementing secure
exploiting parallelism on a current multi-core computer. Benchmark
results of execution time and memory for the Google Chrome v8
Benchmark suite show that the approach is practical for a mainstream
browser setting. Certain programs are even executed faster under
secure multi-execution than under the standard execution.
We discuss challenges and propose possible solutions for
implementing the technique in a real browser, in particular handling
the DOM tree and browser callback functions. Finally, we discuss how
secure multi-execution can be extended to handle language features
like exceptions, concurrency or non-determinism.