Speaking as somebody who works in computer systems research:
I agree with Pentashagon’s impression: we could engineer a compiler and operating system with proof-carrying code tomorrow, without needing any major research breakthroughs. Things very similar to proof-carrying code are in routine deployment. (In particular, Java bytecode comes with proofs of type safety that are checked at load time and researchers have built statically-verified kernels and compilers.)
I believe the real barrier at this point is that any sort of verification effort has to go bottom-up, and that means building new libraries, operating systems, etc ad nausiam before anything else runs. And that’s just a huge expense and means losing a lot of legacy code.
My impression is that it’s not a performance problem. In the schemes I’ve seen, PCC is checked at load or link time, not at run-time, so I wouldn’t expect a big performance hit.
Separately, I’m not sure PCC gets you quite as much security as you might need. Users make mistakes—grant too many permissions, put their password where they shouldn’t, etc. That’s not a problem you can solve with PCC.
Speaking as somebody who works in computer systems research:
I agree with Pentashagon’s impression: we could engineer a compiler and operating system with proof-carrying code tomorrow, without needing any major research breakthroughs. Things very similar to proof-carrying code are in routine deployment. (In particular, Java bytecode comes with proofs of type safety that are checked at load time and researchers have built statically-verified kernels and compilers.)
I believe the real barrier at this point is that any sort of verification effort has to go bottom-up, and that means building new libraries, operating systems, etc ad nausiam before anything else runs. And that’s just a huge expense and means losing a lot of legacy code.
My impression is that it’s not a performance problem. In the schemes I’ve seen, PCC is checked at load or link time, not at run-time, so I wouldn’t expect a big performance hit.
Separately, I’m not sure PCC gets you quite as much security as you might need. Users make mistakes—grant too many permissions, put their password where they shouldn’t, etc. That’s not a problem you can solve with PCC.