***ng0_ is now known as ng0
***ChanServ sets mode: +o rekado
<rain1>new complier correctness paper <true-grue>rain1, They've updated it? I think that I've seen the older version this paper before. <true-grue>I like that they spent time to put their work in historical context, really interesting references. <xentrac>I recently downloaded the seL4 binary verification paper, but I haven't read it yet <xentrac>they claim that it extends their proofs of correctness of seL4's source code to the binaries they are using <xentrac>although not all optimization settings on the compilers they are using produce verifiable binaries <xentrac>in theory this eliminates the compiler from the set of things their proof's validity depends on <xentrac>sadly this doesn't tell you that anything you're *running* on the kernel isn't backdoored <xentrac>but the same approach could be applied <rain1>> knowing that a theorem has been proved does not help understand how the theorem statement relates to reality. <rain1>that's an interesting point to address