[LLVMdev] Current work on type-safety proving?

[Vikram Adve]

Jules,

The link Chris forwarded (safecode.cs.uiuc.edu) describes the most  
relevant work so far.  But that work aims to make ordinary C and C++  
programs memory-safe, without using garbage collection or any other  
automatic memory management scheme, i.e., allowing dangling pointers  
but ensuring they are harmless.  It also allows any casts that are  
legal in C.

If you want to enforce strict type safety with GC and without  
arbitrary casts, you should be able to build on top of SAFECode and  
provide a garbage collector.  You'd have to define what pointer casts  
are legal and check for them.  But SAFECode would give you several  
other checks you need including:
-- array bounds (just looking for 0-length arrays isn't enough)
-- uninitialized variables
-- many stdlib usage checks.

--Vikram
http://www.cs.uiuc.edu/~vadve
http://llvm.cs.uiuc.edu/


On Sep 4, 2006, at 9:04 AM, Jules wrote:

> I was just wondering what existing work has been done on proving
> programs type-safe using the LLVM framework?  I've read the paper on
> memory-safety for embedded systems, but that's not quite what I'm
> looking for, as my application (which involves running untrusted code
> within a trusted context) might fail if a pointer to one object  
> became a
> pointer to another of the same type.
>
> Looking at the documentation, it seems a trivial check for type-safety
> would be simply to ensure that the program didn't use any 'cast'
> instructions, only used the memory allocation facilities of a trusted
> garbage collector, and didn't contain any zero-length arrays (as these
> might be used for unsafe pointer arithmetic).  However I guess that in
> the real world, these constraints would be almost impossible to  
> program
> to (e.g., my simple C++ test programs suggest that it's impossible to
> write any non-trivial C++ program that doesn't generate a 'cast'), so
> there must be circumstances that allow such constructs.
>
> Has any work been done on this?  If not, what pointers would you give
> for places to start?
>
> Thanks,
>
> Jules
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev