An architecture for provably secure computation

We describe an architecture requiring very few changes to any standard von Neumann machine that provably withstands coalitions between a malicious operating system and other users, in the sense that: 1. If the operating system permits a program to run, then the program produces the same outputs as it would produce if it were running on an ideal, single-user machine; moreover, even if the operating system behaves according to expectations only most of the time, the programs get, executed. 2. The only information leaked by a program to the malicious coalition is the time and space requirements of the program. 3. If the malicious operating system is dynamically replaced by a good operating system, then the latter can quickly and correctly determine what memory resources are available for future programs, as well as how much time is left for each of the currently executing programs, and can distribute these resources without any restrictions. This can be accomplished without restarting currently executing programs. To our knowledge, ours is the first attempt to provide provable guarantees along these lines, and the first treatment of any kind, provable or otherwise, for the third property.