I am intrigued by and understand the very basics of Proof Carrying Code (PCC) and I recognize that LLVM is a machine-independent intermediate language. LLVM is the intermediate form of many languages, including the new Rust language. Typed Assembly is another style of intermediate form which can be used to generate PCC proofs but it has not gained the same popularity/utility. I've heard of Singularity, Verve and JX.
As I understand it, generating PCC proofs are within practicality even for large programs, but that their resulting size and verification burden (necessary only once per "installation") are non-negligible. I don't care about 10x (discardable) proofs nor several hours of verification - I'm very interested in a provably-safe operating environment.
Is there anything missing from the LLVM language or type system that would prevent us from emitting such proofs? Or can you tell that am I missing something about the bigger picture?
PCC for what properties? Memory safety?
Yes, memory safety which I believe is a minimum policy required to ensure that a process cannot take over the kernel or another application. Seems to me that (popularly) a message passing interprocess-communication scheme restores some of the functionality taken away by direct memory access (Erlang, Singularity OS).
Do you have a citation/reference for your statement about practicality?
Here's something that suggests its practicality to me: "It has been shown that proofs for Java type safety can be compressed to 12%–20% of the size of x86 machine code ... but unfortunately this increases the proof checking time by a factor of 3". -- Interpretation of Necula, Oracle-Based Checking of Untrusted Software by Franz
What research have you done?
I've been following this topic (including the names I mentioned previously) over the years reading and absorbing what I can comprehend.
I think it helps to separate "is it possible to do PCC for LLVM bitcode?" from "why doesn't the Clang compiler currently implement PCC?"
Yes, I'm mostly interested in "is it possible to do PCC for LLVM bitcode?" - but I'm not being too specific because I'm not confident that I understand how all the pieces fit together which is why I'm here trying to get an answer from a human who already gets it and can contribute to the understanding of people who are merely at my stage of understanding.
But see, related to your "why doesn't the Clang compiler currently implement PCC?", I would have assumed that the LLVM compiler (the one that goes from LLVM to assembly) would be the one capable of emitting the proof, since it still has higher level concepts of the code before it gets erased in the final binary (as does, I believe, TAL) and of interest because type-safe languages like C# and Rust compile to LLVM, possibly with enough type information to unify the approach among all LLVM languages. So had I been more specific, I'd be getting shat on for that.
I think it would help to clarify exactly what you're asking about
That's pretty much what I'm looking for!