4
$\begingroup$

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?

More

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!

$\endgroup$
  • $\begingroup$ While the concepts involved are certainly CS territory, I'm not sure if a question that aims at one specific language is ontopic here. I'll let the community decide. $\endgroup$ – Raphael Nov 11 '15 at 15:00
  • $\begingroup$ PCC for what properties? Memory safety? Do you have a citation/reference for your statement about practicality? What research have you done? Have you tried doing some searching on Google Scholar to find the state-of-the-art in PCC, and to see if you can find any research papers that implement PCC for LLVM? $\endgroup$ – D.W. Nov 11 '15 at 18:14
  • $\begingroup$ Finally, I think it would help to clarify exactly what you're asking about: Extending a C compiler to generate proofs of memory safety as it translates from C to LLVM bitcode? Something else? It's not clear where you expect LLVM to come into it or what task you're hoping about, so some edits to clarify this might help. $\endgroup$ – D.W. Nov 11 '15 at 18:18
  • $\begingroup$ I still think you need to clarify what the source language is. Your citation talks about Java. Doing PCC when the source language is Java is very different than when the source language is C; the latter raises a host of issues not present in Java. Also, there are reasons why you'd want to start from the source language, not from LLVM bitcode. Is an answer that explains those issues and reasons the kind of thing you'd count as a satisfactory answer? $\endgroup$ – D.W. Nov 11 '15 at 19:48
  • $\begingroup$ I'm only considering this now, but I guess that while LLVM is capable of strong type safety mechanisms, a compiler like clang for languages like c which are not enforced as type safe, the resulting LLVM cannot take advantage of those type safe mechanisms either (falling back to some idea of unsafe)? Is a property of type-safety not enough to guarantee memory safety? Rust understands memory safety. So perhaps LLVM lacks a native understanding of the safety property it would need to then emit a proof of that safety property? $\endgroup$ – Jason Kleban Nov 11 '15 at 20:08
2
$\begingroup$

This is a project I've been thinking of venturing into for a few years now, and I was fortunate to have a very useful discussion about it at the time I started planning it with Chris Lattner (at the time, one of the main architects of LLVM, although better known these days perhaps for his work on Swift).

It does seem that there is a possibility of producing correctness proofs for a subset of C (or potentially C++) using LLVM. There has already been some work done which would be useful:

  • As discussed in comments, memory safety is critical. Without memory safety, type safety is essentially irrelevant. A number of memory-safety related analyses and transformations have already been implemented for LLVM that could help. These include:

  • "fat pointers", i.e. transformation of C style pointers into pointers into areas of defined size, in order to catch bound errors

  • a transformation applied to dynamic memory allocation that enables detection of use of pointers after they have been freed. These two features are described in this paper.

For the subset of C programs that perform no type casts, applying these transformations may be adequate. Of course, real C and/or C++ code often uses typecasts, and adding this facility is more challenging. For performance sake, as many of these cases as possible must be caught at verification time rather than runtime, although in the end of the day the use of runtime type information and a dynamic casting implementation would be enough to allow for entirely safe C code.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.