This is probably only *theoretically* possible with quantum computation, but it's *practically* possible with tamperproof hardware: TCMs used for good instead of evil, maybe?
On Mon, Jul 28, 2014 at 06:05:47PM +0200, Lodewijk andré de la porte wrote:
> <3
>> If you're a secure kernel developer, Onion routing expert, fantastic CI would be very interested in contract work for running Linux on L4 microkernels.
> coder or technology investor, and this triggered your interests, please
> contact me!
You can see my experience here https://lkml.org/lkml/1999/3/7/59
But if you give me the code, and I can emulate the hardware with qemu,
I can extract keys/code/whatever from anything running inside the 'secure'
microkernel.
If you want the 'tamper evident' hardware it must be open-source hardware
and you will need on the order of at least a million USD to fabricate the
silicon,
and then another million to offer cash prizes at DEFCON for anyone
that can hack the silicon & microkernel.
So if you can secure 2 to 10 million, let's get it done.
Otherwise talking about the theory of a formal-methods 'microkernel' running
on today's buggy broken pre-trojaned hardware is unethical and dangerous.
Do you know what your network card firmware is doing? Neither do I, but I bet
the NSA and Chinese intelligence will have updates for you when the 'secure'
kernel comes out.