provable security and sandboxes

Question

Maybe this can be answered by an answer to a more general question, such as what programs can be proven secure.

Can it be (or has it been) formally proven that a sandbox is secure?

Answer 1

The term "sandbox" is wide, generic, and often misused and misunderstood.

Let's consider a type of sandbox, a virtual machine running under control of an hypervisor. The guest system is nominally isolated and cannot "see" the host system. However, this is relative to the implementation of the hypervisor, which is a combination of software and hardware, both of which being susceptible to bugs (hardware is always involved in that the whole thing, ultimately, runs on a CPU; I am not speaking about using or not using the AMD-V/Intel-VT opcodes). Escapes from hypervisors have happened. "Proving" the hypervisor to be correct would mean proving that it is bug-free. Proving that software is free of bugs has been a rather elusive goal for the last half century... and for hardware, even more so.

Moreover, sandboxes do not equate to safety. For a sandbox to be useful, it must have a few open doors: you run some software in the sandbox, but you will want to see the result, be it something displayed, files saved somewhere, or some network activity. When people use a Web browser in a sandbox, they want the browser to, say, actually browse the Web, so external network connections from the sandbox must be allowed; and the sandboxed browser must also have the possibility to display things, so it has an access to the graphic hardware (possibly a controlled access, but if you want 3D acceleration, strict controls become difficult). You want a sandbox because you suspect that the browser could be subverted and hijacked by an attacker. But, at that point, you have already lost (not the whole war, but significant battles nonetheless): the subverted browser, sandbox or not, is network-able and can be used as relay to attack other sites or send spam, seemingly originating from your address.

In more succint words, amputation is not the ultimately advisable type of medicine.

Let's see another kind of sandbox, the Java Virtual Machine and its support for applets. It has two main facets:

• The "code" is not raw binary code for the local CPU, but "bytecode": opcodes for a conceptual, abstract machine, which lives in a non-hardware world where generic pointer arithmetics are not allowed. References have unescapable types, and array accesses are bounds-checked.

• The external access facilities for the applet code are restricted: network connections can be made only to the originating server; local files cannot be read or written to; and so on.

When the bytecode must be run, it is first analyzed: the JVM implementation does a control flow analysis which formally proves (yes, in the sense of "provable security") that the code complies to the type rules for bytecode (namely, that it never calls a method on an object which does not feature that method). This allows for translation to efficient native code, without needing specialized virtualization hardware. Moreover, it protects against many types of subversion (buffer overflows are reliably detected, there is no dangling pointer or double-free because of GC-based memory management...). This kind of protection is not sufficient for "security" because you still want the access controls (e.g. blocking external connections except to the originating server) which are enforced by the system classes. The bytecode analysis is there to ensure that only the system classes are used, and are used correctly; the rest is up to the system classes.

Of course, over the history of Java, both the bytecode analyzer and system classes implementations have been found to have flaws. They are not intrinsic: what they try to achieve is not mathematically impossible. But, let's face it: bugs happen. The JVM is a rather complex piece of software which is far from being proven to be bug free. Also, the JVM runs within an operating system and on some tangible hardware, neither of which being bug-free either.

This illustrates my points:

• A sandbox provides "provable security" only insofar as its implementation has no bugs. That's somewhat utopic.
• What the sandbox actually provides is enforcement of a set of rules which may or, more often, may not, embody what you really mean by "security". As usual, the first step of proper security is to define clearly what you want.

Answer 2

Assume that you have proven that your sandbox is immune to all attacks. If this proof where made about 10 years ago it would have not taken into consideration dangling pointer and padding oracle attacks because these methods of exploitation where unknown at the time. Therefor you could not have proven that this sandbox was totally secure, as that would be a contradiction -><-

Answer 3

Your question seems to indicate a misunderstanding of what security is. Proven security is an oxymoron. Nothing can ever be completely secure, or as the old IT security joke goes, the only provably secure storage is writing to dev/null (ie, destruction). Security is simply a game of resources and costs. It tries to balance the need of legitimate users getting at information while preventing attackers from doing the same, but with any allowable access, given sufficient resources and time, it will always be possible or at least feasible to break the system and gain access.

Self destructive systems are an attempt to avoid this problem by limiting the amount of access that can be done, but inventive means can circumvent most of these as well given significant enough resources and effort (sometimes down to the level of actually dissolving layers of chips, layer by layer).

The question really needs more clarification to be answerable. Do you perhaps mean, can protection against a particular type of attack be proven? If so, what kinds of attacks are you worried about?

Answer 4

It depends what kind of provable security you talk abot (for either for its impossible and nonsense). But in security algorithms provable security means that in order to break your algorithm someone needs to break underlaying crypto. Thus if we think of our crypto-alg as secure one, and you write a proof that only by breaking the crypto you will be able to break your algorithm then it does not mean anything, it's just something that can be researched and published nothing more. And I agree with Rook attack patterns are evolving something proof for now will not be secure within a decade or so.