Lightweight type analysis for memory safety through verification ofAPI uses

[Marcelo Sousa]

(* 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
--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/