3 ms·
After proving the full functional correctness (that machine code implements spec), they did additional security proofs against the spec, including confidentiali
by sanxiyn 8y ago
After proving the full functional correctness (that machine code implements spec), they did additional security proofs against the spec, including confidentiality and integrity. If you accept their TCB(no hardware bugs etc), the entire proof is incredibly strong.