<div dir="ltr">Hello,<br><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Apr 3, 2013 at 4:31 PM, John Criswell <span dir="ltr"><<a href="mailto:criswell@illinois.edu" target="_blank">criswell@illinois.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF"><div class="im">
<div>On 4/3/13 8:21 AM, Marcelo Sousa wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">
<div>I am interested in type-based verification of LLVM IR in
the areas of certified compilation and software </div>
</div>
</blockquote>
<br></div>
Can you explain what you mean by type-based verification? Do you
mean that you want to use a set of typing rules to perform
verification, or do you mean something else?<div class="im"><br></div></div></blockquote><div>By type-based verification, I mean to use a set of typing rules that enforce certain properties of interest, namely: memory safety, well-formedness of the SSA code, concurrency related problems, etc. I think that even a type checker for LLVM IR could be useful. Part of the motivation was that it seems to me that the set of typing rules hasn't been properly formalized anywhere and I think it's quite useful as documentation and also for algorithmic type-checking.<br>
</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div text="#000000" bgcolor="#FFFFFF"><div class="im">
<br>
<blockquote type="cite">
<div dir="ltr">
<div>verification. It seems to me that the LLVM IR type system
is rather informal in the sense that there is no paper with a
proper formalization of the type rules, and for example, a
proof of soundness for well-formedness of the code. <br>
</div>
</div>
</blockquote>
<br></div>
Another important feature of the LLVM type system is that it is not
a "safe" type system. It is possible to do all sorts of type unsafe
things, such as casting integers to pointers and dereferencing
them. One of the standard LLVM transforms (load widening) will
generate loads that access memory past the end of a memory object.
LLVM IR is capable of representing all the unsafe computations that
C can do.<div class="im"><br></div></div></blockquote><div>I understand, although this is not a problem if you consider a refined type system that uses type qualifiers. You could then have an integer annotated with a pointer type that was casted from.<br>
</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div text="#000000" bgcolor="#FFFFFF"><div class="im">
<br>
<blockquote type="cite">
<div dir="ltr">
<div>I would like to know if you are aware of any work in this
direction for LLVM IR so that I can compare with my own
implementation.</div>
</div>
</blockquote>
<br></div>
The SAFECode/SVA work uses a points-to analysis called DSA which
infers the types of memory objects. A key result of the work is
that the points-to analysis/type inference results of DSA can be
made sound at run-time. The original version of DSA, working on
older versions of LLVM, was able to find a fairly decent number of
type-safe memory objects. The SAFECode/SVA work developed a simple
type checker that verified that the type-inference results returned
by DSA are consistent (i.e., if DSA says that a memory object is
used in a type-safe manner, then it is actually used in a type-safe
manner). There is also some work by Greg Morrisett's group at
Harvard at creating a verified type-checker for the SAFECode/SVA
system. SAFECode/SVA papers can be found at
<a href="http://sva.cs.illinois.edu/pubs.html" target="_blank">http://sva.cs.illinois.edu/pubs.html</a>.<br></div></blockquote><div><br></div><div>Thanks, this is useful information. Actually, your paper on Memory Safety for Low-Level Software/Hardware interactions is in the direction of what I'm interested. I devised a refined type system for a subset of LLVM IR that enforces separation of IO and regular memory, and identifies use after free. My goal is to apply this type system to verification of the Linux Kernel. <br>
Your work on SVA does not seem to focus on a type-based approach since it's based on run-time monitoring and guaranteeing a safe executing environment. <br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
<br>
As far as formalisms for the LLVM IR, there is one from University
of Pennsylvania (Santosh Nagarakatte, now at Rutgers, was involved
with that work), the one used by Greg Morrisett's group for the
verified type checker, and there might be one from Grigore Rosu's
group here at the University of Illinois. There is also an LLVM
translation validator from Greg Morrisett's group
(<a href="http://llvm-md.org" target="_blank">http://llvm-md.org</a>).<br>
<br>
I think another person wrote asking about translation validation a
few months ago. You might want to search the llvmdev archives for
that conversation.</div></blockquote><div><br></div><div>I am aware of these formalisms, but not sure what you mean by the
verified type checker. I may need to read again their POPL paper but I was not aware of a verified type checker for LLVM IR in Coq.<br><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF"><div class="im"><br>
<br>
<blockquote type="cite">
<div dir="ltr">
<div>Moreover, it would be valuable to get some feedback on
suitable type-based analysis that the LLVM community would
like to have in the infrastructure.</div>
</div>
</blockquote>
<br></div>
LLVM already as a type-based alias analysis (called TBAA) which is
used for optimization. There's a proposal floating around on the
list to improve it; you might want to take a look at that.<br>
<br>
SAFECode can use type-safety to optimize away load/store checks
(provided that it uses garbage collection or automatic pool
allocation to make the optimization sound). Using TBAA instead of
DSA might generate better results. Address Sanitizer (ASan) might
benefit from that optimization as well.<br>
<br>
Automatic pool allocation could also benefit from something like
TBAA.<br>
<br></div></blockquote><div>This is of absolute interest to me. I will look for the proposal.<br><br></div><div>Regards,<br>Marcelo<br></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
I think you'll have to be more specific, though, on what you mean by
type-based analysis and provide details on how it could be applied.<br></div></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>
<br>
I apologize if my response is a bit of a ramble; I'm basically
providing a bit of information hoping that some of it is relevant to
what you are asking. I hope you find some of it useful. <br></div></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div text="#000000" bgcolor="#FFFFFF">
<br>
-- John T.<br>
<br>
<blockquote type="cite">
<div dir="ltr">
<div><br>
</div>
<div>Regards,</div>
<div>Marcelo</div>
</div>
<br>
<fieldset></fieldset>
<br>
<pre>_______________________________________________
LLVM Developers mailing list
<a href="mailto:LLVMdev@cs.uiuc.edu" target="_blank">LLVMdev@cs.uiuc.edu</a> <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a>
</pre>
</blockquote>
<br>
</div>
</blockquote></div><br></div></div>