[LLVMdev] Current work on type-safety proving?
vadve at cs.uiuc.edu
Mon Sep 4 15:49:11 CDT 2006
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.
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
> 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?
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu
More information about the LLVMdev