lkml.org 
[lkml]   [2013]   [Sep]   [17]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
SubjectLightweight type analysis for memory safety through verification of API uses
From
(* Apologies if this is a duplicate: I screw up the plain text before *)

Hello all,

I've designed and implemented a tool similar to sparse and CQUAL that
does type inference of user specified type qualifiers, e.g. iomem. It
receives an API specification with the type qualifiers and also a
partial order, e.g. IOAddr is not compatible with KernelAddr and
ioremap returns a pointer to IOAddr while __kmalloc returns a pointer
to a KernelAddr.

The tool is part of a verification framework for LLVM that I'm
developing called llvmvf. I'm using the llvmlinux project to compile
with clang and I perform intra/interprocedural analysis on every IR
module. I can easily extend to inter-module analysis for a whole
driver analysis.

The performance results are quite fast when compared to similar tools:
less than 5 min to analyse the entire source code (~9k modules;
millions of constraints).

Initially, I focused on separation of IO vs regular memory and I
implemented a partial transformation that converts inline assembly to
LLVM IR functions because I'm also interested in catching misuses of
atomic instructions with IO memory pointers.

I'm looking for bugs related to misuses of IO pointers to validate my
approach and have a good direction on how to increase the precision.
More importantly, I'm looking for other use cases that are likely to
produce a small number of false positives and could be useful to the
linux kernel community. I would like your general feedback and
suggestions of analysis. In particular, I'm thinking on using this
approach to verify the DMA API, and I'm looking for known bugs that
could be used for validation.

Kind regards,
Marcelo


\
 
 \ /
  Last update: 2013-09-17 15:21    [W:0.049 / U:0.304 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site