[LLVMdev] LLVM Language Reference Strictness

[John Criswell]

On 10/20/11 4:47 AM, Don Quixote de la Mancha wrote:
> On Thu, Oct 20, 2011 at 2:37 AM, Shea Levy<shea at shealevy.com>  wrote:
>> . The
>> (probably impossible) end-goals to this project would be a) that every
>> program which passes its checks would be as safe to run in kernel mode
>> with full memory access as it would be in user mode
> That would be a very useful thing to have for embedded systems.  Some
> such as uCLinux run ports of "safe" operating systems with the safety
> stripped out, whereas others like Texas Instruments' DSP/BIOS run
> entirely as a single operating system kernel.

You may want to read the early SAFECode papers 
(http://sva.cs.illinois.edu/pubs.html).  The paper "Memory Safety 
without Run-time Checks or Garbage Collection" 
(http://llvm.org/pubs/2003-05-05-LCTES03-CodeSafety.html) and "Ensuring 
Code Safety Without Runtime Checks for Real-Time Control Systems" 
(http://llvm.org/pubs/2002-08-08-CASES02-ControlC.html) are particularly 
relevant and, I believe, would allow you to run user code in kernel 
space safely without resorting to run-time checks.

You might also want to read the SVA paper from Usenix Security 2009 
(http://llvm.org/pubs/2009-08-12-UsenixSecurity-SafeSVAOS.html) and the 
HyperSafe paper 
(http://www.csc.ncsu.edu/faculty/jiang/pubs/OAKLAND10.pdf) to get an 
idea of other memory safety concerns beyond your standard compiler loads 
and stores.  Despite the fact that these papers describe memory safety 
issues for OS kernel/hypervisor code, these issues also effect 
user-space code (e.g., threading libraries, mmap(), etc.).

As an FYI, SAFECode later evolved into a system that could support 
general C programs by using a combination of static analysis, an 
optional memory-region transform, and run-time checks; that is the 
system available today (http://sva.cs.illinois.edu).  The code for those 
older systems should still be in the safecode SVN repository, though, so 
I think you could rebuild the original system which rejected type-unsafe 
programs if you wanted to do so.

On a final note, as long as you have the whole program to analyze, using 
something like SAFECode in its modern form should permit you to run 
user-space code in the kernel as long as you're willing to accept having 
run-time checks.  That said, there is still a fair amount of work to 
make sure that the memory safety is airtight (potentially enough to 
warrant a research paper).  The two issues that come to mind off-hand are:

1)  There's an issue with using the points-to analysis (DSA) on C++ 
programs and C programs that mimic vtables; the points-to analysis 
cannot always tell when it has analyzed the complete program, and that 
can cause SAFECode's checks to loose completeness.

2) There's still some work left for the run-time checks and static 
analysis.  For example, some of the C standard library still needs 
run-time checks (or be processed with SAFECode).  Special checks are 
needed on calls to mmap().  Inline assembly needs to be handled 
somehow.  Of course, you can choose to write a static analysis that 
detects use of those features and rejects the program if those features 
are found.

If you're interested in chatting further on this topic, please feel free 
to email either me or the svadev at cs.illinois.edu mailing list.

-- John T.